Tool Support for Composition and Verification of Formal Behavior

Author

Kolahi, Siamak ; Salah, Aziz ; Mizouni, Rabeb ; Dssouli, Rachida

Author_Institution

Concordia Univ., Montreal

fYear

2007

fDate

18-20 Nov. 2007

Firstpage

471

Lastpage

475

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/IIT.2007.4430441

Filename

4430441