Specification-based Prototyping for Embedded Systems

Abstract

Specifiction of software for safety critical, embedded computer systems has been widely addressed in literture. To achieve the high level of confidence in a specification's correctness necessary in many applications, manual inspections, formal verification, and simulation must be used in concert. Researchers have successfully addressed issues in inspection and verification; however, results in the areas of execution and simulation of specifications have not made as large an impact as desired. In this paper we present an approach to specification-based prototyping which addresses this issue. This approach combines the advantages of rigourous formal specifications and rapid systems prototyping. We base our work on a modeling language using hierarchical state machines. The approach lets us refine a formal executable model of the system requirements to a detailed model of the software requirements. Throughout this refinement process, the specification issued as a prototype of the proposed software. By using the formal specification as the prototype, we guarantee that the formal specification of the system is always consistent with the observed behavior of the prototype. The approach is supported with the Nimbus environment, a framework that allows the formal specification to execute and interact with software models of its embedding environment or even the physical environment itself (hardware-in-the-loop simulatioan.