Kolahi, Siamak (2008) Composition and verification of formal behaviors. Masters thesis, Concordia University.
Preview |
Text (application/pdf)
5MBMR42532.pdf - Accepted Version |
Abstract
In this thesis, we present a platform and a tool support for formal modeling, automated composition, and formal verification of partial system behaviors defined as Use Case Automata (UCAs). Based on research works [24, 31, 32], the Use case Composition, Modeling and Verification (UCOMV) is presented as tool support for the visual modeling of formal behaviors and their merging through the notion of composition expression. The composition expressions determine the extension points in the use cases where the composition is performed, and the operators for the semantics of the composition. The theory and the tool supports a new incremental approach of building the desired system specification with a formal automated mechanism of composition. In addition, it allows the verification of UCAs over temporal properties defined as part of the system requirements specification using an integrated model verification tool. The UCOMV also provides features on traceability of the requirements, and an XML based schema for the introduction of new operators for UCAs composition.
| Divisions: | Concordia University > Gina Cody School of Engineering and Computer Science > Computer Science and Software Engineering |
|---|---|
| Item Type: | Thesis (Masters) |
| Authors: | Kolahi, Siamak |
| Pagination: | xi, 144 leaves : ill. ; 29 cm. |
| Institution: | Concordia University |
| Degree Name: | M. Comp. Sc. |
| Program: | Computer Science and Software Engineering |
| Date: | 2008 |
| Thesis Supervisor(s): | Dssouli, Rachida and Salah, Aziz |
| Identification Number: | LE 3 C66C67M 2008 K65 |
| ID Code: | 976024 |
| Deposited By: | Concordia University Library |
| Deposited On: | 22 Jan 2013 16:18 |
| Last Modified: | 13 Jul 2020 20:09 |
| Related URLs: |
Repository Staff Only: item control page
Download Statistics
Download Statistics