Model checking of java programs using networks of fadds

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

Abstrakty

EN

In the paper we present the current theoretical base of the J2FADD tool, which translates a Java program to a network of finite automata with discrite data (FADDs).The reason for building the tool is that to model check a concurrent program writ-ten in Java by means of the tools like Uppaal or VerICS (the module VerICS ), an automata model of the Java program must be build first. This is because these tools verify only systems modeled as networks of automata, in particular, systems modeled as networks of FADDs. We also make an attempt to evaluate the J2FADD tool by comparison of it with the two well known Java verification tools: Bandera and Java PathFinder.

Słowa kluczowe

EN

Java programming language; computer programming; PathFinder code; programming languages

PL

język programowania Java; programowanie komputerowe; Pathfinder; języki programowania

• Wydawca: Wydawnictwo Uniwersytetu Humanistyczno-Przyrodniczego im. Jana Długosza w Częstochowie
• Czasopismo: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
• Rocznik: 2009
• Tom: Vol. 14
• Strony: 151--164
• Opis fizyczny: Bibliogr. 16 poz., rys., tab.

Twórcy

autor

Woźna B.

• Institute of Mathematics and Computer Science Jan Długosz University in Częstochowa al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland

autor

Zbrzezny A.

• Institute of Mathematics and Computer Science Jan Długosz University in Częstochowa al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland

Bibliografia

• [1] http://www.ajd.czest.pl/∼modelchecking
• [2] Symbolic Analysis Laboratory (SAL). http://sal.csl.sri.com/ (2008).
• [3] J. Bengtsson, K. Larsen, F. Larsson, P. Pettersson, W. Yi , C. Weise. New generation of Uppaal . In: Proc. Int. Workshop on Software Tools for Technology Transfer, T. Margaria, B. Steffen (Eds.), pp. 43–51, 1998.
• [4] E.M. Clarke, O. Grumberg, D.A. Peled. Model Checking , The MIT Press, Cambridge, Massachusetts, 1999.
• [5] J.C. Corbett, M.B. Dwyer, J. Hatcliff, S. Laubach, C.S. Pǎsǎreanu, Robby, H. Zheng. Bandera: Extracting finite-state models from Java source code. In: Proc. 22nd Int. Conf. on Software Engineering (ICSE ’00), ACM Press, New York, pp. 439-448, 2000.
• [6] P. Dembiński, A. Janowska, P. Janowski, W. Penczek, A. Pólrola, M. Szreter, B. Woźna, A. Zbrzezny. VerICS : A tool for verifying timed automata and Estelle specifications. In:Proc. 9th Int. Conf.on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’03), H. Garavel, J. Hatcliff (Eds.), Lecture Notes in Computer Sience, vol. 2619, pp. 278–283, Springer, Berlin 2003.
• [7] A. Farzan, F. Chen, J. Meseguer, G. Roşu. Formal analysis of Java programs in Java FAN. In: Proc. 16th Int. Conf. on Computer-aided Verification (CAV’04), R. Alur, D.A. Peled (Eds.), Lecture Notes in Computer Sience, vol. 3114, pp. 501-505, Springer, Berlin 2004.
• [8] C.A.R. Hoare. Communicating Sequential Processes , Prentice Hall, London 1985.
• [9] J. E. Hopcroft, J.D. Ullman. Introduction to Automata Theory, Languages, and Computation, Addison-Wesley, Reading, Massachusetts 1979.
• [10] D. Park, U. Stern, J.U. Skakkebaek, D.L. Dill. Java model checking. In: Proc. 15th IEEE Int. Conf. on Automated Software Engineering(ASE’2000), pp. 253-256, IEEE, 2000.
• [11] C. Pǎsǎreanu, W. Visser. Verification of Java program s using symbolic execution and invariant generation. In: Model Checking Software, Proc. SPIN’04 , S. Graf, L. Mounier (Eds.), Lecture Notes in Computer Sience, vol. 2989, pp. 164–181, Springer, Berlin 2004.
• [12] W. Penczek, B. Woźna, A. Zbrzezny. Bounded model checking for the universal fragment of CTL, Fundamenta Informaticae,51, 135–156,2002.
• [13] A. Rataj, B. Woźna, A. Zbrzezny. A translator of Java programs to TADDs. In: Proc. Int. Workshop on Concurrency, Specification and Programming (CS&P’08), pp. 524-535, 2008.
• [14] A. Rataj, B. Woźna, A. Zbrzezny. A translator of Java programs toTADDs. Fundamenta Informaticae, 95, 305-324, 2009.
• [15] A.S. Tanenbaum. Modern Operating Systems , Prentice Hall, Amsterdam 2001.
• [16] A. Zbrzezny, B. Woźna. Towards verification of Java programs in Ver-ICS. Fundamenta Informaticae,85, 533-548, 2008.