Model Checking of Asbru

Andriy Dunets, Simon Bäumler, Arjen Hommersom, Wolfgang Reif

Model Checking of Asbru

Model checking is known as an automatic verification technique which can be applied very efficiently. Formalisation of medical guidelines in Asbru enables us to apply formal verification on medical guidelines. In this deliverable we show, how model checking can be applied to Asbru plans. After a short survey, which model checking techniques are suitable for verification of Asbru, we show how a finite state model can be constructed from Asbru plans and how they can automatically compiled. Further, we discuss what kind of properties can be verified with model checking.

published 24.07.2009 in: Universität Augsburg, Technical Report 2009-14 Technical Report, Institute of Computer Science, University of Augsburg, Juli 2009