A New Approach to Model Checking of UML State Machines

• Autorzy: Niewiadomski A. , Penczek W. , Szreter M.
• Języki publikacji: EN

Abstrakty

EN

The paper presents a new approach to model checking of systems specified in UML. All the executions of an UML system (unfolded to a given depth) are encoded directly into a boolean propositional formula, satisfiability of which is checked using a SAT-solver. Contrary to other UML verification tools we do not use any of the existing model checkers as we do not translate UML specifications into an intermediate formalism. The method has been implemented as the (prototype) tool BMC4UML and some experimental results are presented.

Słowa kluczowe

EN

UML; bounded model checking; symbolic verification

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

Twórcy

autor

Niewiadomski A.

autor

Penczek W.

autor

Szreter M.

• Institute of Computer Science, University of Podlasie, ul. Sienkiewicza 51, 08-110 Siedlce, Poland,

Bibliografia

• [1] G. Behrmann, A. David, K. G. Larsen, J. H°akansson, P. Pettersson, W. Yi, and M. Hendriks. UPPAAL 4.0. In QEST, IEEE Computer Society, pages 125-126, 2006.
• [2] P. Bhaduri and S. Ramesh. Model Checking of Statechart Models: Survey and Research Directions. ArXiv Computer Science e-prints, July 2004.
• [3] A. Cimatti, E. M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. Nusmv 2: An opensource tool for symbolic model checking. In CAV, pages 359-364, London, UK, 2002. Springer-Verlag.
• [4] K. Compton, Y. Gurevich, J. Huggins, and W. Shen. An automatic verification tool for UML. Technical Report CSE-TR-423-00, University of Michigan, 2000.
• [5] M. L. Crane and J. Dingel. On the semantics of UML state machines: Categorization and comparison. Technical Report 2005-501, School of Computing, Queen's University, Kingston, Ontario, Canada, 2005.
• [6] K. Diethers, U. Goltz, and M. Huhn. Model checking UML statecharts with time. In Critical Systems Development with UML - Proceedings of the UML'02 workshop, pages 35-52. Technische Universität München, 2002.
• [7] J. Dubrovin, T. Junttila, and K. Heljanko. Symbolic step encodings for object based communicating state machines. Technical Report B24, Helsinki University of Technology, Laboratory for Theoretical Computer Science, 2007.
• [8] M. E. B. Gutiérrez,M. Barrio-Solórzano,C. E. C. Quintero, and P. de la Fuente. UML Automatic Verification Tool with Formal Methods. Electr. Notes Theor. Comput. Sci., 127(4):3-16, 2005.
• [9] G. J. Holzmann. The SPIN Model Checker : Primer and Reference Manual. Addison-Wesley Professional, September 2003.
• [10] T. Jussila, J. Dubrovin, T. Junttila, T. Latvala, and I. Porres. Model checking dynamic and hierarchical UML state machines. In MoDeV2a, pages 94-110, 2006.
• [11] A. Knapp, S. Merz, and C. Rauh. Model checking - timed UML state machines and collaborations. In FTRTFT, pages 395-416, 2002.
• [12] J. Lilius and I. Paltor. vUML: A tool for verifying uml models. In ASE, pages 255-258, 1999.
• [13] K. Mcmillan. The SMV system. Technical Report CMU-CS-92-131, School of computer Science, Carnegie Mellon University, 1992.
• [14] A. Niewiadomski, W. Penczek, and M. Szreter. Semantyka operacyjna wybranych diagramów UML (In Polish). Technical Report 1009, ICS PAS, 2008.
• [15] OMG. Unified Modeling Language. http://www.omg.org/spec/UML/2.1.2, 2007.
• [16] A. Zbrzezny. A boolean encoding of arithmetic operations. In Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'08), volume 225(3) of Informatik-Berichte, pages 536-547. Humboldt University, 2008.