Abstract
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, check system invariants, but also verify more complex properties defined by temporal logic formulas. To reduce the time-to-market for embedded architectures and assist SystemC designers in the complexity of verification process at design time, we advocate a novel approach where (a) generic safety properties are used for sub-architecture verification during architecture prototyping, and (b) sub-architecture models are built according to the presented (Behavior, Interactions, and Priority) framework, in order to ensure that models verification results still hold for subsequent architecture prototype candidates. This approach best helps the designer at two levels. At the prototype dimensioning level, it introduces a sets of predefined properties for common sub-architecture classes. At the verification level, it enables to check safety properties of a subarchitecture without the need to redo the verification process for next prototypes comprising it. We present the framework and show its feasibility on several examples.