Abstract
In this paper we describe modeling for verification of business process with Spin model checker. Our primary goal is the development of Promela language description for e–invoice web service. Modeling for verification follows Church’s synthesis problem: for input scenario “data–flow” model, output is Promela model. Sequence of model transformations translates the scenario into the Promela language code. At the end whole process is illustrated with e–invoice web service example.
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
van der Aalst, W.: The application of petri nets for workflow management. The Journal of Circuits, Systems and Computers 8(1), 21–66 (1998)
Milner, R.: A Calculus of Communicating Systems, vol. 92. Springer, Berlin (1980)
Holzmann, G.: Spin model checker, the: primer and reference manual, 1st edn. Addison-Wesley Professional (2003)
Uchitel, S., Brunet, G., Chechik, M.: Synthesis of partial behavior models from properties and scenarios. IEEE Transactions on Software Engineering 35(3), 384–406 (2009)
OASIS Standard, Web Services Business Process Execution Language Version 2.0 (2007), http://docs.oasis-open.org/wsbpel/2.0/OS/wsbpel-v2.0-OS.html
Crnkovic, I., Sentilles, S., Vulgarakis, A., Chaudron, M.R.V.: A classification framework for software component models. IEEE Transactions on Software Engineering 37(5), 593–615 (2011)
Grosse-Rhode, M.: Semantic integration of heterogeneous formal specifications via transformation systems (2001)
Caskurlu, B.: Model Driven Engineering. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 286–298. Springer, Heidelberg (2002)
Whittle, J., Jayaraman, P.K.: Synthesizing hierarchical state machines from expressive scenario descriptions. ACM Trans. Softw. Eng. Methodol. 19(3) (2010)
Blaskovic, B., Randic, M.: From declarative model to solution: Scheduling scenario synthesis. In: 9th International Conference on Telecommunications, ConTel 2007, Zagreb, Hrvatska, June 13-15, pp. 139–142 (2007), doi:10.1109/CONTEL.2007.381862.
Blaskovic, B., Randic, M.: Model Based Scheduling Scenario Generation. In: Katalinic, B. (ed.) DAAAM International Scientific Book, pp. 031–044. DAAAM International, Vienna (2006) ISBN 3-901509-47-X, ISSN 1726-968704, doi: 0.2507/daaam.scibook.2006.04
Blašković, B., Lovrek, I.: Verification of Signalling Protocols for Telecommunication Services in Intelligent Network Environment. In: 1st International Workshop on Applied Formal Methods in System Design, Maribor, pp. 156–165 (June 1996)
Murata, T.: Petri Nets: Properties, Analysis and Applications. Proceedings of the IEEE 77, 541–580 (1989) (an invited survey paper)
Bhaduri, P., Ramesh, S.: Model Checking of Statechart Models: Survey and Research Directions, CoRR, cs.SE/0407038 (2004)
Korenblat, K., Grumberg, O., Katz, S.: Translations between Textual Transition Systems and Petri Nets. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 339–359. Springer, Heidelberg (2002)
Varpaaniemi, K.: Efficient Detection of Deadlocks in Petri Nets. Series A: Research Reports 26. Helsinki University of Technology, ESPOO, Finland (October 1993)
Gronberg, P., Tiusanen, M., Varpaaniemi, K.: PROD - A Pr/T-Net Reachability Analysis Tool. Series B: Technical Reports 11. Helsinki University of Technology, ESPOO, Finland (June 1993)
Dutertre, B., Moura, L.D.: The YICES SMT solver. Tech. Rep., SRI (2006)
Wooldridge, M.J.: Introduction to multiagent systems. Wiley (2002)
Shoham, Y., Leyton-Brown, K.: Multiagent Systems - Algorithmic, Game-Theoretic, and Logical Foundations. Cambridge University Press (2009)
Omg unified modeling languageTM (omg uml), OMG Document Number: formal/2009-02-04, Infrastructure Version 2.2 (2009)
ITU, Z.100 Specification and Description Language (SDL). ITU-T Telecommunication Standardisation Sector, Geneva (August 2002)
ITU, Z.120 Message Sequence Charts (MSC). ITU-T Telecommunication Standardisation Sector, Geneva (April 2004)
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Blašković, B., Skočir, Z., Humski, L. (2012). Scenario Modeling and Verification for Business Processes. In: Jezic, G., Kusek, M., Nguyen, NT., Howlett, R.J., Jain, L.C. (eds) Agent and Multi-Agent Systems. Technologies and Applications. KES-AMSTA 2012. Lecture Notes in Computer Science(), vol 7327. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30947-2_46
Download citation
DOI: https://doi.org/10.1007/978-3-642-30947-2_46
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-30946-5
Online ISBN: 978-3-642-30947-2
eBook Packages: Computer ScienceComputer Science (R0)