Stepwise Refinement of Distributed Systems

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.- 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.