Abstract
LOTOS is a Formal Description Technique developed within ISO to specify services and protocols. This paper describes a tool for doing LOTOS to LOTOS transformations. It has applications in state exploration, deadlock detection, testing, validation and in design by stepwise refinement. The transformations are: expansion (transformation of parallelism into summation and prefix); parameterized expansion; i action removal. The transformations obtain LOTOS specifications which relate to the original one through strong (expansion and parameterized expansion) or weak (i-action removal) bisimulation congruence.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
E. Brinksma, G. Scollo, and C. Steenbergen. LOTOS Specifications, Their Implementation and Their Tests. In Sixth International Workshop on Protocol Specification, Testing and Verification, Montreal, June 1986.
H. Ehrig, W. Fey, and H. Hansen. ACT ONE: An Algebraic Language with two Levels of Semantics. Technical Report, Tech. Universitat Berlin, 1983.
R. Foorgard. Reve-A Program for Generating and Analyzing Term Rewriting Systems. Technical Report MIT/LCS/TR-343, September 1984.
ISO. LOTOS a Formal Description Technique based on the Temporal Ordering of Observational Behaviour. IS 8807, TC97/SC21, 1989.
D. Frutos J. Quemada, A. Azcorra. A Timed Calculus for LOTOS. Technical Report, March 1989.
R. Milner. A Calculus of Communicating Systems. Springer-Verlag, Berlin, 1980.
R. Nicola and Hennessy, M.C.B. Testing Equivalences for Processes. Theoretical Computer Science, 34(1,2):83–133, Nov 1984.
J. Quemada, A. Fernandez, and J.A. Manas. LOLA: Design and Verification of Protocols using LOTOS. Ibericom, Conf. on Data Communications, Lisbon, May 1987.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Quemada, J., Pavón, S., Fernández, A. (1990). State exploration by transformation with lola. In: Sifakis, J. (eds) Automatic Verification Methods for Finite State Systems. CAV 1989. Lecture Notes in Computer Science, vol 407. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52148-8_25
Download citation
DOI: https://doi.org/10.1007/3-540-52148-8_25
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52148-8
Online ISBN: 978-3-540-46905-6
eBook Packages: Springer Book Archive