Verifying properties of process definitions

ABSTRACT

It seems important that the complex processes that synergize humans and computers to solve widening classes of societal problems be subjected to rigorous analysis. One approach is to use a process definition language to specify these processes and to then use analysis techniques to evaluate these definitions for important correctness properties. Because humans demand flexibility in their participation in complex processes, process definition languages must incorporate complicated control structures, such as various concurrency, choice, reactive control, and exception mechanisms. The underlying complexity of these control abstractions, however, often confounds the users' intuitions as well as complicates any analysis.Thus, the control abstraction complexity in process definition languages presents analysis challenges beyond those posed by traditional programming languages. This paper explores some of the difficulties of analyzing process definitions. We explore issues arising when applying the FLAVERS finite state verification system to processes written in the Little-JIL process definition language and illustrate these issues using a realistic auction example. Although we employ a particular process definition language and analysis technique, our results seem more generally applicable.

REFERENCES

• 1: Alfred Bröckers , Volker Gruhn, Computer-Aided Verification of Software Process Model Properties, Proceedings of Advanced Information Systems Engineering, p.521-546, June 08-11, 1993
• 2: A. G. Cass , H. Lee , B. S Lerner , L. J. Osterweil, Formally Defining Coordination Processes to Support Contract Negotiation, University of Massachusetts, Amherst, MA, 1999
• 3: James C. Corbett , George S. Avrunin, Using integer programming to verify general safety and liveness properties, Formal Methods in System Design, v.6 n.1, p.97-123, Jan. 1995 [doi>10.1007/BF01384316]
• 4: Matthew B. Dwyer , Lori A. Clarke, Data flow analysis for verifying properties of concurrent programs, Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, p.62-75, December 06-09, 1994, New Orleans, Louisiana, United States
• 5: C. Fernstr~ om. PROCESS WEAVER: Adding process support to UNIX. In Second Int. Conf. on the Software Process, pages 12-26, 1993.
• 6: David Harel , Amir Pnueli , Hagi Lachover , Amnon Naamad , Michal Politi , Rivi Sherman , Aharon Shtull-Trauring , Mark Trakhtenbrot, STATEMATE: A Working Environment for the Development of Complex Reactive Systems, IEEE Transactions on Software Engineering, v.16 n.4, p.403-414, April 1990 [doi>10.1109/32.54292]
• 7: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 8: R. Kadia, Issues encountered in building a flexible software development environment: lessons from the Arcadia project, Proceedings of the fifth ACM SIGSOFT symposium on Software development environments, p.169-180, December 09-11, 1992, Tyson's Corner, Virginia, United States
• 9: M. Kumar and S. I. Feldman. Internet auctions. TR, IBM Institute for Advanced Commerce, Nov 1998.
• 10: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 11: National Institute of Standards and Technology. Integration Definition For Function Modeling (IDEF0), 1993. Federal Information Processing Standards 183.
• 12: Gleb Naumovich , George S. Avrunin , Lori A. Clarke, Data flow analysis for checking properties of concurrent Java programs, Proceedings of the 21st international conference on Software engineering, p.399-410, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302663]
• 13: L. Osterweil, Software processes are software too, Proceedings of the 9th international conference on Software Engineering, p.2-13, March 1987, Monterey, California, United States
• 14: A. Wise, Little-JIL 1.0 Language Report TITLE2:, University of Massachusetts, Amherst, MA, 1998

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS

General Terms:
Design, Experimentation, Management, Measurement, Performance, Theory, Verification