Stepwise Refinement of Distributed Systems

1. Front Matter

   PDF

2. Composing specifications

   • Martín Abadi, Leslie Lamport

   Pages 1-41

3. Refinement calculus, part I: Sequential nondeterministic programs

   • R. J. R. Back, J. von Wright

   Pages 42-66

4. Refinement calculus, part II: Parallel and reactive programs

   • R. J. R. Back

   Pages 67-93

5. MetateM: A framework for programming in temporal logic

   • Howard Barringer, Michael Fisher, Dov Gabbay, Graham Gough, Richard Owens

   Pages 94-129

6. Constraint-oriented specification in a constructive formal description technique

   • Ed Brinksma

   Pages 130-152

7. Functional specification of time sensitive communicating systems

   • Manfred Broy

   Pages 153-179

8. Modular verification of Petri Nets

   • Werner Damm, Gert Döhmen, Volker Gerstner, Bernhard Josko

   Pages 180-207

9. Abadi & Lamport and stark: Towards a proof theory for stuttering, dense domains and refinement mappings

   • Eduard Diepstraten, Ruurd Kuiper

   Pages 208-238

10. Algebraic implementation of objects over objects

    • H. -D. Ehrich, A. Sernadas

    Pages 239-266

11. Refinement of actions in causality based models

    • Rob van Glabbeek, Ursula Goltz

    Pages 267-300

12. Transformation of combined data type and process specifications using projection algebras

    • M. Große-Rhode, H. Ehrig

    Pages 301-339

13. Various simulations and refinements

    • He Jifeng

    Pages 340-360

14. On decomposing and refining specifications of distributed systems

    • Bengt Jonsson

    Pages 361-385

15. Verifying the correctness of AADL modules using model checking

    • Bernhard Josko

    Pages 386-400

16. Specialization in logic programming: From horn clause logic to prolog and concurrent prolog

    • Joost N. Kok

    Pages 401-413

17. Analysis of discrete event coordination

    • R. P. Kurshan

    Pages 414-453

18. Refinement and projection of relational specifications

    • Simon S. Lam, A. Udaya Shankar

    Pages 454-486

19. Compositional theories based on an operational semantics of contexts

    • Kim Guldstrand Larsen

    Pages 487-518

20. Multivalued possibilities mappings

    • Nancy A. Lynch

    Pages 519-543

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.

• Ableitung
• Beweistheorie
• Verfeinerung
• automata
• distributed systems
• formal verification
• logic
• model checking
• petri net
• programming
• proof theory
• semantics
• verification
• verteiltes Datenverarbeitungssystem

Policies and ethics