Show simple item record

dc.contributor.authorDrusinsky, Doron
dc.contributor.authorShing, Man-Tak
dc.contributor.authorDemir, Kadir Alpaslan
dc.date2006en_US
dc.date.accessioned2018-11-02T21:32:13Z
dc.date.available2018-11-02T21:32:13Z
dc.date.issued2006
dc.identifier.citationDrusinsky, Doron, M-T. Shing, and Kadir Alpaslan Demir. "Creation and validation of embedded assertion statecharts." Rapid System Prototyping, 2006. Seventeenth IEEE International Workshop on. IEEE, 2006.
dc.identifier.urihttps://hdl.handle.net/10945/60582
dc.descriptionProceedings of the Seventeenth IEEE International Workshop on Rapid System Prototyping (RSP'06)en_US
dc.description.abstractThis 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.en_US
dc.description.sponsorshipThe research reported in this article was funded in part by a grant from the U.S. Missile Defense Agency.
dc.titleCreation and Validation of Embedded Assertion Statechartsen_US
dc.typeArticle
dc.contributor.corporateNaval Postgraduate School
dc.contributor.departmentComputer Science (CS)


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record