TY - BOOK ID - 2394122 TI - Stepwise refinement of distributed systems : models, formalisms, correctness AU - de Bakker, J. W. AU - de Roever, Willem P. PY - 1990 VL - 430 SN - 0387525599 3540525599 3540470352 PB - Berlin Springer DB - UniCat KW - Electronic data processing KW - Traitement réparti KW - Distributed processing KW - Congresses KW - Congrès KW - -681.3*D13 KW - 681.3*F3 KW - ADP (Data processing) KW - Automatic data processing KW - Data processing KW - EDP (Data processing) KW - IDP (Data processing) KW - Integrated data processing KW - Computers KW - Office practice KW - Concurrent programming KW - Logics and meanings of programs (Theory of computation) KW - Automation KW - 681.3*F3 Logics and meanings of programs (Theory of computation) KW - 681.3*D13 Concurrent programming KW - Traitement réparti KW - Congrès KW - 681.3*D13 KW - Distributed processing&delete& KW - Computer network architectures. KW - Logic design. KW - Computer science. KW - Computer Communication Networks. KW - Computer System Implementation. KW - Logics and Meanings of Programs. KW - Programming Techniques. KW - Informatics KW - Science KW - Design, Logic KW - Design of logic systems KW - Digital electronics KW - Electronic circuit design KW - Logic circuits KW - Machine theory KW - Switching theory KW - Architectures, Computer network KW - Network architectures, Computer KW - Computer architecture UR - https://www.unicat.be/uniCat?func=search&query=sysid:2394122 AB - 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. ER -