Timed and Hybrid Automata in SAL

Author

Suman, P. Vijay ; Pandya, Paritosh K.

Author_Institution

Sch. of Technol. & Comput. Sci., Tata Inst. of Fundamental Res., Mumbai, India

fYear

2008

fDate

26-29 Sept. 2008

Firstpage

480

Lastpage

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.

Keywords

automata theory; formal verification; programming language semantics; public domain software; reachability analysis; software tools; specification languages; SAL; clocks; hybrid automata; model check reachability; open source tool; timed automata; Automata; Clocks; Computer science; Context modeling; Data structures; Job shop scheduling; Real time systems; Scientific computing; Surface-mount technology; Synchronization; Digitization; SAL; Symbolic Model Checking; Timed Automata; k-induction;

fLanguage

English

Publisher

ieee

Conference_Titel

Symbolic and Numeric Algorithms for Scientific Computing, 2008. SYNASC '08. 10th International Symposium on

Conference_Location

Timisoara

Print_ISBN

978-0-7695-3523-4

Type

conf

DOI

10.1109/SYNASC.2008.9

Filename

5204858