2008 10th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (2008)
Sept. 26, 2008 to Sept. 29, 2008
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SYNASC.2008.9
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.
Timed Automata, SAL, Symbolic Model Checking, k-induction, Digitization
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.