Slicing of Timed Automata with Discrete Data

• Autorzy: Janowska A. , Janowski P.
• 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*.

Słowa kluczowe

EN

timed systems; Timed Automata; static analysis; program slicing

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2006
• Tom: Vol. 72, nr 1-3
• Strony: 181--195
• Opis fizyczny: bibliogr. 25 poz.

Twórcy

autor

Janowska A.

autor

Janowski P.

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

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 andW. 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 skeletons for branching-time temporal logic. 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 fixpoints. 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 multithreaded programs with JVM concurrency primitives. In Proc. of the Int. Symposium on Static Analysis (SAS'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 Note 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(1):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.