Abstract
We present a logic for reasoning about state transition systems (LOTOS behaviours) which allows properties involving repeated patterns over actions and data to be expressed. The state transition systems are derived from LOTOS behaviours; however, the logic is applicable to any similar formalism. The semantics of the logic is given with respect to symbolic transition systems, allowing reasoning about data to be separated from reasoning about flow of control. Several motivational examples are included.
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.
Similar content being viewed by others
References
Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23, 279–295 (1997)
International Organisation for Standardisation: Information Processing Systems – Open Systems Interconnection – LOTOS – A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour (1988)
Calder, M., Shankland, C.: A Symbolic Semantics and Bisimulation for Full LOTOS. In: Kim, M., Chin, B., Kang, S., Lee, D. (eds.) Proceedings of FORTE 2001, 21st International Conference on Formal Techniques for Networked and Distributed Systems, pp. 184–200. Kluwer Academic Publishers, Dordrecht (2001)
Calder, M., Maharaj, S., Shankland, C.: A Modal Logic for Full LOTOS based on Symbolic Transition Systems. The Computer Journal 45, 55–61 (2002)
Calder, M., Maharaj, S., Shankland, C.: An Adequate Logic for Full LOTOS. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 384–395. Springer, Heidelberg (2001)
Fernandez, J.C., Garavel, H., Kerbrat, A., Mateescu, R., Mounier, L., Sighireanu, M.: CADP (CAESAR/ALDEBARAN Development Package): A Protocol Validation and Verification Toolbox. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 437–440. Springer, Heidelberg (1996)
Mateescu, R., Garavel, H.: XTL: A Meta-Language and Tool for Temporal Logic Model-Checking. In: Proceedings of the International Workshop on Software Tools for Technology Transfer STTT 1998, Aalborg, Denmark (1998)
Mateescu, R., Sighireanu, M.: Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus. In: Proceedings of the 5th International Workshop on Formal Methods for Industrial Critical Systems FMICS 2000, Berlin, Germany (2000), Full version available as INRIA Research Report RR-3899
Cornejo, M.A., Garavel, H., Mateescu, R., de Palma, N.: Specification and Verification of a Dynamic Reconfiguration Protocol for Agent-Based Applications. Technical Report 4222, INRIA (2001)
Sighireanu, M., Mateescu, R.: Verification of the Link Layer Protocol of the IEEE- 1394 Serial Bus (FireWire): an Experiment with E-LOTOS. Springer International Journal on Software Tools for Technology Transfer (STTT) 2, 68–88 (1998)
Hennessy, M., Milner, R.: Algebraic Laws for Nondeterminism and Concurrency. Journal of the Association for Computing Machinery 32, 137–161 (1985)
Mateescu, R.: Vérification des propriétés temporelles des programmes parall‘eles. PhD thesis, Institut National Polytechnique de Grenoble (1998)
Hennessy, M., Lin, H.: Symbolic Bisimulations. Theoretical Computer Science 138, 353–389 (1995)
Eertink, H.: Simulation Techniques for the Validation of LOTOS Specifications. PhD thesis, University of Twente (1994)
Garavel, H., Lang, F.: NTIF: A General Symbolic Model for Communicating Sequential Processes with Data. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 276–291. Springer, Heidelberg (2002)
Spies, K., Merz, S., Broy, M. (eds.): Dagstuhl Seminar 1994. LNCS, vol. 1169. Springer, Heidelberg (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Shankland, C., Bryans, J., Morel, L. (2004). Expressing Iterative Properties Logically in a Symbolic Setting. In: Rattray, C., Maharaj, S., Shankland, C. (eds) Algebraic Methodology and Software Technology. AMAST 2004. Lecture Notes in Computer Science, vol 3116. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27815-3_35
Download citation
DOI: https://doi.org/10.1007/978-3-540-27815-3_35
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22381-8
Online ISBN: 978-3-540-27815-3
eBook Packages: Springer Book Archive