Abstract
In this paper we present a verification methodology, using an action-based logic, able to check properties for full CCS terms, allowing also verification on infinite state systems. Obviously, for some properties we are only able to give a semidecision procedure. The idea is to use (a sequence of) finite state transition systems which approximate the, possibly infinite state, transition system corresponding to a term. To this end we define a particular notion of approximation, which is stronger than simulation, suitable to define and prove liveness and safety properties of the process terms.
Chapter PDF
References
J. C. M. Baeten, J. A. Bergstra, J. W. Klop. Deddability of bisimulation equivalence for processes generating context-free languages. Journal of ACM 40, 3, 1993, pp. 653–682.
G. Bruns. A practical technique for process abstraction. CONCUR'93, LNCS 715, pp. 37–49.
A. Bouali, S. Gnesi, S. Larosa. The integration Project for the JACK Environment. Bulletin of the EATCS, n. 54, October 1994, pp. 207–223.
O. Burkart, B. Steffen. Pushdown processes: Parallel Composition and Model Checking. Proceedings, CONCUR 94, LNCS 836, 1994, pp. 98–113.
E.M. Clarke, E.A. Emerson, A.P. Sistla. Automatic Verification of Finite State Concurrent Systems using Temporal Logic Specifications. ACM Toplas, 8 (2), 1986, pp. 244–263.
E.M. Clarke, O. Grumberg, D.E. Long. Model Checking and Abstraction. ACM Toplas, 16 (5), 1994, pp. 1512–1542.
R. Cleaveland, J. Parrow, B. Steffen. The Concurrency Workbench. Proceedings of Automatic Verification Methods for Finite State Systems. Lecture Notes in Computer Science 407, Springer-Verlag, 1990, pp. 24–37.
D.Dams, O.Grumberg, R.Gerth. Automatic Verification of Abstract Interpretation of Reactive Systems: Abstractions Preserving ∀CTL*, ∃CTL*, CTL*. IFIP working conference on Programming Concepts, Methods and Calculi (PROCOMET'94), 1994.
N. De Francesco, P. Inverardi. Proving Finiteness of CCS Processes by Non-standard Semantics. Acta Informatica, 31 (1), 1994, pp. 55–80.
R. De Nicola, A. Fantechi, S. Gnesi, G. Ristori. An action-based framework for verifying logical and behavioural properties of concurrent systems. Computer Network and ISDN systems, Vol. 25, No. 7, 1993, pp 761–778.
R. De Nicola, F. W. Vaandrager. Action versus State based Logics for Transition Systems. Proceedings Ecole de Printemps on Semantics of Concurrency. LNCS 469, 1990, pp. 407–419.
J.C. Fernandez, H. Garavel, L. Mounier, A. Rasse, C. Rodriguez, J. Sifakis. A Toolbox for the Verification of LOTOS Programs. 14th ICSE, Melbourne, 1992, pp. 246–261.
J.C. Fernandez, L. Mounier. Verifying Bisimulations “On the Fly”. Formal Description Techniques, III, Elsevier Science Publisher, pp. 95–110, 1991.
J. C. Godskesen, K. G. Larsen, M. Zeeberg. TAV Users Manual. Internal Report, Aalborg University Center, Denmark, 1989.
M. Hennessy and R. Milner. Algebraic Laws for Nondeterminism and Concurrency. Journal of ACM, 32, 1985, pp. 137–161.
H. Hungar, B. Steffen. Local Model Checking for Context-Free Processes. Proceedings, ICALP 93, LNCS 700, 1993, pp. 593–605
H. Hungar. Local Model Checking for Parallel Composition of Context-Free Processes. Proceedings, CONCUR 94, LNCS 836, 1994, pp. 114–128.
H. Huttel, C Stirling. Actions speak louder than words: Proving Bisimilarity for Context Free Processes. LICS 91, IEEE Computer Society Press, 1991, pp. 376–386.
E. Kindler. Safety and Liveness Properties: A Survey. Bulletin of the EATCS, 53, 1994, pp. 268–272.
E. Madelaine. Verification Tools from the Concur Project. Bulletin of EATCS 47, 1992, pp. 110–120.
E. Madelaine, D. Vergamini. AUTO: A Verification Tool for Distributed Systems Using Reduction of Finite Automata Networks. FORTE '89, North-Holland, 1990, pp. 61–66.
Z. Manna, A. Pnueli. The Anchored Version of the Temporal Framework, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. Lecture Notes in Computer Science 354, Springer-Verlag, 1989, pp. 201–284.
R. Milner. Communication and Concurrency. Prentice Hall, 1989.
D. Taubner. Finite Representations of CCS and TCSP Programs by Automata and Petri Nets. LNCS 369, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
De Francesco, N., Fantechi, A., Gnesi, S., Inverardi, P. (1995). Model checking of non-finite state processes by finite approximations. In: Brinksma, E., Cleaveland, W.R., Larsen, K.G., Margaria, T., Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1995. Lecture Notes in Computer Science, vol 1019. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60630-0_10
Download citation
DOI: https://doi.org/10.1007/3-540-60630-0_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60630-7
Online ISBN: 978-3-540-48509-4
eBook Packages: Springer Book Archive