Abstract
The modal logic FULL is designed to capture strong bisimulation over early symbolic transition systems (STSs) for full LOTOS. It provides a compact way of expressing and verifying properties involving both data and transitions. In this paper we present a restricted prototype implementation of a model checker for LOTOS for queries written using the FULL logic. The model checker is developed within the CADP package using XTL.
Chapter PDF
Similar content being viewed by others
Keywords
References
I. Ajubi, G. Scollo, and M. van Sinderen. Formal Description of the OSI Session Layer. In P.H.J. van Eijk, C.A. Vissers, and M. Diaz, editors, The Formal Description Technique LOTOS, pages 89–210. Elsevier Science Publishers B.V. (North-Holland), 1989.
D. Amyot, L. Charfi, N. Gorse, T. Gray, L. Logrippo, J. Sincennes, B. Stepien, and T. Ware. Feature Description and Feature Interaction Analysis with Use Case Maps and LOTOS. In M. Calder and E. Magill, editors, Feature Interactions in Telecommunications and Software Systems VI. IOS Press, May 2000.
M. Broy, S. Merz, and K. Spies, editors. Formal Systems Specification, volume 1169 of Lecture Notes in Computer Science. Springer-Verlag, 1996.
J. Bryans, M. Calder, S. Maharaj, B. Ross, and C. Shankland. Report on Developing a Symbolic Framework for Reasoning about Full LOTOS. Unpublished, 2001.
J. Bryans, A. Verdejo, and C. Shankland. Using Rewriting Logic to implement the modal logic FULL. In D. Nowak, editor, AVoCS’01: Workshop on Automated Verification of Critical Systems, 2001. Oxford University Computing Laboratory technical report PRG-RR-01-07.
J. R. Burch, E. M. Clarke, D. E. Long, K. McMillan, and D. L. Dill. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer Aided Design of Integrated Circuits, 13(4):401–424, 1994.
M. Calder, S. Maharaj, and C. Shankland. A Modal Logic for Full LOTOS based on Symbolic Transition Systems. The Computer Journal, 2001. In press.
M. Calder, S. Maharaj, and C. Shankland. An Adequate Logic for Full LOTOS. In J. Oliveira and P. Zave, editors, Formal Methods Europe’01, LNCS 2021, pages 384–395, 2001.
M. Calder and C. Shankland. A Symbolic Semantics and Bisimulation for Full LOTOS. Technical Report TR-2001-77, University of Glasgow, 2001.
E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512–1542, 1994.
E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, 1999.
E.A. Emerson and A. P. Sistla. Symmetry and model checking. In C. Courcoubetis, editor, Proceedings of the 5th Workshop on Computer Aided Verification, pages 463–478, 1993.
J.-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, R. Mounier, and M. Sighireanu. CADP(CAESAR/ALDEBARAN Development Package): A Protocol Validation and Verification Toolbox. In R. Alur and T. Henzinger, editors, CAV’96, volume 1102 of Lecture Notes in Computer Science, pages 437–440. Springer Verlag, 1996.
R. A. Hardy. RPC Specification in LOTOS. Unpublished manuscript, 2000.
M. Hennessy and H. Lin. Symbolic bisimulations. Theoretical Computer Science, 138:353–389, 1995.
M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the Association for Computing Machinery, 32(1):137–161, 1985.
ISO:8807. Information Processing Systems — Open Systems Interconnection — LOTOS — A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. International Organisation for Standardisation, 1988.
J. J. Joyce and C-J. H. Seger. Linking BDD-based symbolic evaluation to interactive theorem proving. In Proceedings of the 30th Design Automation Conference. Association for Computing Machinery, 1993.
D. Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333–354, 1983.
R. Mateescu and H. Garavel. XTL: A Meta-Language and Tool for Temporal Logic Model-Checking. In Proceedings of the International Workshop on Software Tools for Technology Transfer, July 1998.
C. Pecheur. Using LOTOS for specifying the CHORUS distributed operating system kernel. Computer Communications, 15(2):93–102, March 1992.
S. Rajan, N. Shankar, and M. K. Srivas. An integration of model checking with automated theorem proving. In P. Wolper, editor, Proceedings of the 1995 Workshop on Computer-Aided Verification, volume 939 of LNCS, pages 84–97. Springer-Verlag, 1995.
P. Robinson and C. Shankland. Implementing the modal logic FULL using Ergo. In D. Nowak, editor, AVoCS’01: Workshop on Automated Verification of Critical Systems, 2001. Oxford University Computing Laboratory technical report PRG-RR-01-07.
C. Stirling. Temporal Logics for CCS. In J. de Bakker, W.-P. de Roever, and G Rozenberg, editors, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, volume 354 of LNCS, pages 66–672, REX School/Workshop, Noordwijkerhout, The Netherlands, May/June 1989. Springer-Verlag.
Kenneth J. Turner. An architectural description of intelligent network features and their interactions. Computer Networks, 30(15):1389–1419, September 1998.
Alberto Verdejo and Narciso Marti-Oliet. Implementing CCS in Maude. In Proceedings of FORTE/PSTV 2000, pages 351–366, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 IFIP International Federation for Information Processing
About this paper
Cite this paper
Bryans, J., Shankland, C. (2001). Implementing a Modal Logic Over Data and Processes Using XTL. In: Kim, M., Chin, B., Kang, S., Lee, D. (eds) Formal Techniques for Networked and Distributed Systems. FORTE 2001. IFIP International Federation for Information Processing, vol 69. Springer, Boston, MA. https://doi.org/10.1007/0-306-47003-9_13
Download citation
DOI: https://doi.org/10.1007/0-306-47003-9_13
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-7923-7470-1
Online ISBN: 978-0-306-47003-5
eBook Packages: Springer Book Archive