The Community for Technology Leaders
2008 10th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (2008)
Timisoara, Romania
Sept. 26, 2008 to Sept. 29, 2008
ISBN: 978-0-7695-3523-4
pp: 480-486
ABSTRACT
Various methodologies to model and analyze timed and hybrid systems using SAL are reported. We assume that the system is specified as a network of timed/hybrid automata with synchronized transitions and urgency. We show how to translate the system into a SAL model with the time domain being either discrete or dense, and the clocks being either saturated or unsaturated. Depending on these choices, various tools provided by SAL to model check reachability properties over the system are used to establish safety properties of timed systems. We profile the performance of these tools with a comparative study.
INDEX TERMS
Timed Automata, SAL, Symbolic Model Checking, k-induction, Digitization
CITATION

P. K. Pandya and P. V. Suman, "Timed and Hybrid Automata in SAL," 2008 10th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing(SYNASC), Timisoara, Romania, 2008, pp. 480-486.
doi:10.1109/SYNASC.2008.9
89 ms
(Ver 3.3 (11022016))