Abstract
We present SAM, a symbolic model checker for ACTL, the action-based version of CTL. SAM relies on implicit representations of Labeled Transition Systems (LTSs), the semantic domain for ACTL formulae, and uses symbolic manipulation algorithms. SAM has been realized by translating (networks of) LTSs and, possibly recursive, ACTL formulae into BSP (Boolean Symbolic Programming), a programming language aiming at defining computations on boolean functions, and by using the BSP interpreter to carry out computations (i.e. verifications).
This work was partly supported by the ESPRIT project GUARDS and by Progetto Coordinato CNR “Metodologie e strumenti di analisi, verifica e validazione per sistemi software affidabili”.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
D. Austry, G. Boudol. Algebre de processus et synchronization, Theoretical Computer Science, 1(30), 1984.
C. Bernardeschi, A. Fantechi, S. Gnesi. Formal Specification and Verification of the Inter-Channel Consistency Network, GUARDS Esprit project, Technical Report D3A4/6004c, 1997.
C. Bernardeschi, A. Fantechi, S. Gnesi, S. Larosa, G. Mongardi, D. Romano. A Formal Verification Environment for Railway Signaling System Design, in Formal Methods in System Design 12, 139–161, 1998.
A. Bouali, S. Gnesi, S. Larosa. The integration Project for the JACK Environment, Bulletin of the EATCS, n.54, pp.207–223, 1994. (see also http://repl.iei.pi.cnr.it/projects/JACK.)
R.S. Boyer, J.S., Moore. “A Computational Logic”, ACM Monograph Series, Academic Press, 1979.
R.E. Bryant. Graph Based algorithms for boolean function manipulation, IEEE Transaction on Computers, C-35(8), 1986.
J.R. Burch, E.M. Clarke, K.L. McMillan, D. Dill, J. Hwang. Symbolic Model Checking 1020 states and beyond, in Proceedings of LICS, 1990.
Clarke, E.M., Emerson, E.A., Sistla, A.P., “Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specification,” ACM Transaction on Programming Languages and Systems, 8(2):244–263, 1986.
R. Cleaveland, J. Parrow, B. Steffen. The Concurrency Workbench, in Proc. of Automatic Verification Methods for Finite State Systems, LNCS 407, pp. 24–37, 1990.
R. Cleaveland, S. Sims. The NCSU Concurrency Workbench, in Proc. of Computer Aided Verification, LNCS 1102, pp. 394–397, 1996.
R. De Nicola, A. Fantechi, S. Gnesi, G. Ristori. An action-based framework for verifying logical and behavioural properties of concurrent systems, Computer Networks and ISDN Systems, 25(7):761–778, 1993.
R. De Nicola, A. Fantechi, S. Gnesi, G. Ristori. Verifying Hardware Components within JACK, in Proceedings of CHARME’ 95, LNCS 987, pp. 246–260, 1995.
R. De Nicola, F. W. Vaandrager. Action versus State based Logics for Transition Systems, Proceedings Ecole de Printemps on Semantics of Concurrency, LNCS 469, pp. 407–419, 1990.
E.A. Emerson, J. Halpern. “Sometime” and “Not never” revisited: On branching versus linear time temporal logic, JACM 33:151–178, 1986.
E.A. Emerson, C. Lei. Efficient Model Checking in Fragments of the Propositional Mu-Calculus, in Proceedings of LICS, pp. 267–278, 1986.
A. Fantechi, S. Gnesi, G. Ristori. From ACTL to μ-Calculus, ERCIM Workshop on Theory and Practice in Verification, Pisa, December 9–11, 1992.
J.C. Fernandez, H. Garavel, A. Kerbrat, L. Mounier, R. Mateescu, M. Sighireanu. CADP: A Protocol Validation and Verification Toolbox, CAV’96, LNCS 1102, pp. 436–440, 1996.
G. Ferro. “AMC: ACTL Model Checker. Reference Manual”, IEI-Internal Report B4-47, December 1994.
M. Hennessy, R. Milner. Algebraic Laws for Nondeterminism and Concurrency, JACM 32:137–161, 1985.
D. Kozen. Results on the Propositional μ-calculus, Theoretical Computer Science, 27:333–354, 1983.
E. Madelaine, R. de Simone. The FC2 Reference Manual, Available by ftp from http://cma.cma.fr:pub/verif as file http://fc2refman.ps.gz, 1993.
R. Milner. Communication and Concurrency, Prentice-Hall International, Englewood Cliffs, 1989.
G.D. Plotkin. A Structural Approach to Operational Semantics, Technical Report DAIMI FN-19, Aarhus University, Dep. of Computer Science, Denmark, 1981.
R. Pugliese, E. Tronci. Automatic Verification of a Hydroelectric Power Plant. FME≐96, LNCS 1051, pp. 425–444, 1996.
V. Roy, R. De Simone. AUTO and Autograph, in Proceedings of the Workshop on Computer Aided Verification, LNCS 531, 65–75, 1990.
C. Stirling. An Introduction to modal and temporal logics for CCS, In Concurrency: Theory, Language, and Architecture, LNCS 391, 1989.
E. Tronci. Hardware Verification, Boolean Logic Programming, Boolean Functional Programming, in Proceedings of LICS, 1995.
E. Tronci. On Computing Optimal Controllers for Finite State Systems, Proc. of the 36th IEEE Conf. on Decision and Control, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fantechi, A., Gnesi, S., Mazzanti, F., Pugliese, R., Tronci, E. (1999). A Symbolic Model Checker for ACTL. In: Hutter, D., Stephan, W., Traverso, P., Ullmann, M. (eds) Applied Formal Methods — FM-Trends 98. FM-Trends 1998. Lecture Notes in Computer Science, vol 1641. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48257-1_14
Download citation
DOI: https://doi.org/10.1007/3-540-48257-1_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66462-8
Online ISBN: 978-3-540-48257-4
eBook Packages: Springer Book Archive