Formal verification of embedded systems based on CFSM networks
Felice Balarin, Harry Hsieh, Attila Jurecska, Luciano Lavagno, Alberto L. Sangiovanni-Vincentelli · 1996
Both timing and functional properties are essential to characterize the correct behavior of an embedded system.Verication is in general performed either by simulation, or by bread-boarding.Given the safety requirements of such systems, a formal proof that the properties are indeed satised is highly desirable.In this paper, we present a formal veri cation methodology for embedded systems.The formal model for the behavior of the system used in POLIS is a network of Codesign Finite State Machines.This model is translated into automata, and veri ed using automatatheoretic techniques.An industrial embedded system is veri ed using the methodology.W e demonstrate that abstractions and separation of timing and functionality is crucial for the successful use of formal veri cation for this example.We also show that in POLIS abstractions and separation of timing and functionality can be done by simple syntactic modi cation of the representation of the system.