@inproceedings{734c563cf8b547d1a9ce2415bb24b4c1,
title = "Model checking for managers",
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.",
author = "W. Janssen and R. Mateescu and S. Mauw and P. Fennema and {Stappen, van der}, P.",
year = "1999",
doi = "10.1007/3-540-48234-2_7",
language = "English",
isbn = "3-540-66499-8",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "92--107",
editor = "D. Dams and R. Gerth and S. Leue and M. Massink",
booktitle = "Theoretical 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)",
address = "Germany",
}