Abstract
Previous works on assumption/guarantee specifications typically reason about relevant properties at the semantic level or define a special-purpose logic. We feel it is beneficial to formulate such specifications in a more widely used formalism. Specifically, we adopt the lineartime temporal logic (LTL) of Manna and Pnueli. We find that, with past temporal operators, LTL admits a succinct syntactic formulation of assumption/guarantee specifications. This contrasts, in particular, with the work by Abadi and Lamport using TLA, where working at the syntactic level is more complicated. Our composition rules are derived entirely within LTL and can also handle internal variables. We had to overcome a number of technical problems in this pursuit, in particular, the problem of extracting the safety closure of a temporal formula. As a by-product, we identify general conditions under which the safety closure can be expressed in a succinct way that facilitates syntactic manipulation.
This work was supported in part by the Swedish Board for Industrial and Technical Development (NUTEK) as part of ESPRIT BRA project No. 6021 (REACT) and by the Swedish Research Council for Engineering Sciences (TFR).
The full paper is available as [11]; direct requests to {bengt, tsay}@docs.uu.se.
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
M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82:253–284, 1991.
M. Abadi and L. Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems, 15(1):73–132, January 1993.
M. Abadi and L. Lamport. Conjoining specifications. Technical Report 118, SRC DEC, 1993. Part of the paper appears in PODC '94 as “Open Systems in TLA”.
M. Abadi and G.D. Plotkin. A logical view of composition. Theoretical Computer Science, 114(1):3–30, June 1993.
B. Alpern and F.B. Schneider. Defining liveness. Information Processing Letters, 24(4):181–185, October 1985.
H. Barringer and R. Kuiper. Hierarchical development of concurrent systems in a temporal logic framework. In Seminar on Concurrency, LNCS 197, pages 35–61. Springer-Verlag, 1984.
P. Collette. Application of the composition principle to Unity-like specifications. In TAPSOFT '93, LNCS 668, pages 230–242. Springer-Verlag, 1993.
P. Collette. Design of Compositional Proof Systems Based on Assumption-Guarantee Specifications — Application to UNITY. PhD thesis, Université Catholique de Louvain, June 1994.
P. Grønning, T.Q. Nielsen, and H.H. Løvengreen. Refinement and composition of transition-based rely-guarantee specifications with auxiliary variables. In FST&TCS, LNCS 472, pages 332–348. Springer-Verlag, 1991.
C.B. Jones. Tentative steps towards a development method for interfering programs. ACM Transactions on Programming Languages and Systems, 5(4):596–619, October 1983.
B. Jonsson and Y.-K. Tsay. Assumption/guarantee specifications in linear-time temporal logic. Technical Report DoCS 95/58, Department of Computer Systems, Uppsala University, January 1995.
L. Lamport. What good is temporal logic? In R.E.A. Mason, editor, Information Processing 83, pages 657–668. IFIP, North-Holland, 1983.
L. Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, May 1994.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.
J. Misra and K.M. Chandy. Proofs of networks of processes. IEEE Transactions on Software Engineering, 7(4):417–426, July 1981.
A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13:45–60, 1982.
A. Pnueli. System specification and refinement in temporal logic. In FST&TCS, LNCS 652, pages 1–38. Springer-Verlag, 1992.
Q. Xu, A. Cau, and P. Collette. On unifying assumption-commitment style proof rules for concurrency. In CONCUR '94, LNCS 836, pages 267–282. Springer-Verlag, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jonsson, B., Tsay, YK. (1995). Assumption/guarantee specifications in linear-time temporal logic (extended abstract). In: Mosses, P.D., Nielsen, M., Schwartzbach, M.I. (eds) TAPSOFT '95: Theory and Practice of Software Development. CAAP 1995. Lecture Notes in Computer Science, vol 915. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59293-8_200
Download citation
DOI: https://doi.org/10.1007/3-540-59293-8_200
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59293-8
Online ISBN: 978-3-540-49233-7
eBook Packages: Springer Book Archive