Ebook: Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness: REX Workshop, Mook, The Netherlands May 29 – June 2, 1989 Proceedings

The stepwise refinement method postulates a system construction route that starts with a high-level specification, goes through a number of provably correct development steps, and ends with an executable program. The contributions to this volume survey the state of the art in this extremely active research area. The world's leading specialists in concurrent program specification, verification, and the theory of their refinement present latest research results and surveys of the fields. State-based, algebraic, temporal logic oriented and category theory oriented approaches are presented. Special attention is paid to the relationship between compositionality and refinement for distributed programs. Surveys are given of results on refinement in partial-order based approaches to concurrency. A unified treatment is given of the assumption/commitment paradigm in compositional concurrent program specification and verification, and the extension of these to liveness properties. Latest results are presented on specifying and proving concurrent data bases correct, and deriving network protocols from their specifications.

---

The stepwise refinement method postulates a system construction route that starts with a high-level specification, goes through a number of provably correct development steps, and ends with an executable program. The contributions to this volume survey the state of the art in this extremely active research area. The world's leading specialists in concurrent program specification, verification, and the theory of their refinement present latest research results and surveys of the fields. State-based, algebraic, temporal logic oriented and category theory oriented approaches are presented. Special attention is paid to the relationship between compositionality and refinement for distributed programs. Surveys are given of results on refinement in partial-order based approaches to concurrency. A unified treatment is given of the assumption/commitment paradigm in compositional concurrent program specification and verification, and the extension of these to liveness properties. Latest results are presented on specifying and proving concurrent data bases correct, and deriving network protocols from their specifications.

---

The stepwise refinement method postulates a system construction route that starts with a high-level specification, goes through a number of provably correct development steps, and ends with an executable program. The contributions to this volume survey the state of the art in this extremely active research area. The world's leading specialists in concurrent program specification, verification, and the theory of their refinement present latest research results and surveys of the fields. State-based, algebraic, temporal logic oriented and category theory oriented approaches are presented. Special attention is paid to the relationship between compositionality and refinement for distributed programs. Surveys are given of results on refinement in partial-order based approaches to concurrency. A unified treatment is given of the assumption/commitment paradigm in compositional concurrent program specification and verification, and the extension of these to liveness properties. Latest results are presented on specifying and proving concurrent data bases correct, and deriving network protocols from their specifications.
Content:
Front Matter....Pages -
Composing specifications....Pages 1-41
Refinement calculus, part I: Sequential nondeterministic programs....Pages 42-66
Refinement calculus, part II: Parallel and reactive programs....Pages 67-93
MetateM: A framework for programming in temporal logic....Pages 94-129
Constraint-oriented specification in a constructive formal description technique....Pages 130-152
Functional specification of time sensitive communicating systems....Pages 153-179
Modular verification of Petri Nets....Pages 180-207
Abadi & Lamport and stark: Towards a proof theory for stuttering, dense domains and refinement mappings....Pages 208-238
Algebraic implementation of objects over objects....Pages 239-266
Refinement of actions in causality based models....Pages 267-300
Transformation of combined data type and process specifications using projection algebras....Pages 301-339
Various simulations and refinements....Pages 340-360
On decomposing and refining specifications of distributed systems....Pages 361-385
Verifying the correctness of AADL modules using model checking....Pages 386-400
Specialization in logic programming: From horn clause logic to prolog and concurrent prolog....Pages 401-413
Analysis of discrete event coordination....Pages 414-453
Refinement and projection of relational specifications....Pages 454-486
Compositional theories based on an operational semantics of contexts....Pages 487-518
Multivalued possibilities mappings....Pages 519-543
Completeness theorems for automata....Pages 544-560
Formal verification of data type refinement — Theory and practice....Pages 561-591
From trace specifications to process terms....Pages 592-621
Some comments on the assumption-commitment framework for compositional verification of distributed programs....Pages 622-640
Refinement of concurrent systems based on local state transformations....Pages 641-668
Construction of network protocols by stepwise refinement....Pages 669-695
A derivation of a broadcasting protocol using sequentially phased reasoning....Pages 696-730
Verifying atomic data types....Pages 731-758
Predicates, predicate transformers and refinement....Pages 759-776
Foundations of compositional program refinement....Pages 777-807
Back Matter....Pages -

---

The stepwise refinement method postulates a system construction route that starts with a high-level specification, goes through a number of provably correct development steps, and ends with an executable program. The contributions to this volume survey the state of the art in this extremely active research area. The world's leading specialists in concurrent program specification, verification, and the theory of their refinement present latest research results and surveys of the fields. State-based, algebraic, temporal logic oriented and category theory oriented approaches are presented. Special attention is paid to the relationship between compositionality and refinement for distributed programs. Surveys are given of results on refinement in partial-order based approaches to concurrency. A unified treatment is given of the assumption/commitment paradigm in compositional concurrent program specification and verification, and the extension of these to liveness properties. Latest results are presented on specifying and proving concurrent data bases correct, and deriving network protocols from their specifications.
Content:
Front Matter....Pages -
Composing specifications....Pages 1-41
Refinement calculus, part I: Sequential nondeterministic programs....Pages 42-66
Refinement calculus, part II: Parallel and reactive programs....Pages 67-93
MetateM: A framework for programming in temporal logic....Pages 94-129
Constraint-oriented specification in a constructive formal description technique....Pages 130-152
Functional specification of time sensitive communicating systems....Pages 153-179
Modular verification of Petri Nets....Pages 180-207
Abadi & Lamport and stark: Towards a proof theory for stuttering, dense domains and refinement mappings....Pages 208-238
Algebraic implementation of objects over objects....Pages 239-266
Refinement of actions in causality based models....Pages 267-300
Transformation of combined data type and process specifications using projection algebras....Pages 301-339
Various simulations and refinements....Pages 340-360
On decomposing and refining specifications of distributed systems....Pages 361-385
Verifying the correctness of AADL modules using model checking....Pages 386-400
Specialization in logic programming: From horn clause logic to prolog and concurrent prolog....Pages 401-413
Analysis of discrete event coordination....Pages 414-453
Refinement and projection of relational specifications....Pages 454-486
Compositional theories based on an operational semantics of contexts....Pages 487-518
Multivalued possibilities mappings....Pages 519-543
Completeness theorems for automata....Pages 544-560
Formal verification of data type refinement — Theory and practice....Pages 561-591
From trace specifications to process terms....Pages 592-621
Some comments on the assumption-commitment framework for compositional verification of distributed programs....Pages 622-640
Refinement of concurrent systems based on local state transformations....Pages 641-668
Construction of network protocols by stepwise refinement....Pages 669-695
A derivation of a broadcasting protocol using sequentially phased reasoning....Pages 696-730
Verifying atomic data types....Pages 731-758
Predicates, predicate transformers and refinement....Pages 759-776
Foundations of compositional program refinement....Pages 777-807
Back Matter....Pages -
....