Slicing Timed Systems

• Autorzy: Janowska A. , Janowski P.
• Języki publikacji: EN

Abstrakty

EN

This paper presents a method of slicing timed systems to create reduced models for model checking verification. The reduction is made at the very beginning of the verification process and this makes it beneficial and effective in handling the state explosion problem. The method uses techniques of static analysis to examine the syntax of a program and to remove irrelevant fragments of the code. The timed extension of the classical slicing definition is given and applied to Intermediate Language of the verification system Verics and Estelle specification language.

Słowa kluczowe

EN

static analysis; program slicing; system verification; timed systems; Timed Automata

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2004
• Tom: Vol. 60, nr 1-4
• Strony: 187--210
• Opis fizyczny: Bibliogr. 16 poz., wykr.

Twórcy

autor

Janowska A.

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

autor

Janowski P.

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

Bibliografia

• [1] Alur, R., Dill, D.: Automata for Modelling Real-Time Systems, Proc. of the Int. Colloquium on Automata. Languages and Programming (ICALP'90), volume 443 of LNCS. Springer-Verlag, 1Ł)9().
• [2] Bozga, М., Fernandez. J.-C., Ghirvu, L.: Using Static Analysis to Improve Automatic Test Generation, Proc. of the 6th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'00), volume 1785 of LNCS. Springer-Verlag, 2000.
• [3] Bozga, M., Fernandez. J.-C., Ghirvu. L., Graf, S., Krimtn. J., Mounier. L., Sifakis, J.: IF: An Intermediate Representation for SDL and its Applications, Proc. of SDL Forum'99, 1999.
• [4] Browne, M. C., Clarke, E. M., Grumberg, O.: Characterizing Finite Kripke Structures in Propositional Temporal Logic, Theoretical Computer Science. 59(1/2). 1988.
• [5] Clarke, E., Emerson. E.: Design and Synthesis of Synchronization Skeletons for Branching-Time Temporal Logic, Proc. of Workshop on Logic of Programs, volume 131 of LNCS. Springer-Verlag, 1981.
• [6] Dembiński, P., Janowska. A., Janowski, P., Penczek, W., Półrola, A., Szreter, M., Woźna, В., Zbrzezny. A.: VerICS: A Tool for Verifying Timed Automata and Estelle Specifications, Proc. of the 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03), volume 2619 of LNCS, Springer-Verlag, 2003.
• [7] Doroś, A., Janowska, A., Janowski. P.: From Specification Languages to Timed Automata. Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'02). Informatik-Berichte 161(1). Humboldt University. Berlin, 2002.
• [8] Dwyer, M., Hatcliff, J., Schmidt, D.: Bandera: Tools for automated reasoning about software systems behaviour, ECRIM News, 36. 1999.
• [9] Gerth, R., Kuiper, R., Peled. D., Penczek, W.: A Partial Order Approach to Branching Time Logic Model Checking, Proc. of the 3rd Israel Symposium on Theory on Computing and Systems (ISTCS'95), IEEE, 1995.
• [10] Hatcliff, J., Corbett, J. C., Dwyer, M. B., Sokołowski. S., Zheng. H.: A Formal Study of Slicing for Multi-threaded programs with JVM Concurrency Primitives, Proc. of the Int. Symposium on Static Analysis (SAS199), 1999.
• [11l Hatcliff, J., Dwyer. M. B., Zheng. H.: Slicing Software for Model Construction. Proc. of the ACM Workshop on Partial Evaluation and Program Manipulation (PEPM'99), BRICS NS-99-1, 1999.
• [121 Holzmann, G. J.: The Model Checker SPIN. IEEE Trans, on Software Eng., 23(5). 1997.
• [13] ISO/IEC 9074(E), Estelle - A Formal Description Technique Based on an Extended State-Transition Model. International Standards Organization, 1997.
• [14] Millett, L. I., Teitelbaum, Т.: Slicing Promela and Its Applications to Model Checking, Simulation and Protocol Understanding, Proc. of the 4th Int. SPIN Workshop (SPIN’98), 1998.
• [15] Tip. F.: A survey of program slicing techniques. Journal of Programming Languages, 3. 1995.
• [16] Weiser, M.: Program slicing, IEEE Trans, on Software Eng., 10(4), 1984.