Specifying Concurrent Program Modules

ACM Transactions on Programming Languages and SystemsPublished 1 April 1983Open access

Leslie Lamport

DOI10.1145/69624.357207

Source URL

Citations524

SJR quartileQ2

SJR score0.56

SNIP1.52

View PDF

TL;DR

A method for specifying program modules in a concurrent program is described, based upon temporal logic, but uses new kinds of temporal assertions to make the specifications simpler and easier to understand.

Abstract

article Free AccessSpecifying Concurrent Program Modules Author: Leslie Lamport Computer Science Laboratory, SRI International, 333 Ravenswood Avenue, Menlo Park, CA Computer Science Laboratory, SRI International, 333 Ravenswood Avenue, Menlo Park, CAView Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 5Issue 2April 1983 pp 190–222https://doi.org/10.1145/69624.357207Published:01 April 1983Publication History 396citation1,279DownloadsMetricsTotal Citations396Total Downloads1,279Last 12 Months82Last 6 weeks2 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

Keywords

Computer Science

The temporal logic of programs

5,586 Citations1977Amir Pnueli

A unified approach to program verification is suggested, which applies to both sequential and parallel programs, and the main proof method is that of temporal reasoning in which the time dependence of events is the basic concept.

ACM Transactions on Programming Languages and SystemsProving Liveness Properties of Concurrent Programs

583 Citations1982Susan Owicki, Leslie Lamport

A formal proof method, based on temporal logic, for deriving liveness properties is presented, which allows a rigorous formulation of simple informal arguments and how to reason with temporal logic and use safety (invariance) properties in proving liveness is shown.

View PDF

Communications of the ACMConcurrent reading and writing

280 Citations1977Leslie Lamport

Two general theorems are proved, and some algorithms are presented to illustrate their use, including a solution to the general problem in which a read is repeated if it might have obtained an incorrect result, and two techniques for transmitting messages between processes.

View PDF

IRE Transactions on Communications SystemsFormal Methods in Communication Protocol Design

221 Citations1980Gregor von Bochmann, Carl A. Sunshine

This paper surveys the formal methods being applied to the problems of protocol specification, verification, and implementation, including state transition models, program verification, symbolic execution, and design rules.

Acta InformaticaThe ?Hoare logic? of concurrent programs

181 Citations1980Leslie Lamport

Hoare's logical system for specifying and proving partial correctness properties of sequential programs is generalized to concurrent programs and it is shown that by specifying certain requirements for the unimplemented parts, correctness properties can be proved without completely implementing the program.

Lecture notes in computer scienceFrom state machines to temporal logic: Specification methods for protocol standards

90 Citations1985Richard L. Schwartz, P. M. Melliar‐Smith

The paper characterizes specification languages such as state transition diagrams, variants of temporal logic approaches, and sequence expressions by the extent to Which information is encoded as properties of a single state versus properties ofa history of the entire computation state sequence.

International Conference on Distributed Computing SystemsTemporal Logic Specification of Distributed Systems.

59 Citations1981Richard L. Schwartz, P. M. Melliar‐Smith

In selected patients with locally advanced LSCC, VATS played a positive role in postoperative recovery and associated similar survival outcome compared with thoracotomy after neoadjuvant chemotherapy.

Verifying network protocols using temporal logic

57 Citations1980Brent Hailpern, Susan Owicki

This paper discusses the application of program verification techniques to protocols and presents tools of concurrent program verification that are especially useful for protocols: history variables that record sequences of input and output values, temporal logic for expressing properties that must hold in a future system state, and module specification and composition rules.