zbMATH — the first resource for mathematics

Scenario-based consistency verification of component-based real-time system designs. (Chinese. English summary) Zbl 1096.68671
Summary: For real-time software systems, this paper considers the problem of checking component-based designs for timing scenario-based specifications, which is one of the challenges in real-time computing domain. Firstly the timing scenario-based specifications are specified by UML sequence diagrams with a set of Boolean expressions, then the interface automata for modeling real time systems through adding time intervals on the actions is extended. The component-based designs are modeled by a real-time interface automaton network which contains a set of real-time interface automata synchronized by shared actions. Based on analyzing the compatible integer state space of a real-time interface automata network, a corresponding reachability graph is constructed and finally an algorithm for checking the consistency between the real-time component-based designs and the timing scenario-based specifications is developed.
68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
68N99 Theory of software
Full Text: DOI