Loading...
Please wait, while we are loading the content...
Similar Documents
Tool support for composition and verification of formal behaviors.
| Content Provider | CiteSeerX |
|---|---|
| Author | Kolahi, Siamak |
| 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). Use case Composition, Modeling and Verification (UCOMV) supports visual modeling of formal behaviors and their merging through the notion of composition expression. These expressions determine 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 specification with a formal automated mechanism of composition. In addition, it allows the verification of UCAs over behavioral properties defined as temporal property specifications. We also provide an XML based schema for the presentation of UCA models in other tool extensions to the suit. |
| File Format | |
| Access Restriction | Open |
| Subject Keyword | Formal Modeling Tool Extension Formal Behavior Use Case Composition Extension Point Temporal Property Specification Visual Modeling Uca Model Use Case Automaton Partial System Behavior Formal Automated Mechanism Formal Verification New Incremental Approach Behavioral Property Composition Expression Tool Support Intended Composition |
| Content Type | Text |