Verification of an abstract component using communication patterns

摘要

Model-driven development and verification approaches are highly desirable in embedded systems development since they help identify functional or non-functional issues in the early stage of development when verification complexity is relatively lower than that of the implemented system. Nevertheless, typical model-driven verification approaches focus mainly on functional aspects, leaving the communication behavior largely under-specified. This paper anticipates that understanding and specifying communication mechanism is important in modeling as well as analysis, and suggests a set of communication patterns categorized by the level of abstraction, message handling mechanisms, and buffering strategies. Design of a component may start with the specification of an abstract component with the default communication pattern, which can be recursively verified and refined. Using communication patterns helps us improve the separation of concerns and facilitating smooth transition of a component design from an abstract function-oriented component to a concrete component with detailed communication behavior.