Banerjee, A. ; Ray, S. ; Dasgupta, P. ; Chakrabarti, P. P. ; Ramesh, S. ; Vignesh, P. ; Ganesan, V. (2008) A dynamic assertion-based verification platform for UML statecharts over rhapsody In: TENCON 2008 - 2008 IEEE Region 10 Conference, 19-21 November 2008, University of Hyderabad, Hyderabad, India.
Full text not available from this repository.
Official URL: http://ieeexplore.ieee.org/document/4766503/
Related URL: http://dx.doi.org/10.1109/TENCON.2008.4766503
Abstract
For quite some time, the Unified Modeling Language (UML) has been adopted by designers of safety critical control systems such as automotive and aviation control. This has led to an increased emphasis on setting up a validation flow over UML that can be used to guarantee the correctness of UML models. In this paper, we propose a dynamic Assertion-based verification (ABV) framework for validation of UML Statecharts over the Rhapsody platform of I-logix. We present an extension of Linear Temporal Logic (LTL), named Action-LTL that allows assertions to be specified over data attributes and events of UML models. We present a methodology for automatic generation of Rhapsody Statecharts from Action-LTL specifications. These generated Statecharts are added as simulation observers to an existing UML model to detect specification violations during simulation. In view of the capacity limitations of existing formal assertion-based verification tools, we believe that our methods are of immediate practical value to the UML-based design community.
| Item Type: | Conference or Workshop Item (Paper) |
|---|---|
| Source: | Copyright of this article belongs to Institute of Electrical and Electronics Engineers. |
| Keywords: | Unified Modeling Language; Formal Specification; Program Verification; Temporal Logic |
| ID Code: | 101671 |
| Deposited On: | 12 Dec 2016 09:56 |
| Last Modified: | 12 Dec 2016 09:56 |
Repository Staff Only: item control page
