In this paper, we address the formal venfication in workflow systems More precisely, we consider the automatic verification of one of the most prominent workflow models, namely the Information Control Nets (ICNs) model We present a powerful method for the qualitative analy sis of ICNs The analysis proposed rests on an observed analogy between ICNs and usual process algebra Actually, ICNs are translated into CCS process algebra agents The properties to be verified are expressed in a temporal logic, the propositional modal ν-calculus The verification is done thanks to model-checking algorithms
Get full access to this article
View all access options for this article.
References
1.
Brooks, S.D.1985. "On the Relationship of CCS and CSP." Technical Report, Carnegie-Mellon University.
2.
Brooks, S.D., C.A.R. Hoare, and A.W. Roscoe.1984. "A Theory of Communicating Sequential Process," ACM, 31(3):560-599.
3.
Brooks, S.D. and A.W. Roscoe.1985. "An Improved Failure Set Model for Communicating Processes," In Seminar on Concurrency, Springer-Verlag, pp. 281-305.
4.
Cook, C.1980. "Office Streamlining Using the ICN Model and Methodology ," In National Computer Conference.
5.
Hennessy, M. and R. Milner.1985. "Algebraic Laws for Nondeterminism and Concurrency," Journal of the ACM, 32(1):137-161.
Menascé, D., V. Almeida, and L. Dowdy.1994. Capacity Planning and Performance Modeling: from Mainframes to Client-Server Systems, Prentice-Hall .
8.
Milner, A.J.R.G.1980. "A Calculus of Communicating Systems," In Lecture Notes in Computer Science 92, Springer-Verlag, pp. 281-305.
9.
Milner, A.J.R.G.1989. Communication and Concurrency , Prentice-Hall.
10.
Milner, R.1991. The Polyadic π-Calculus: A Tutorial. Technical Report, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh.
11.
Milner, R., J. Parrow, and D. Walker. "A Calculus of Mobile Processes," Technical Report, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, 1989.
12.
Nutt, G.J.1990. A Simulation System Architecture for Graphs Model, Springer-Verlag, pp. 417-435.
13.
Nutt, G.J. and C.A. Ellis.1979. "Backtalk: An Office Environment Simulator ," In ICCI'79, Conference Record, pp. 22.3.1-22.3.5.
14.
Petri, C.A.1962. Kommunikation mit Automaten. PhD thesis, Univ. Bonn, West Germany.
15.
Reisig, W.1985. Petri Nets. An Introduction, Volume 4 of Monographs of Theoretical Computer Science, Springer-Verlag.
