Using SPIN and STeP to Verify Business Processes Specifications
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.
KeywordsBusiness Process Model Check Business Transaction Unexpected Situation Partial Order Reduction
Unable to display preview. Download preview PDF.
- 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
- 8.Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems (Specification). Springer, Heidelberg (1992)Google Scholar
- 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