LEADER 05731nam 22006735 450 001 996465626303316 005 20200705132411.0 010 $a3-540-47035-2 024 7 $a10.1007/3-540-52559-9 035 $a(CKB)1000000000233523 035 $a(SSID)ssj0000326915 035 $a(PQKBManifestationID)11231690 035 $a(PQKBTitleCode)TC0000326915 035 $a(PQKBWorkID)10297621 035 $a(PQKB)10925167 035 $a(DE-He213)978-3-540-47035-9 035 $a(PPN)155199005 035 $a(EXLCZ)991000000000233523 100 $a20121227d1990 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aStepwise Refinement of Distributed Systems$b[electronic resource] $eModels, Formalisms, Correctness. REX Workshop, Mook, The Netherlands, May 29 - June 2, 1989. Proceedings /$fedited by Jaco W. de Bakker, Willem-Paul de Roever, Grzegorz Rozenberg 205 $a1st ed. 1990. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d1990. 215 $a1 online resource (XII, 812 p.) 225 1 $aLecture Notes in Computer Science,$x0302-9743 ;$v430 300 $aBibliographic Level Mode of Issuance: Monograph 311 $a0-387-52559-9 311 $a3-540-52559-9 327 $aComposing 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 -- Refinement and projection of relational specifications -- Compositional theories based on an operational semantics of contexts -- Multivalued possibilities mappings -- Completeness theorems for automata -- Formal verification of data type refinement ? Theory and practice -- From trace specifications to process terms -- Some comments on the assumption-commitment framework for compositional verification of distributed programs -- Refinement of concurrent systems based on local state transformations -- Construction of network protocols by stepwise refinement -- A derivation of a broadcasting protocol using sequentially phased reasoning -- Verifying atomic data types -- Predicates, predicate transformers and refinement -- Foundations of compositional program refinement. 330 $aThe 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. 410 0$aLecture Notes in Computer Science,$x0302-9743 ;$v430 606 $aArchitecture, Computer 606 $aComputer logic 606 $aComputer programming 606 $aComputer communication systems 606 $aComputer System Implementation$3https://scigraph.springernature.com/ontologies/product-market-codes/I13057 606 $aLogics and Meanings of Programs$3https://scigraph.springernature.com/ontologies/product-market-codes/I1603X 606 $aProgramming Techniques$3https://scigraph.springernature.com/ontologies/product-market-codes/I14010 606 $aComputer Communication Networks$3https://scigraph.springernature.com/ontologies/product-market-codes/I13022 615 0$aArchitecture, Computer. 615 0$aComputer logic. 615 0$aComputer programming. 615 0$aComputer communication systems. 615 14$aComputer System Implementation. 615 24$aLogics and Meanings of Programs. 615 24$aProgramming Techniques. 615 24$aComputer Communication Networks. 676 $a004/.36 702 $aBakker$b Jaco W. de$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aRoever$b Willem-Paul de$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aRozenberg$b Grzegorz$4edt$4http://id.loc.gov/vocabulary/relators/edt 906 $aBOOK 912 $a996465626303316 996 $aStepwise Refinement of Distributed Systems$92831606 997 $aUNISA