Creation and Validation of Embedded Assertion Statecharts
Demir, Kadir Alpaslan
MetadataShow full item record
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.
Proceedings of the Seventeenth IEEE International Workshop on Rapid System Prototyping (RSP'06)
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 ...
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 ...
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 ...