Model checking for managers

W. Janssen, R. Mateescu, S. Mauw, P. Fennema, P. Stappen, van der

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

36 Citations (Scopus)


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.
Original languageEnglish
Title of host publicationTheoretical and Practical Aspects of SPIN Model Checking (Proceedings 5th and 6th International Workshops, Trento, Italy, July 5, 1999, Toulouse, France, September 21 and 24, 1999)
EditorsD. Dams, R. Gerth, S. Leue, M. Massink
Place of PublicationBerlin
ISBN (Print)3-540-66499-8
Publication statusPublished - 1999

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Dive into the research topics of 'Model checking for managers'. Together they form a unique fingerprint.

Cite this