NDLI: Compositional specification and verification of distributed systems

Content Provider	ACM Digital Library
Author	Jonsson, Bengt
Copyright Year	1994
Abstract	We present a method for specification and verification of distributed systems that communicate via asynchronous message passing. The method handles both safety and liveness properties. It is compositional, i.e., a specification of a composite system can be obtained from specifications of its components. Specifications are given as labeled transition systems with fairness properties, using a program-like notation with guarded multiple assignments. Compositionality is attained by partitioning the labels of a transition system into input events, which intuitively denote message receptions, and output events, which intuitively denote message transmissions. A specification denotes a set of allowed sequences of message transmissions and receptions, in analogy with the way finite automata are used as acceptors of finite strings. A lower-level specification implements a higher-level one. We present a verification technique which reduces the problem of verifying the correctness of an implementation to classical verification conditions. Safety properties are verified by establishing a simulation relation between transition systems. Liveness properties are verified using methods for proving termination under fairness assumptions. Since specifications can be given at various levels of abstraction, the method is suitable in a development process where a detailed implementation is developed from an abstract specification through a sequence of refinement steps. As an application of the method, an algorithm by Thomas for updating a distributed database is specified and verified.
Starting Page	259
Ending Page	303
Page Count	45
File Format	PDF
ISSN	01640925
e-ISSN	15584593
DOI	10.1145/174662.174665
Volume Number	16
Issue Number	2
Journal	ACM Transactions on Programming Languages and Systems (TOPLAS)
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1994-03-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Assertional reasoning Compositionality Message passing Modular specification Specification Stepwise refinement
Content Type	Text
Resource Type	Article
Subject	Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

A stepwise refinement heuristic for protocol construction

Modular specification and verification of object-oriented programs

Bounded phase analysis of message-passing programs

Modular refinement of hierarchic reactive machines

[9] J. Hooman and W.P. de Roever. Verification and specification of concurrent programs.

Real-time specifications

Temporal specification and verification of reactive modules (1992).

Constructing formal rules to verify message communication in distributed systems

Behavioral Subtyping, Specification Inheritance, and Modular Reasoning

Compositional specification and verification of distributed systems

Similar Documents

A stepwise refinement heuristic for protocol construction

Modular specification and verification of object-oriented programs

Bounded phase analysis of message-passing programs

Modular refinement of hierarchic reactive machines

[9] J. Hooman and W.P. de Roever. Verification and specification of concurrent programs.

Real-time specifications

Temporal specification and verification of reactive modules (1992).

Constructing formal rules to verify message communication in distributed systems

Behavioral Subtyping, Specification Inheritance, and Modular Reasoning

Compositional specification and verification of distributed systems