Title :
Tool Support for Composition and Verification of Formal Behavior
Author :
Kolahi, Siamak ; Salah, Aziz ; Mizouni, Rabeb ; Dssouli, Rachida
Author_Institution :
Concordia Univ., Montreal
Abstract :
In this paper, we present a tool support for formal modeling, automated composition, and formal verification of partial system behaviors described as use case automata (UCAs). The tool, called UCOMV, supports visual modeling of formal behaviors and their merging through the notion of composition expressions. These expressions specify the extension points in the UCAs where the composition is performed, as well as the semantics of the intended composition. UCOMV supports a new incremental approach of building the desired behavioral model by using a formal automated mechanism of composition. In addition, it allows the verification of UCAs over behavioral properties defined as temporal property specifications.
Keywords :
automata theory; formal specification; formal verification; systems analysis; composition expressions; formal automated mechanism; formal behavior; formal modeling; formal verification; partial system behaviors; temporal property specifications; use case automata; visual modeling; Automata; Computer aided software engineering; Computer science; Costs; Decision support systems; Engines; Formal verification; Merging; Safety; Automated Composition; Behavioral Modeling; Formal Verification; Use Case Automata;
Conference_Titel :
Innovations in Information Technology, 2007. IIT '07. 4th International Conference on
Conference_Location :
Dubai
Print_ISBN :
978-1-4244-1840-4
Electronic_ISBN :
978-1-4244-1841-1
DOI :
10.1109/IIT.2007.4430441
