AUTOMATICALLY CHECKING REAL-TIME SYSTEMS FOR LINEAR DURATION PROPERTY

In this paper, some design ideas, as well as some related algorithms, of a tool on checking a real-time system for a linear duration property are presented. Timed automata are used as the model language for real-time systems. Networks of timed automata with shared variables and channels are introduced as model language for concurrent real-time systems. Users can compose a network into a timed automaton through the composition program available in this tool when checking the network. Considering the infinite state space of a timed automaton, the concepts of "integral state" and "state equivalence" are introduced in this paper to divide the infinite state space into finite number of equivalence classes. Then the model can be checked through exploring the space of equivalent classes. However, the number of equivalence classes is generally too large for a computer to manipulate, so the primitive search algorithm is only theoretically feasible. In order to enhance the tool’s ability, the algorithms in this tool adopt some techniques to avoid exhaustive exploring the space in order to get better time- and space-efficiency.