Affiliations: ICS, University of Podlasie, Poland.
artur@iis.ap.siedlce.pl | ICS, University of Podlasie and Institute of Computer
Science, PAS, Poland. penczek@ipipan.waw.pl | Institute of Computer Science, PAS, Poland.
mszreter@ipipan.waw.pl
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
