Refinement mappings are used to prove that a lower-level specification correctly implements
a higher-level one. We consider specifications consisting of a state machine (which may be …

This book is about the verification of reactive systems. A reactive system is a system that
maintains an ongoing interaction with its environment, as opposed to computing some final …

A unified, comprehensive presentation of simulation techniques for verification of concurrent
systems is given, in terms of a simple untimed automaton model. In particular,(1) …

The goal of this book is to provide a comprehensive and systematic introduction to the
important and highly applicable method of data refinement and the simulation methods used …

It is shown how to apply the refinement calculus to stepwise refinement of both parallel
programs and reactive programs. The approach is based on using the action systems model …

A general automaton model for timing-based systems is presented and is used as the
context for developing a variety of simulation proof techniques for such systems. As a first …

In spite of the impressive progress in the development of the two main methods for formal
verification of reactive systems–Symbolic Model Checking and Deductive Verification, they …

We present a method for specification and verification of distributed systems that
communicate via asynchronous message passing. The method handles both safety and …

A syntax-directed formal system for the development of totally correct programs with respect
to an unfair shared-state parallel while-language is proposed. The system can be …

In the stepwise development of a distributed system, the problem arises of verifying that a
specification at a lower level of abstraction correctly implements a specification at a higher …