A Translator of Java Programs to TADDs

• Autorzy: Rataj A. , Woźna B. , Zbrzezny A.
• Języki publikacji: EN

Abstrakty

EN

The model checking tools Uppaal and VerICS accept a description of a network of Timed Automata with Discrete Data (TADDs) as input. Thus, to verify a concurrent programwritten in Java by means of these tools, first a TADD model of the program must be build. Therefore, we have developed the J2TADD tool that translates a Java program to a network of TADDs; the paper presents this tool. The J2TADD tool works in two stages. The first one consists in translation of a Java code to an internal assembly language (IAL). Then, the resulting assembly code is translated to a network of TADDs. We exemplify the use of the translator by means of the following well-known concurrency examples written in Java: race condition problem, dining philosophers problem, single sleeping barber problem and readers and writers problem.

Słowa kluczowe

EN

translation; Internal Assembly Language (IAL); Java programs

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2009
• Tom: Vol. 93, nr 1-3
• Strony: 305--324
• Opis fizyczny: Bibliogr. 15 poz., tab., wykr.

Twórcy

autor

Rataj A.

autor

Woźna B.

autor

Zbrzezny A.

• IM&CS, Jan Długosz University Al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland,

Bibliografia

• [1] Symbolic analysis laboratory (SAL). http://sal.csl.sri.com/, 2008.
• [2] J. Bengtsson, K. Larsen, F. Larsson, P. Pettersson, W. Yi, and C. Weise. New generation of UPPAAL. In Proceedings of the International Workshop on Software Tools for Technology Transfer, 1998.
• [3] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, Cambridge, 1999.
• [4] J. Corbett, M. Dwyer, J. Hatcliff, Robby C. Pasareanu, S. Laubach, and H. Zheng. Bandera: Extracting finite-state models from java source code. In Proceedings of the 22nd International Conference on Software Engineering(ICSE '00), pages 439-448, New York, NY, USA, 2000. ACM Press.
• [5] P. Dembiński, A. Janowska, P. Janowski, W. Penczek, A. Pólrola, M. Szreter, B. Woźna, 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] Azadeh Farzan, Feng Chen, José Meseguer, and Grigore Ros¸u. Formal analysis of java programs in javafan. In Proceedings of Computer-aided Verification (CAV'04), volume 3114 of LNCS, pages 501 - 505, 2004.
• [7] C.A.R. Hoare. Communicating sequential processes. Prentice Hall, 1985.
• [8] G. J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.
• [9] A. Janowska and P. Janowski. Slicing of timed automata with discrete data. Fundamenta Informaticae, 72(1-3):181-195, 2006.
• [10] K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
• [11] D. Park, U. Stern, J. U. Skakkebaek, and D. L. Dill. Java model checking. In Proceedings of the 15th IEEE International Conference on Automated Software Engineering (ASE'2000).
• [12] C. Pasareanu and W. Visser. Verification of Java Programs Using Symbolic Execution and Invariant Generation. In Proceedings of SPIN'04, volume 2989 of LNCS, pages 164-181. Springer-Verlag, 2004.
• [13] Andrew S. Tanenbaum. Modern Operating Systems. Prentice Hall, Vrije University, Amsterdam, The Netherlands, 2/e edition, 2001.
• [14] A. Zbrzezny and A. Pólrola. Sat-based reachability checking for timed automata with discrete data. Fundamenta Informaticae, 79(3-4):579-593, 2007.
• [15] A. Zbrzezny and B. Woźna. Towards verification of Java programs in VerICS. Fundamenta Informaticae, 85(1-4):533-548, 2008.