Guiding Component-Based Hardware/Software Co-Verification with Patterns

In component-based hardware/software co-verification, properties of an embedded system are established from properties of its hardware and software components. A major challenge in component-based co-verification is the property formulation problem: (1) what are the system properties to verify, (2) what are the component properties needed for verifying the system properties, and (3) what are the environment assumptions for establishing these properties. We present a pattern-guided approach to the property formulation problem. We develop an embedded architecture description language (EADL). A key feature of EADL is its support to specification of architectural patterns for embedded systems. Such patterns capture recurring system structures and, furthermore, templates for properties to verify on systems following these patterns and strategies for decomposing system properties into component properties. We have applies EADL in co-verification of medical sensor systems, which shows that architectural patterns have major potential in facilitating component-based co-verification.