摘要：Formal verification has become very useful andpopular in last decade in area of embedded systems designand in analysis of critical systems. It can reveal commonerrors, check system invariants, but also verify more complexproperties defined by temporal logic formulas. To reduce thetime-to-market for embedded architectures and assist SystemCdesigners in the complexity of verification process at designtime, we advocate a novel approach where (a) generic safetyproperties are used for sub-architecture verification duringarchitecture prototyping, and (b) sub-architecture models arebuilt according to the presented (Behavior, Interactions, andPriority) framework, in order to ensure that models verificationresults still hold for subsequent architecture prototype candidates. This approach best helps the designer at two levels. Atthe prototype dimensioning level, it introduces a sets of predefined properties for common sub-architecture classes. At theverification level, it enables to check safety properties of a subarchitecture without the need to redo the verification processfor next prototypes comprising it. We present the frameworkand show its feasibility on several examples.
