loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Seventh International Conference on Real-Time Computing Systems and Applications (RTCSA'00)
Verifying temporal constraints on data in multi-rate transactions using timed automata
Cheju Island, South Korea
December 12-December 14
ISBN: 0-7695-0930-4
A. Wall, Malardalen Univ., Vasteras, Sweden
K. Sandstrom, Malardalen Univ., Vasteras, Sweden
J. Maki-Turja, Malardalen Univ., Vasteras, Sweden
C. Norstrom, Malardalen Univ., Vasteras, Sweden
Wang Yi, Malardalen Univ., Vasteras, Sweden
Transactions involving multiple tasks, possibly with different period times, are common constructs used in the design of real-time systems. Data flowing through a transaction is usually subject to temporal constraints, such as maximum time from input to output or a maximum time difference between inputs. Such constraints are of great importance to guarantee the correct functioning of the designed system, but normally they cannot be checked using the traditional approach to schedulability analysis. We describe how to use timed automata and reachability analysis to verify such temporal constraints on data in transactions. By making a timed automaton model of the data dependencies in a transaction, we enable automatic verification of timing constraints such as end-to-end latency. The model can handle different computational models and any non-preemptive execution order of the tasks in the transaction. Our experiences from industrial case studies indicate that in a substantial number of applications, the transactions are of sizes that can be handled using this approach.
Index Terms:
program verification; automata theory; transaction processing; real-time systems; reachability analysis; scheduling; temporal constraint verification; multi-rate transactions; timed automata; real-time systems; schedulability analysis; reachability analysis; data dependencies; end-to-end latency; computational models; nonpreemptive execution order
Citation:
A. Wall, K. Sandstrom, J. Maki-Turja, C. Norstrom, Wang Yi, "Verifying temporal constraints on data in multi-rate transactions using timed automata," rtcsa, pp.263, Seventh International Conference on Real-Time Computing Systems and Applications (RTCSA'00), 2000
Usage of this product signifies your acceptance of the Terms of Use.