A toolset for the specification and verification of embedded systems

Abstract

Because of many malfunctions of some critical real-time systems (Pentium bug, Ariane lance rocket), which have caused life and billion dollars loss, computer aided formal methods have been developed and successfully applied for the debugging and the verification of hardware/software. The cost of correction of a hardware/software bug is huge enough to justify high expenses to develop more and more verification techniques to safeguard investments. Present software verification technology can certainly be useful but is yet too limited to cope with the formidable challenge caused by the fast development of the technology essentially the embarked one. In this paper, we underline the various features of a tool based on four different systems: a specification, a simulation, a verification and a code-generation models. The ABP protocol is introduced as an application test.