Conjoining specifications
ACM Transactions on Programming Languages and SystemsPublished 1 May 1995Open access
Martı́n Abadi, Leslie Lamport
Citations451
SJR quartileQ2
SJR score0.56
SNIP1.52
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
It is shown how to specify components of concurrent systems and considers both the decomposition of a given system into parts, and the composition of given parts to form a system.
Abstract
We show how to specify components of concurrent systems. The specification of a system is the conjunction of its components' specifications. Properties of the system are proved by reasoning about its components. We consider both the decomposition of a given system into parts, and the composition of given parts to form a system.
Keywords
Computer Science
Information Processing LettersDefining liveness
1,025 Citations1985Bowen Alpern, Fred B. Schneider
A formal definition for liveness properties is proposed, and every property is shown to be the intersection of a safety property and a liveness property.
Theoretical Computer ScienceThe existence of refinement mappings
734 Citations1991Martı́n Abadi, Leslie Lamport
The authors consider specifications consisting of a state machine that specifies safety requirements and an arbitrary supplementary property that specifies liveness requirements and show that under reasonable assumptions about the specifications, if S/ Sub 1/ implements S/sub 2/, then by adding auxiliary variables to S/ sub 1/ one can guarantee the existence of a refinement mapping.
Theoretical Computer ScienceThe temporal semantics of concurrent programs
701 Citations1981Amir Pnueli
It is demonstrated that specification of the Temporal character of the program's behavior is absolutely essential for the unambiguous understanding of the meaning of programming constructs.
IEEE Transactions on Software EngineeringProofs of Networks of Processes
497 Citations1981Jayadev Misra, K. Mani Chandy
The proof method is based upon specifying a process by a pair of assertions, analogous to pre-and post-conditions in sequential program proving, and the correctness of network specification is proven by applying inference rules to the specifications of component processes.
ACM Transactions on Programming Languages and SystemsComposing specifications
459 Citations1993Martı́n Abadi, Leslie Lamport
This work examines the precise distinction between a system and its environment, and provides the requisite proof rule when modules are specified with safety and liveness properties.
IFIP CongressWhat Good is Temporal Logic
444 Citations1983Leslie Lamport
This was an invited paper and describes the state of my views on specification and verification at the time, notable for introducing the idea of invariance under stuttering and explaining why it’s a vital attribute of a specification logic.
Journal of Symbolic LogicGames and full completeness for multiplicative linear logic
381 Citations1994Samson Abramsky, Radha Jagadeesan
It is shown that this semantics yields a categorical model of Linear Logic and proves full completeness for Multiplicative Linear Logic with the MIX rule: every winning strategy is the denotation of a unique cut-free proof net.
ACM Transactions on Programming Languages and SystemsAn old-fashioned recipe for real time
239 Citations1994Martı́n Abadi, Leslie Lamport
TLA (the temporal logic of actions) is illustrated how they work with the examples of a queue and of a mutual-exclusion protocol, and two problems must be addressed: avoiding the real-time programming version of Zeno's paradox, and coping with circularities when composing real- time assumption/guarantee specifications.
Communications of the ACMA simple approach to specifying concurrent systems
237 Citations1989Leslie Lamport
The transition axiom method provides a conceptual and logical foundation for writing formal specifications; it is not a specification language and is not meant as a paradigm for how systems should be built.
ACM Transactions on Software Engineering and MethodologyConjunction as composition
206 Citations1993Pamela Zave, Michael Jackson
The criteria for success are that a wide variety of specification languages should be accommodated, there should be no restrictions on where boundaries between languages can be placed, and intuitive expectations of the specifier should be met.
Lecture notes in computer scienceA proof technique for rely/guarantee properties
114 Citations1985Eugene W. Stark
This paper presents a proof technique that permits us to infer that a program P satisfies a rely/guarantee specification R ⊃ G, given that it satisfies a finite collection of rely/Guarantee specifications R i ⊁ G i.
Theoretical Computer ScienceA logical view of composition
82 Citations1993Martı́n Abadi, Gordon Plotkin
Two logics of safety specifications for reactive systems are defined; one of the logics is intuitionistic, while the other one is linear.
Lecture notes in computer scienceVerification of a multiplier: 64 bits and beyond
60 Citations1993Robert P. Kurshan, Leslie Lamport
This work shows how to verify a 64-bit multiplier by applying COSPAN, a model-checking algorithm, to verify local properties of the complex low-level circuit, and using TLP, a theorem prover based on the Temporal Logic of Actions, to prove that these properties imply the correctness of the multiplier.
Distributed ComputingP — A logic — a compositional proof system for distributed programs
53 Citations1991Partosh K. Pandya, Mathai Joseph
Proof rules for deriving some liveness properties of a program from its P-A logic specification are discussed; these properties have the form “Q untilR”, whereQ, R are assertions over communication traces.
Lecture notes in computer scienceApplication of the composition principle to unity-like specifications
28 Citations1993Pierre Collette
This paper interprets Unity formulas in Abadi and Lamport's compositional model, and reduces the premises of the composition rule to proof obligations that can be carried out in the existing Unity proof system.
IEEE Transactions on ComputersAn algebraic model for asynchronous circuits verification
16 Citations1988Christian Berthet, E. Cerny
An algebraic methodology for comparing switch-level circuits with higher-level specifications is presented, and is well suited for speed-independent circuits for which the specification is given as a collection of properties.