Algorithms for selecting interactions among timed components based on TIOA/TIOTS

摘要

In a real-time system based on Timed I/O Automata (TIOA)/ Timed I/O Transition System (TIOTS), components are modeled as TIOAs. Yet for a large system, there are often too many interactions among components for system designers to examine manually. To solve this difficulty, we put forth an algorithm that computes the time property- delay- of each interaction. Firstly we formally define path (the interaction among TIOAs), route (one implementation of a specified TIOA in a given environment) and the time property — delay. Secondly, the algorithm divides a interaction into parts, each associated with a TIOA; then computes all possible delays for each TIOA, and finds the maximum delays; finally sums them up to get the total delay of a path. With this novel algorithm, interactions of a timed system can be formally viewed and selected in terms of time criteria in order to verify and test the timed property of the system. Hence we can filter out those interactions (paths) that meet certain time requirements or limitations from the upper level of models. Several applications and examples have shown that our algorithm is effective and facilitates the timed verification of the whole real-time automata system.