Translation of Intermediate Language to Timed Automata with Discrete Data

• Autorzy: Janowska A. , Janowski P. , Wróblewski D.
• Języki publikacji: EN

Abstrakty

EN

The aim of this work is to describe the translation from Intermediate Language, one of the input formalisms of the model checking platform VerICS, to timed automata with discrete data and to compare it with the translation to classical timed automata. The paper presents syntax and semantics of both formalisms, the translation rules as well as a simple example.

Słowa kluczowe

EN

translation; Intermediate Language; Timed Automata

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 85, nr 1-4
• Strony: 235--248
• Opis fizyczny: bibliogr. 10 poz., tab.

Twórcy

autor

Janowska A.

autor

Janowski P.

autor

Wróblewski D.

• Institute of Informatics Warsaw University ul. Banacha 2 02-097 Warsaw, Poland,

Bibliografia

• [1] R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi. An implementation of three algorithms for timing verification based on automata emptiness. In Proc. of the 13th IEEE Real-Time Systems Symposium (RTSS'92), pages 157-166. IEEE Computer Society, 1992.
• [2] R Alur and D Dill. Automata for modelling real-time systems. In Proc. of the Int. Colloquium on Automata, Languages and Programming (ICALP'90), volume 443 of LNCS, pages 322-335. Springer-Verlag, 1990.
• [3] M. C. Browne, E. Clarke, and O. Grumberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59(1/2):115-131, 1988.
• [4] E. Clarke and E. Emerson. Design and synthesis of synchronization skeletons for branching-time temporal logic. In Proc. of Workshop on Logic of Programs, volume 131 of LNCS, pages 52-71. Springer-Verlag, 1981.
• [5] P. Dembiński, A. Janowska, P. Janowski, W. Penczek, A. P´ołrola, M. Szreter, B. Wo´zna, and A. Zbrzezny. VerICS: A tool for verifying Timed Automata and Estelle specifications. In Proc. of the 9th Int. Conf. On Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03), volume 2619 of LNCS, pages 278-283. Springer-Verlag, 2003.
• [6] A. Doroś, A. Janowska, and P. Janowski. From specification languages to Timed Automata. In Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'02), volume 161(1) of Informatik-Berichte, pages 117-128. Humboldt University, 2002.
• [7] T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HYTECH: A model checker for hybrid systems. International Journal on Software Tools for Technology Transfer, 1(1-2):110-122, 1997.
• [8] P. Pettersson and K. G. Larsen. UPPAAL2k. Bulletin of the European Association for Theoretical Computer Science, 70:40-44, February 2000.
• [9] A. Półrola and A. Zbrzezny. Sat-based reachability checking for timed automata with discrete data. In Proc.of the Int. Workshop on Concurency, Specification and Programming (CSP'06), volume 206(2) of Informatik Berichte, pages 207-218. Humboldt University, 2006.
• [10] B. Woźna, A. Zbrzezny, and W. Penczek. Checking reachability properties for timed automata via SAT. Fundamenta Informaticae, 55(2):223-241, 2003.