A model and temporal proof system for networks of processes
An approach is presented for modeling networks of processes that communicate exclusively through message passing. A process (or a network) is defined by its set of possible behaviors, where each behavior is an abstraction of an infinite execution sequence of the process. The resulting model is simple and modular and facilitates information hiding. It can describe both synchronous and asynchronous networks. It supports recursively-defined networks and can characterize liveness properties such as progress of inputs and outputs, termination, and deadlock. A sound and complete temporal proof system based on the model is presented. It is compositional - a specification of a network is formed naturally from specifications of its components.
- A calculus of communicating systems
- A proof technique for communicating sequential processes
- scientific article; zbMATH DE number 3980467 (Why is no real title available?)
- scientific article; zbMATH DE number 3755842 (Why is no real title available?)
- scientific article; zbMATH DE number 3469994 (Why is no real title available?)
- scientific article; zbMATH DE number 3566181 (Why is no real title available?)
- scientific article; zbMATH DE number 3566182 (Why is no real title available?)
- scientific article; zbMATH DE number 1461825 (Why is no real title available?)
- Proofs of Networks of Processes
- Ten Years of Hoare's Logic: A Survey—Part I
- The incompleteness of Misra and Chandy's proof systems
- A multiprocess network logic with temporal and spatial modalities
- An operator net model for distributed systems
- A compositional axiomatization of statecharts
- An experience in proving regular networks of processes by modular model checking
- A fully abstract trace model for dataflow and asynchronous networks
- Model-100: specification language for interacting processes
- scientific article; zbMATH DE number 1617289 (Why is no real title available?)
- scientific article; zbMATH DE number 3862445 (Why is no real title available?)
- scientific article; zbMATH DE number 3890715 (Why is no real title available?)
- scientific article; zbMATH DE number 3938554 (Why is no real title available?)
- scientific article; zbMATH DE number 3956416 (Why is no real title available?)
- scientific article; zbMATH DE number 3980467 (Why is no real title available?)
- A new look at the delay network model of program behaviour
- scientific article; zbMATH DE number 4056975 (Why is no real title available?)
- TTL : a formalism to describe local and global properties of distributed systems
- scientific article; zbMATH DE number 139998 (Why is no real title available?)
- scientific article; zbMATH DE number 591003 (Why is no real title available?)
- Towards a complete hierarchy of compositional dataflow models
- Abstract switches: a distributed model of communication and computation
- An introduction to compositional methods for concurrency and their application to real-time.
- Automated temporal reasoning about reactive systems
- The need for compositional proof systems: a survey
This page was built for publication: A model and temporal proof system for networks of processes
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1079948)
