Using SPIN and STeP to Verify Business Processes Specifications

  • Juan C. Augusto
  • Michael Butler
  • Carla Ferreira
  • Stephen-John Craig
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2890)


Business transactions are prone to failure and having to deal with unexpected situations. Some business process specification languages, e.g. StAC, introduce notions like compensation handling. Given the need of verification of correctness in business related software, it is important to fill in the gap between business process specification languages like StAC and the verification software already available.

We report on two of our previous attempts to develop a tool to allow verification of StAC specifications by using already existing systems, SPIN and STeP. We highlight some of the problems we faced during these attempts as they can prevent successful and widespread use of verification tools. Our experience can be used to make the available tools more versatile and hence, useful to a wider range of applications.


Business Process Model Check Business Transaction Unexpected Situation Partial Order Reduction 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Augusto, J., Butler, M.: Some Observations About Using SPIN and STeP to Verify StAC Specifications. Technical report, DSSE-TR-2002-9, Electronics and Computer Science Department, University of Southampton, 34 pages (2002)Google Scholar
  2. 2.
    Abrial, J.: The B-Book: Assigning Programs to Meanings. Cambridge University, Cambridge (1996)zbMATHCrossRefGoogle Scholar
  3. 3.
    Bjorner, N., Browne, A., Colon, M., Finkbeiner, B., Manna, Z., Sipma, B., Uribe, T.: Verifying temporal properties of reactive systems: A step tutorial. Formal Methods in System Design 16, 227–270 (1999)CrossRefGoogle Scholar
  4. 4.
    Butler, M., Ferreira, C.: A process compensation language. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM 2000. LNCS, vol. 1945, pp. 61–76. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  5. 5.
    Chessell, M., Griffin, C., Vines, D., Butler, M., Ferreira, C., Henderson, P.: Extending the concept of transaction compensation. IBM Journal of Systems and Development 41(4), 743–758 (2002)CrossRefGoogle Scholar
  6. 6.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)zbMATHGoogle Scholar
  7. 7.
    Holzmann, G.: The spin model checker. IEEE Trans. on Software Engineering 23(5), 279–295 (1997)CrossRefMathSciNetGoogle Scholar
  8. 8.
    Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems (Specification). Springer, Heidelberg (1992)Google Scholar
  9. 9.
    Manna, Z.: The STeP group. STeP: The Stanford Temporal Prover (Educational Release), User’s Manual. Technical report, STAN-CS-TR-95-1562, Computer Science Department, Stanford University. 138 pages (1995)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Juan C. Augusto
    • 1
  • Michael Butler
    • 1
  • Carla Ferreira
    • 1
  • Stephen-John Craig
    • 1
  1. 1.Declarative Systems and Software Engineering Research Group, Department of Electronics and Computer ScienceUniversity of SouthamptonSouthamptonUK

Personalised recommendations