Abstract
We present a partial solution to the Dagstuhl RPC-Memory Specification Problem which is carried out in linear-time temporal logic (LTL). Our language is quite similar to TLA (Temporal Logic of Actions) by Lamport. However, our use of this language provides some (in our opinion) interesting novelties. A major contribution of this paper is in our opinion a demonstration of different structuring mechanisms that exist in LTL. We use flexible predicates to represent synchronizing events, as in e.g., LOTOS, that serve for communication between components. In the specification of a component, the central part is a set of formulas that for each state variable states the constraints under which it may change, and for each event states the constraints (in terms of state changes) under which it may occur. We define a graphical syntax for parts of a temporal logic specification that involve “control”.
This contribution contains solutions to the specification problems, except for the timing extension, i.e., we solve Problem 1, 2 and 3 except for the verification parts which is only briefly covered.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi, L. Lamport, and S. Merz. A TLA Solution to the RPC-Memory Specification Problem. This volume.
J. Blom, B. Jonsson, and L. Kempe. Using temporal logic for modular specification of telephone services. In L. G. Bouma and Hugo Velthuijsen, editors, Feature Interactions in Telecommunications Systems, pages 197–216, Amsterdam, The Netherlands, May 1994. IOS Press.
A. Borgida, J. Mylopoulos, and R. Reiter. On the frame problem in procedure specifications. IEEE Trans. on Software Engineering, 21(10):785–798, 1995.
M. Broy and L. Lamport. The RPC-Memory Specification Problem. This volume.
L. Lamport. Lake arrowhead specification problem, 1987. Manuscript.
L. Lamport. The temporal logic of actions. Technical report, DEC/SRC, 1991.
K. G. Larsen, B. Steffen, and C. Weise. The Methodology of Modal Constraints. This volume.
N. Lynch and M.R. Tuttle. An Introduction to Input/Output Automata. Technical Report MIT/LCS/TM-373, MIT, Nov. 1988. TM-351 Revised.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer Verlag, 1992.
J.L. Peterson. Petri nets. Computing Surveys, 9(3):221–252, 1977.
P.H.J. van Eijk, C.A. Vissers, and M. Diaz, editors. The Formal Description Technique LOTOS. North-Holland, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Blom, J., Jonsson, B. (1996). Constraint oriented temporal logic specification. In: Broy, M., Merz, S., Spies, K. (eds) Formal Systems Specification. Lecture Notes in Computer Science, vol 1169. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0024429
Download citation
DOI: https://doi.org/10.1007/BFb0024429
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61984-0
Online ISBN: 978-3-540-49573-4
eBook Packages: Springer Book Archive