Stepwise Refinement of Distributed Systems : Models, Formalisms, Correctness. REX Workshop, Mook, The Netherlands, May 29 - June 2, 1989. Proceedings. 1st ed. 1990

種類:

電子ブック

責任表示:

edited by Jaco W. de Bakker, Willem-Paul de Roever, Grzegorz Rozenberg

出版情報:

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 1990

著者名:

• Bakker, Jaco W. de.
• Roever, Willem-Paul de.
• Rozenberg, Grzegorz.
• SpringerLink (Online service)

シリーズ名:

Lecture Notes in Computer Science ; 430

ISBN:

9783540470359 [3540470352]    

注記:

Composing specifications -- Refinement calculus, part I: Sequential nondeterministic programs -- Refinement calculus, part II: Parallel and reactive programs -- MetateM: A framework for programming in temporal logic -- Constraint-oriented specification in a constructive formal description technique -- Functional specification of time sensitive communicating systems -- Modular verification of Petri Nets -- Abadi & Lamport and stark: Towards a proof theory for stuttering, dense domains and refinement mappings -- Algebraic implementation of objects over objects -- Refinement of actions in causality based models -- Transformation of combined data type and process specifications using projection algebras -- Various simulations and refinements -- On decomposing and refining specifications of distributed systems -- Verifying the correctness of AADL modules using model checking -- Specialization in logic programming: From horn clause logic to prolog and concurrent prolog -- Analysis of discrete event coordination --
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 specify

ローカル注記:

岐阜大学構成員専用E-BOOKS (Gifu University members only)