Systematic Verification of Embedded Components with Re-usable Properties

Formal verification has become very useful and popular in last decade in area of embedded systems design and in analysis of critical systems. It can reveal common errors like deadlocks, starvation, check system invariants, but also verify more complex properties defined by LTL formulas whose writing may be very error prone for non expert users. To reduce the time-to-market for embedded systems and assist designers in the complexity of verification step at design time, we advocate the pre-development of re-usable behavioral properties for each family of embedded components to be verified. The proposed approach is to pre-define the re-usable properties by specifying them as logics on standard input/output signals and standard data values. Obtaining this re-usable form enables them to be used for every new component in the product line, hence without the need to spend additional time to redo the verification setup every time a new component is used to create a new design. We have successfully pre-defined LTL re-usable properties for widely used industrial embedded components families such as fifos and buses, and have performed generic verification using SPIN tool.