A New Approach to Model Checking of UML State Machines

Issue title: Concurrency Specification and Programming (CS&P)

Article type: Research Article

Authors: Niewiadomski, Artur | Penczek, Wojciech | Szreter, Maciej

Affiliations: ICS, University of Podlasie, Poland. [email protected] | ICS, University of Podlasie and Institute of Computer Science, PAS, Poland. [email protected] | Institute of Computer Science, PAS, Poland. [email protected]

Note: [] Address for correspondence: Institute of Computer Science, University of Podlasie, ul. Sienkiewicza 51, 08-110 Siedlce, Poland

Abstract: 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.

Keywords: UML, Bounded Model Checking, symbolic verification

DOI: 10.3233/FI-2009-0103

Journal: Fundamenta Informaticae, vol. 93, no. 1-3, pp. 289-303, 2009