Automating the refinement of specifications for distributed systems via syntactic transformations

Paul Attie, Champak Das

Research output: Contribution to journalArticle

Abstract

The idea of successively refining an abstract specification until it contains enough detail to suggest an implementation has been investigated by numerous researchers. The emphasis to date has been on techniques that, unfortunately, lead to a large amount of manual formal labour for each refinement step. With such techniques, both the cost and the possibility of errors arising informal manipulation are high. Using a theorem prover can reduce the number of manipulation errors, but, given current technology, the amount of labour is still daunting. This research explores an alternative solution to the refinement problem, namely the use of syntactic transformations to realize each refinement step. We reduce formal labour by employing automatic transformations that guarantee the preservation of desirable properties—e.g., deadlock-freedom. Automatic transformations are particularly appealing for the development of large, complex distributed systems, where a manual approach to refinement would be prohibitively expensive. Distributed computations are, by nature, reactive and concurrent, so their correctness cannot be specified as a simple functional relationship between inputs and outputs. Instead, specifications must describe the time-varying behaviour of the system. Further difficulty is caused by the fact that such important characteristics of distributed systems as deadlock-freedom are global properties that cannot be achieved through considering local structures only. Transformations generally must encompass the entire system. This paper presents two syntactic transformations—the left-sequence introduction and the right-sequence introduction—and demonstrates that they preserve deadlock-freedom.

Original languageEnglish (US)
Pages (from-to)1129-1144
Number of pages16
JournalInternational Journal of Systems Science
Volume28
Issue number11
DOIs
StatePublished - Jul 1997
Externally publishedYes

Fingerprint

Syntactics
Distributed Systems
Deadlock
Refinement
Personnel
Specification
Specifications
Manipulation
Distributed Computation
Refining
Functional Relationship
Local Structure
Preservation
Concurrent
Complex Systems
Correctness
Time-varying
Entire
Syntax
Costs

ASJC Scopus subject areas

  • Control and Systems Engineering
  • Theoretical Computer Science
  • Computer Science Applications

Cite this

Automating the refinement of specifications for distributed systems via syntactic transformations. / Attie, Paul; Das, Champak.

In: International Journal of Systems Science, Vol. 28, No. 11, 07.1997, p. 1129-1144.

Research output: Contribution to journalArticle

@article{8795474de87e439e804d81690e47849f,
title = "Automating the refinement of specifications for distributed systems via syntactic transformations",
abstract = "The idea of successively refining an abstract specification until it contains enough detail to suggest an implementation has been investigated by numerous researchers. The emphasis to date has been on techniques that, unfortunately, lead to a large amount of manual formal labour for each refinement step. With such techniques, both the cost and the possibility of errors arising informal manipulation are high. Using a theorem prover can reduce the number of manipulation errors, but, given current technology, the amount of labour is still daunting. This research explores an alternative solution to the refinement problem, namely the use of syntactic transformations to realize each refinement step. We reduce formal labour by employing automatic transformations that guarantee the preservation of desirable properties—e.g., deadlock-freedom. Automatic transformations are particularly appealing for the development of large, complex distributed systems, where a manual approach to refinement would be prohibitively expensive. Distributed computations are, by nature, reactive and concurrent, so their correctness cannot be specified as a simple functional relationship between inputs and outputs. Instead, specifications must describe the time-varying behaviour of the system. Further difficulty is caused by the fact that such important characteristics of distributed systems as deadlock-freedom are global properties that cannot be achieved through considering local structures only. Transformations generally must encompass the entire system. This paper presents two syntactic transformations—the left-sequence introduction and the right-sequence introduction—and demonstrates that they preserve deadlock-freedom.",
author = "Paul Attie and Champak Das",
year = "1997",
month = "7",
doi = "10.1080/00207729708929473",
language = "English (US)",
volume = "28",
pages = "1129--1144",
journal = "International Journal of Systems Science",
issn = "0020-7721",
publisher = "Taylor and Francis Ltd.",
number = "11",

}

TY - JOUR

T1 - Automating the refinement of specifications for distributed systems via syntactic transformations

AU - Attie, Paul

AU - Das, Champak

PY - 1997/7

Y1 - 1997/7

N2 - The idea of successively refining an abstract specification until it contains enough detail to suggest an implementation has been investigated by numerous researchers. The emphasis to date has been on techniques that, unfortunately, lead to a large amount of manual formal labour for each refinement step. With such techniques, both the cost and the possibility of errors arising informal manipulation are high. Using a theorem prover can reduce the number of manipulation errors, but, given current technology, the amount of labour is still daunting. This research explores an alternative solution to the refinement problem, namely the use of syntactic transformations to realize each refinement step. We reduce formal labour by employing automatic transformations that guarantee the preservation of desirable properties—e.g., deadlock-freedom. Automatic transformations are particularly appealing for the development of large, complex distributed systems, where a manual approach to refinement would be prohibitively expensive. Distributed computations are, by nature, reactive and concurrent, so their correctness cannot be specified as a simple functional relationship between inputs and outputs. Instead, specifications must describe the time-varying behaviour of the system. Further difficulty is caused by the fact that such important characteristics of distributed systems as deadlock-freedom are global properties that cannot be achieved through considering local structures only. Transformations generally must encompass the entire system. This paper presents two syntactic transformations—the left-sequence introduction and the right-sequence introduction—and demonstrates that they preserve deadlock-freedom.

AB - The idea of successively refining an abstract specification until it contains enough detail to suggest an implementation has been investigated by numerous researchers. The emphasis to date has been on techniques that, unfortunately, lead to a large amount of manual formal labour for each refinement step. With such techniques, both the cost and the possibility of errors arising informal manipulation are high. Using a theorem prover can reduce the number of manipulation errors, but, given current technology, the amount of labour is still daunting. This research explores an alternative solution to the refinement problem, namely the use of syntactic transformations to realize each refinement step. We reduce formal labour by employing automatic transformations that guarantee the preservation of desirable properties—e.g., deadlock-freedom. Automatic transformations are particularly appealing for the development of large, complex distributed systems, where a manual approach to refinement would be prohibitively expensive. Distributed computations are, by nature, reactive and concurrent, so their correctness cannot be specified as a simple functional relationship between inputs and outputs. Instead, specifications must describe the time-varying behaviour of the system. Further difficulty is caused by the fact that such important characteristics of distributed systems as deadlock-freedom are global properties that cannot be achieved through considering local structures only. Transformations generally must encompass the entire system. This paper presents two syntactic transformations—the left-sequence introduction and the right-sequence introduction—and demonstrates that they preserve deadlock-freedom.

UR - http://www.scopus.com/inward/record.url?scp=0031268350&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0031268350&partnerID=8YFLogxK

U2 - 10.1080/00207729708929473

DO - 10.1080/00207729708929473

M3 - Article

AN - SCOPUS:0031268350

VL - 28

SP - 1129

EP - 1144

JO - International Journal of Systems Science

JF - International Journal of Systems Science

SN - 0020-7721

IS - 11

ER -