TY - GEN
T1 - Specification-based prototyping for embedded systems
AU - Thompson, Jeffrey M.
AU - Heimdahl, Mats P.E.
AU - Miller, Steven P.
PY - 1999
Y1 - 1999
N2 - 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 for- mal 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).
AB - 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 for- mal 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).
UR - http://www.scopus.com/inward/record.url?scp=84887437658&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84887437658&partnerID=8YFLogxK
U2 - 10.1007/3-540-48166-4_11
DO - 10.1007/3-540-48166-4_11
M3 - Conference contribution
AN - SCOPUS:84887437658
SN - 3540665382
SN - 9783540665380
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 163
EP - 179
BT - Software Engineering, ESEC/FSE 1999 - 7th European Software Engineering Conference, Held Jointly with the 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering, Proceedings
PB - Springer Verlag
T2 - 7th European Software Engineering Conference, ESEC 1999 - Held Jointly with the 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering, FSE 1999
Y2 - 6 September 1999 through 10 September 1999
ER -
