Model Checking for Managers

Wil Janssen, Radu Mateescu, Sjouke Mauw, Peter Fennema and Petra van der Stappen

Proceedings of the 6th International SPIN Workshop on Practical Aspects of Model Checking (Toulouse, France), September 1999.

Abstract:

Model checking is traditionally applied to computer system design. It has proven to be a valuable technique. However, it requires detailed specifications of systems and requirements, and is therefore not very accessible. In this paper we show how model checking can be applied in the context of business modeling and analysis by people that are not trained in formal techniques. Spin is used as the model checker underlying a graphical modeling language, and requirements are specified using business requirements patterns, which are translated to LTL. We illustrate our approach using a business model of an insurance company.

16 pages

PDF

PostScript