Gesellschaft für Informatik e.V.

Lecture Notes in Informatics

INFORMATIK 2011 Informatik schafft Communities P-192, 312-312 (2011).

Gesellschaft für Informatik, Bonn

Copyright © Gesellschaft für Informatik, Bonn


From business modeling to verified applications

Christian Ammann , Stephan Kleuker and Elke Pulvermüller


UML activity diagrams can be used to model business processes which are implemented in a software project. It is a worthwhile goal to automatically transform at least parts of UML diagrams into software. Automated code generation reduces the total amount of errors in a software project but the model itself can still violate specified requirements. A quality improvement is the usage of a model checker which searches through the whole state space of model and checks whether all requirements are met. A model checker requires a formal description of a model for a complete verification. Activity diagrams often describe processes informally which is difficult to verify with a model checker. We therefore propose the transformation of activityto statechart diagrams which allow a more detailed and formal description. Several algorithms exist to map UML statecharts into a model checker input language for a successful formal verification. Afterwards, the model checker searches through the whole state space of a statechart and therefore has to store each state in memory. UML statecharts can reach a high degree of complexity which is problematic for a complete state space traversal because the total amount of available memory is exhausted. Ac- cordingly, we present the domain specific language UDL (UML Statechart Modeling Language) and a transformation from UDL into the Spin model checker input language Promela. UDL contains features for property preserving abstraction which reduces the models state space and therefore the memory consumption of a model checker. Furthermore, we introduce an optimisation technique for the transformation process from UDL to Promela which focuses on a reduced model checker run-time. A case study with a movement tracking system demonstrates how our approach could significantly reduce the memory consumption of a model checker and allows the verification of complex models.

Full Text: PDF

Gesellschaft für Informatik, Bonn
ISBN 978-88579-286-4

Last changed 21.02.2014 20:08:04