Creation and Validation of Embedded Assertion Statecharts
Author
Drusinsky, Doron
Shing, Man-Tak
Demir, Kadir Alpaslan
Date
2006Metadata
Show full item recordAbstract
This paper addresses the need to integrate formal assertions into the modeling, implementation, and testing of statechart based designs. The paper describes an iterative process for the development and verification of statechart prototype models augmented with statechart assertions using the StateRover tool. The novel aspects of the proposed process include (1) writing formal specifications using statechart assertions, (2) JUnit-based simulation and validation of statechart assertions, (3) JUnit-based simulation and testing of statechart prototype models augmented with statechart assertions, (4) automatic, JUnit- based, white-box testing of statechart prototypes augmented with statechart assertions, and (5) spiral adjustment of model and specification using the test results. We demonstrate the proposed process with a prototype of a safety-critical computer assisted resuscitation algorithm (CARA) software for a casualty intravenous fluid infusion pump.
Description
Proceedings of the Seventeenth IEEE International Workshop on Rapid System Prototyping (RSP'06)
Collections
Related items
Showing items related by title, author, creator and subject.
-
Applying UML-based Formal Specification, Validation, and Verification to Space Flight Control System and Defense Software
Alves, Miriam C. Bergue; Beylin, Konstantin; Drusinsky, Doron; Michael, James Bret; Shing, Man-Tak (Monterey, California. Naval Postgraduate School, 2011-02-01); NPS-CS-11-003This report presents the process and results of a formal computer-aided Specification, Validation and Verification (SV&V) of two mission and safety critical projects: the Brazilian Satellite Launcher flight software, and ... -
Validating UML Statechart-Based Assertions Libraries for Improved Reliability and Assurance
Drusinsky, Doron; Michael, James Bret; Otani, Thomas W.; Shing, Man-Tak (2008);In this paper we present a new approach for developing libraries of temporal formal specifications. Our approach is novel in its use of UML statechart-based assertions for formal specifications and its emphasis on validation ... -
Verification and validation for trustworthy software systems
Michael, James Bret; Drusinsky, Doron; Otani, Thomas W.; Shing, Man-Tak (IEEE, 2011);The close interaction between high-integrity systems and their operating environments places a high priority on understanding and satisfying both functional requirements (what the software must do) and safety requirements ...