Towards Verification of Java Programs in VerICS

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

Abstrakty

EN

VerICS is a tool for the automated verification of timed automata and protocols written in both the Intermediate Language and the specification language Estelle. Recently, the tool has been extended to work with Timed Automata with Discrete Data and with multi-agent systems. This paper presents a prototype Timed Automata with Discrete Data model of Java programs. In addition, we show how to use the model together with the verification core of VerICS to validate the well-known alternating bit protocol written in Java. # Greedy Algorithm for Attribute Reduction

Słowa kluczowe

EN

Timed Automata; discrete data model; Java programs

• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 85, nr 1-4
• Strony: 533-548
• Opis fizyczny: bibliogr. 24 poz., tab., wykr.

Twórcy

autor

Zbrzezny, A.

autor

Woźna, B.

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

Bibliografia

• [1] VerICS. http://verics.ipipan.waw.pl/verics/.
• [2] R. Alur. Timed Automata. In Proceedings of the 11th International Conference on Computer Aided Verification (CAV'99), volume 1633 of LNCS, pages 8-22. Springer-Verlag, 1999.
• [3] A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes Drielsma, P.-C. Héam, J. Mantovani, S. Moedersheim, D. von Oheimb, M. Rusinowitch, J. Santiago, M. Turuani, L. Viganò, and L. Vigneron. The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. In Proceedings of 17th International Conference on Computer Aided Verification (CAV'05), volume 3576 of LNCS, pages 281-285, Edinburgh, Scotland, UK, 2005. Springer-Verlag.
• [4] A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: A new symbolic model verifier. In Proceedings of the 11th International Computer Aided Verification Conference (CAV'99), volume 1633 of LNCS, pages 495-499. Springer-Verlag, 1999.
• [5] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999.
• [6] 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.
• [7] James C. Corbett. Constructing compact models of concurrent java programs. In International Symposium on Software Testing and Analysis, pages 1-10, 1998.
• [8] A. Doroś, A. Janowska, and P. Janowski. From specification languages to Timed Automata. In Proceedings of the International Workshop on Concurrency, Specification and Programming (CS&P'02), volume 161(1) of Informatik-Berichte, pages 117-128. Humboldt University, 2002.
• [9] J. Gu, P. Purdom, J. Franco, and B. Wah. Algorithms for the satisfiability (SAT) problem: a survey. In Satisfiability Problem: Theory and Applications, volume 35 of Discrete Mathematics and Theoretical Computer Science(DIMASC), pages 19-152. American Mathematical Society, 1996.
• [10] K. Havelund and T. Pressburger. Model checking JAVA programs using JAVA PathFinder. International Journal on Software Tools for Technology Transfer (STTT), V2(4):366-381,March 2000.
• [11] G. J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.
• [12] G. J. Holzmann. The model checker SPIN. IEEE transaction on software engineering, 23(5):279-295, 1997.
• [13] ISO/IEC 9074(E), Estelle - a formal description technique based on an extended state-transition model. International Standards Organization, 1997.
• [14] A. Janowska and P. Janowski. Slicing of timed automata with discrete data. Fundamenta Informaticae, 72(1-3):181-195, 2006.
• [15] M. Kacprzak, A. Lomuscio, and W. Penczek. From bounded to unbounded model checking for temporal epistemic logic. Fundamenta Informaticae, 63(2,3):221-240, 2004.
• [16] K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
• [17] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Design Automation Conference (DAC'01), pages 530-535, June 2001.
• [18] 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.
• [19] W. Penczek, B. Woźna, and A. Zbrzezny. Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae, 51(1-2):135-156, 2002.
• [20] P. Pettersson and K. G. Larsen. UPPAAL2k. Bulletin of the European Association for Theoretical Computer Science, 70:40-44, February 2000.
• [21] Knot Pipatsrisawat and Adnan Darwiche. Rsat 2.0: Sat solver description. Technical Report D-153, Automated Reasoning Group, Computer Science Department, UCLA, 2007.
• [22] Raja Vallée-Rai, Phong Co, Etienne Gagnon, Laurie Hendren, Patrick Lam, and Vijay Sundaresan. Soot - a java bytecode optimization framework. In Proceedings of the 1999 conference of the Centre for Advanced Studies on Collaborative research (CASCON '99), page 13. IBM Press, 1999.
• [23] W. Visser, K. Havelund, G. Brat, and S. Park. Model checking programs. In Proceedings of the 15th International Conference on Automated Software Engineering (ASE), September 2000.
• [24] A. Zbrzezny and A. Pólrola. Sat-based reachability checking for timed automata with discrete data. Fundamenta Informaticae, 79(3-4):579-593, 2007.