Checking component-based embedded software designs for scenario-based timing specifications

In this paper, for real-time embedded software we consider the problem of checking component-based designs for scenario-based timing specifications. By adding time intervals on the actions, we extend the interface automata for modelling real-time systems. The component-based designs are modelled by real-time interface automaton networks, which includes a set of real-time interface automata synchronized by shared actions, and the scenario-based timing specifications are specified by UML sequence diagrams with a set of boolean expressions. Based on analyzing the compatible integer state space of a real-time interface automaton network and its compatible reachability graph, we develop an algorithm to check the consistency between real-time component-based designs and the scenario-based timing specifications.