Towards verification of Java programs in VerICS

• Autorzy: Orzechowski M. , Woźna B. , Siwiak T.

Warianty tytułu

PL

Na drodze do weryfikacji programów napisanych w Javie w środowisku VerICS

• Języki publikacji: EN

Abstrakty

EN

VerICS has been designed as a tool for automated verification of timed automata, and protocols written in both Intermediate Language and a specification language Estelle. Recently, the tool has been extended to work with so called Timed Automata with Discrete Data and multi-agent systems. The paper presents a prototype of a translator from a subset of the Java programming language to Intermediate Language and Time Automata with Discrete Data, the modeling languages of the VerICS model checker.

PL

Verics został zaprojektowany jako narzędzie do automatycznej weryfikacji automatów czasowych oraz protokołów zapisanych zarówno w języku pośrednim jaki i języku Estelle. Ostatnimi czasy Verics został rozbudowany i obecnie pozwala również na automatyczną weryfikację systemów wieloagentowych oraz protokołów zapisanych za pomocą formalizmu rozszerzonych automatów czasowych. Praca ta opisuje translator z pewnego podzbioru Javy, popularnego ostatnio języka programistycznego, do rozszerzonych automatów czasowych i do języka pośredniego, formalizmów będących językami wejściowymi dla werifikatora Verics.

Słowa kluczowe

EN

VerICS; Java; Intermediate Language; timed automata with discrete data; automated verification

• Wydawca: Instytut Podstaw Informatyki PAN
• Czasopismo: Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
• Rocznik: 2006
• Tom: Nr 997
• Strony: 1--33
• Opis fizyczny: Bibliogr. 37 poz.

Twórcy

autor

Orzechowski M.

autor

Woźna B.

autor

Siwiak T.

• Jan Długosz University al. Armii Krajowej 13/15 42-200 Częstochowa Polska,

Bibliografia

• [1] VerICS. http://verics.ipipan.waw.pl/verics/.
• [2] A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuellar, P. H. Drielsma, P.-C. Heam, J. Mantovani, S. Moeder-sheim, 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 CAV 2005, 11th Int. Conf. on Computer Aided Verification, Edinburgh, Scotland, UK, July 2005.
• [3] P. Blackburn, M. de Rijke, and Y. Yenema. Modal Logic, volume 53 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001.
• [4] A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. NuSMY: A new symbolic model verifier. In Proc. 11th International Computer Aided Verification Conference, pages 495-499, 1999.
• [5] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999. ISBN 0-262-03270-8.
• [6] J. Corbett, M. Dwyer, J. Hatcliff, R. 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] J. C. Corbett. Constructing compact models of concurrent java programs. In International Symposium on Software Testing and Analysis, pages 1-10, 1998.
• [8] P. Dembiński, A. Janowska, P. Janowski, W. Penczek, A. Półrola, 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 W), volume 2619 of LNCS, pages 278-283. Springer-Verlag, 2003.
• [9] 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.
• [10] N. Een and N.Sörensson. MiniSat. http://www.cs.chalmers.se/Cs/Research/Formal Methods/MiniSat/.
• [11] J. Gosling, B. Joy, G. Steele, and G. Bracha. The Java Language Specification. Addison Wesley Longman, Inc., second edition, June 2000.
• [12] 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.
• [13] 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.
• [14] G. J. Holzmann. The model checker SPIN. IEEE transaction on software engineering, 23(5):279-295, 1997.
• [15] G. J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.
• [16] ISO 9074. ISO/IEC 9074(E), Estelle - a formal description technique based on an extended state-transition model. International Standards Organization, 1997.
• [17] A. Janowska and P. Janowski. Slicing of timed automata with discrete data. Fundamenta Informaticae, 72(1-3):181-195, 2006.
• [18] A. Janowska and P. Janowski. Slicing timed systems. Fundamenta Informaticae, 60(1-4):187-210, 2004.
• [19] A. Janowska and W. Penczek. Path compression in timed system In Proceedings of the International Workshop on Concurrency Specification and Programming (CS&P'06), volume 206(3) of Informatik-Berichte, pages 340-351. Humboldt University, 2006.
• [20] 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.
• [21] A. Lomuscio, B. Woźna, and A. Zbrzezny. Bounded model checking real-time multi-agent systems with clock differences: theory and implementation. In Proceedings of the 4th Workshop on Model Checking and Artificial Intelligence (MoChArt'06), pages 62-78, Riva Del Garda, Italy, 2006. ECCAI.
• [22] K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993. ISBN 0-7923-9380-5.
• [23] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient S AT solver. In Proceedings of the 38th Design Automation Conference (DAC'01), pages 530-535, June 2001.
• [24] C. Pasareanu and W. Visser. Verification of Java programs using symbolic execution and invariant generation. In Proceedings of SPIN 2004, volume 2989 of LNCS, pages 164-181, Barcelona, Spian, April 2004. Springer-Verlag.
• [25] 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.
• [26] W. Penczek, B. Woźna, and A. Zbrzezny. Towards bounded model checking for the universal fragment of TCTL. In Proceedings of the 7th International Symposium on Format Techniques in Real-Time and Fault Tolerant Systems (FTRTFT'02), volume 2469 of LNCS, pages 265-288. Springer-Verlag, 2002.
• [27] P. Pettersson and K. G. Larsen. UPFAAL2k. Bulletin of the European Association for Theoretical Computer Science, 70:40-44, Feb. 2000.
• [28] A. Półrola, W. Penczek, and M. Szreter. Reachability analysis for Timed Automata using partitioning algorithms. Fundamenta Informaticae, 55(2):203-221, 2003.
• [29] M. Szreter. Selective search in bounded model checking of reachability properties. In Proceedings of 3rd International Symposium on Automated Technology for Verification and Analysis (ATVA'05), volume 3707 of LNCS, pages 159-173, Taipei, Taiwan, October 2005. Springer Berlin / Heidelberg.
• [30] 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.
• [31] B. Woźna. Bounded Model Checking for the universal fragment of CTL*. Fundamenta Informaticae, 63(l):65-87, 2004.
• [32] B. Woźna, A. Zbrzezny, and W. Penczek. Checking reachability properties for Timed Automata via SAT. Fundamenta Informaticae, 55(2):223-241, 2003.
• [33] B. Woźna, A. Lomuscio, and W. Penczek. Bounded model checking for knowledge over real time. In Proceedings of the 1st International Conference on Autonomous Agents and Multi-Agent Systems (AA-MAS'05), volume I, pages 165-172. ACM Press, July 2005.
• [34] A. Zbrzezny Improvements in SAT-based reachability analysis for timed automata. Fundamenta Informaticae, 60(1-4) :417-434, 2004.
• [35] A. Zbrzezny SAT-based reachability checking for timed automata with diagonal constraints. Fundamenta Informaticae, 67(1-3) :303-322, 2005.
• [36] A. Zbrzezny and A. Półrola. Sat-based reachability checking for timed automata with discrete data. In Proceedings of the International Workshop on Concurrency, Specification and Programming (CS&P'06), volume 206(2) of Informatik-jierichte, pages 207-218. Humboldt University, 2006.
• [37] L. Zhang, C. Madigan, M. Moskewicz, and S. Malik. Efficient conflict driven learning in a boolean satisfiability solver. In Proceedings of International Conference on Computer-Aided Design (IC-CAD'01), pages 279-285, 2001.