Scenario-based verification for component-based embedded software designs

In this paper, for embedded software systems we consider the problem of checking component-based designs for scenario-based specifications. The component-based designs are modelled by interface automaton networks which consist of a set of interface automata synchronized by shared actions, and the scenario-based specifications are specified by UML sequence diagrams. Based on investigating the reachability graph of the state space of the interface automaton networks, we develop the algorithms to check the existential consistency and the mandatory existential consistency including the forward, backward, and bidirectional mandatory existential consistency.