This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2012 IEEE 17th International Conference on Engineering of Complex Computer Systems
Parameter Synthesis for Hierarchical Concurrent Real-Time Systems
Paris, France France
July 18-July 20
ISBN: 978-1-4673-2156-3
Modeling and verifying complex real-time systems, involving timing delays, are notoriously difficult problems. Checking the correctness of a system for one particular value for each delay does not give any information for other values. It is hence interesting to reason parametrically, by considering that the delays are parameters (unknown constants) and synthesize a constraint guaranteeing a correct behavior. We present here Parametric Stateful Timed CSP, a language capable of specifying hierarchical real-time systems with complex data structures. Although we prove that the synthesis is undecidable in general, we present an algorithm for efficient parameter synthesis that behaves well in practice.
Index Terms:
Clocks,Delay,Cost accounting,Semantics,Real time systems,Reactive power,refinement,CSP,parametric timed verification,model checking,robustness
Citation:
Etienne Andre, Yang Liu, Jun Sun, Jin-Song Dong, "Parameter Synthesis for Hierarchical Concurrent Real-Time Systems," iceccs, pp.253-262, 2012 IEEE 17th International Conference on Engineering of Complex Computer Systems, 2012
Usage of this product signifies your acceptance of the Terms of Use.