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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Caesar/Aldebaran Development Package homepage. Available at: http://www.inrialpes.fr/vasy/cadp.html
Property Specification Patterns for Finite-state Verification, ia]Matthew B. Dwyer, George S. Avrunin and James C. Corbett. In: Proceedings of the 2nd Workshop on Formal Methods in Software Practice, March, 1998.
Eertink, H., W.P.M. Janssen, P.H.W.M. Oude Luttighuis, W. Teeuw, and C.A. Vissers, A Business Process Design Language. In: Proceedings World Congress on Formal Methods. Springer LNCS. Toulouse, September 1999.
Franken, H.M. and W. Janssen, Get a grip on changing business processes, Knowledge & Process Management (Wiley), Vol. 5, No.4, pp.208–215. December 1998.
Garavel, H., OPEN/CAESAR: An open software architecture for verification, simulation and testing. INRIA Rapport de recherche n3352, January 1998.
Havelund, K., M. Lowry and J. Penix. Formal analysis of a space craft controller using Spin. in G. Holzman, E. Najm and A. Serhrouchni (eds.), Proceedings of the 4th International SPIN Workshop, Paris, France, Nov. 1998, pp. 147167.
Holzman, G.J., The model checker SPIN, IEEE Transactions on Software Engineering, Vol. 23, No. 5, May 1997, 279–295.
Jacobson, I., M. Ericsson en A. Jacobson, The Object Advantage-Business Process Reengineering with Object Technology, ACM Books, 1995.
Jonkers, H., W. Janssen, A. Verschut and E. Wierstra, “A unified framework for design and performance analysis of distributed systems”, in Proceedings of the 3rd Annual IEEE International Computer Performance and Dependability Symposium (IPDS”98), Durham, NC, USA, Sept. 1998, pp. 109–118.
Janssen, W., R. Mateescu, S. Mauw and J. Springintveld, Verifying business processes using SPIN, in G. Holzman, E. Najm and A. Serhrouchni (eds.), Proceedings of the 4th International SPIN Workshop, Paris, France, Nov. 1998, pp. 21–36. Also available at: http://netlib.bell-labs.com/netlib/spin/ws98/sjouke.ps.gz
Kars, P., The application of Promela and Spin in the BOS project. In: Proceedings Second Spin Workshop. August 1996. Available at: http://netlib.belllabs.com/netlib/spin/ws96/papers.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Janssen, W., Mateescu, R., Mauw, S., Fennema, P., van der Stappen, P. (1999). Model Checking for Managers. In: Dams, D., Gerth, R., Leue, S., Massink, M. (eds) Theoretical and Practical Aspects of SPIN Model Checking. SPIN 1999. Lecture Notes in Computer Science, vol 1680. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48234-2_7
Download citation
DOI: https://doi.org/10.1007/3-540-48234-2_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66499-4
Online ISBN: 978-3-540-48234-5
eBook Packages: Springer Book Archive