Slicing of Timed Automata with Discrete Data

• Autorzy: Janowska, A. , Janowski, P.

Warianty tytułu

PL

Plastrowanie automatów czasowych z danymi dyskretnymi

• Języki publikacji: EN

Abstrakty

EN

The paper proposes how to use static analysis to extract an abstract model of a system. The method uses techniques of program slicing to examine syntax of a system modeled as a set of timed automata with discrete data, a common input formalism of model checkers dealing with time. The method is property driven. The abstraction is exact with respect to all properties expressed in the temporal logic CTL_X*

PL

Praca przedstawia zastosowanie analizy statycznej do uzyskania abstrakcyjnego modelu systemu. Proponowana metoda jest oparta na technice plastrowania programów. Analizie podlega system przedstawiony jako zbiór automatów czasowych rozszerzonych o dane dyskretne, który to formalizm jest stosowany przez weryfikatory modelowe dla systemów czasowych. W przedstawionej metodzie abstrakcja systemu zachowuje prawdziwość formuł logiki temporalnej CTL_X* i jest uzalezniona od weryfikowanej własności.

Słowa kluczowe

PL

systemy czasowe; automat czasowy; analiza statyczna; plastrowanie programów

EN

timed systems; Timed Automata; static analysis; program slicing

• Czasopismo: Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
• Rocznik: 2006
• Tom: Nr 990
• Strony: 1-29
• Opis fizyczny: Bibliogr. 25 poz. rys.

Twórcy

autor

Janowska, A.

autor

Janowski, P.

• Uniwersytet Warszawski 02-097 Warszawa, Banacha 2,

Bibliografia

• [1] A Aho, R Sethi, and J Ullman. Compilers. Addison-Wesley, 1986.
• [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] K. Bartlett, R. Scantlebury, and P. Wilkinson. A note on reliable full-duplex transmission over half-duplex links. Communications of the ACM, 12(5):260-261, 1969.
• [4] G. Behrmann, P. Bouyer, E. Fleury, and K. Larsen. Static guard analysis in timed automata verification. 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 254-277. Springer-Verlag, 2003.
• [5] J. Bengtsson and W. Yi. Timed automata: Semantics, algorithms and tools. In Lecture Notes on Concurrency and Petri Nets, volume 3098 of LNCS. Springer-Verlag, 2004.
• [6] M. Bozga, J-C. Fernandez, and L. Ghirvu. Using static analysis to improve automatic test generation. In Proc. of the 6th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'00), volume 1785 of LNCS, pages 235-250. Springer-Verlag, 2000.
• [7] M. Bozga, J-C. Fernandez, L. Ghirvu, S. Graf, J.P. Krimm, L. Mounier, and J. Sifakis. IF: An intermediate representation for SDL and its applications. In Proc. of SDL Forum'99, 1999.
• [8] V. Braberman, D. Garbervetsky, and A. Olivero. Improving the verification of timed systems using influence information. In Proc. 8th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'02), volume 2280 of LNCS, pages 21-36. Springer-Verlag, 2002.
• [9] E. Clarke and E. Emerson. Design and synthesis of synchronization skele-tons for branching-time temporal logie. In Proc. of Workshop on Logic of Programs, volume 131 of LNCS, pages 52-71. Springer-Verlag, 1981.
• [10] P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by Construction or approximation of fix-points. 4th ACM Symposium on Principles of Programming Languages, 1977.
• [11] C. Daws and S. Yovine. Reducing the number of clock variables of Timed Automata. In Proc. of the IEEE Real- Time Systems Symposium (RTSS'96), pages 73-81. IEEE Comp. Soc. Press, 1996.
• [12] R. Gerth, R. Kuiper, D. Peled, and W. Penczek. A partial order approach to branching time logic model checking. Information and Computation, 150:132-152, 1999.
• [13] J. Hatcliff, J. C. Corbett, M. B. Dwyer, S. Sokolowski, and H. Zheng. A formal study of slicing for multi-threaded programs with JYM concurrency primitives. In Proc. of the Int. Symposium on Static Analysis (S'AS'99), pages 1-18, 1999.
• [14] J. Hatcliff, M. B. Dwyer, and H. Zheng. Slicing software for model construction. In Proc. of the ACM Workshop on Partial Evaluation and Program Manipulation (PEPM'99), volume BRICS NS-99-1 of BRICS Notę Series, 1999.
• [15] T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Journal for Information and Computation, 111 (2): 193-244, 1994.
• [16] G. J. Holzmann. The model checker SPIN. IEEE Trans, on Software Eng., 23(5), 1997.
• [17] A. Janowska and P. Janowski. Slicing timed systems. Fundamenta Informaticae, 60(1-4): 187-210, 2004.
• [18] A. Janowska and P. Janowski. Slicing of timed automata with discrete data. Technical Report 990, ICS PAS, 2006.
• [19] L. Millett and T. Teitelbaum. Slicing promela and its applications to model checking, simulation and protocol understanding. In Proc. of the 4th Int. SPIN Workshop, 1998.
• [20] W. Nabiałek, A. Niewiadomski, W. Penczek, A. Półrola, and M. Szreter. Verics 2004: A model checker for real time and multi-agent systems. In Proc. of the Workshop on Concurency, Specification and Programming (CSP'04), volume 170 of Informatik Berichte. Humboldt University, 2004.
• [21] P. Pettersson and K. G. Larsen. UPPAAL2k. Bulletin of the European Association for Theoretical Computer Science, 70:40-44, 2000.
• [22] F. Tip. A survey of program slicing techniques. Journal of Programming Languages, 3, 1995.
• [23] S. Tripakis and S. Yovine. Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design, 18(l):25-68, 2001.
• [24] A. Valmari. The state explosion problem. In Lecture Notes on Petri Nets I: Basic Models. Advances in Petri Nets, volume 1491 of LNCS. Springer-Verlag, 1998.
• [25] M. Weiser. Program slicing. IEEE Trans, on Software Eng., 10(4), 1984.