A Formal Framework to Integrate Timed Security Rules within a TEFSM-Based System Specification

Abstract--Formal methods are very useful in software industry and are becoming of paramount importance in practical engineering techniques. They involve the design and the modeling of various system aspects expressed usually through different paradigms. In this paper, we propose to combine two modeling formalisms in order to express both functional and security timed requirements of a system. First, the system behavior is specified based on its functional requirements using TEFSM (Timed Extended Finite State Machine) formalism. Second, this model is augmented by applying a set of dedicated algorithms to integrate timed security requirements specified in Nomad language. This language is well adapted to express security properties such as permissions, prohibitions and obligations with time considerations. The resulting secure model can be used for several purposes such as code generation, specification correctness proof, model checking or automatic test generation. In this paper, we appl...

• Type: Journal
• Year: 2009
• Where: APSEC
• Authors: Wissam Mallouli, Amel Mammar, Ana R. Cavalli
• Keywords: APSEC 2009, Nomad Language, Software Engineering, State Machines, Test Generation