Specification-Based Prototyping for Embedded Systems

Date of Publication: 
September 1999
Authors: 
Mats Heimdahl
Authors: 
Steven Miller
Associated Research Groups: 
Critical Systems Research Group
Publication Files: 
Publication Files: 
Abstract: 
Specification of software for safety critical, embedded computer systems has been widely addressed in literature. 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. It combines the advantages of rigorous formal specifications and rapid systems prototyping. 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 is used as a prototype of the proposed software. Thus, 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 while interacting with software models of its embedding environment or even the physical environment itself (hardware-in-the-loop simulation).
Venue: 
Foundations of Software Engineering, Toulouse, France, September, 1999
Bibtex: 
@InProceedings{Thompson99:nimbus-proto,
  author =   {Jeffrey M. Thompson and Mats P.E. Heimdahl and
                  Steven P. Miller},
  title =    {Specification Based Prototyping for Embedded
                  Systems},
  booktitle =    {Seventh ACM SIGSOFT Symposium on the Foundations on
                  Software Engineering},
  pages =    {163-179},
  year =     1999,
  number =   {1687},
  series =   {LNCS},
  month =    {September},
  annote =   {}
}