Test-Time, Run-Time, and Simulation-Time Temporal Assertions in RSP

For cost-effective prototyping, system designers should have a clear understanding of the intended use of the prototype under development. This paper describes a classification of formal specification (temporal) assertions used during system prototyping. The classification introduces two new classes of assertions in addition to the well-known class of test-time assertions: (i) assertions used only during simulation, and (ii) deployable assertions integrated with run-time control flow. Separating the formal specification into three distinct classes allows system designers to develop more effective prototypes to evaluate the different system behaviors and constraints. A prototype of a naval torpedo system is used to illustrate the concept.

• Type: Conference
• Year: 2005
• Where: RSP
• Authors: Doron Drusinsky, Man-tak Shing, Kadir Alpaslan Demir
• Keywords: Deployable Assertions, Formal Specification, Rapid System Prototyping, RSP 2005, Test-time Assertions