| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Formalization of Refinement Calculus for Reactive Systems
| Title: | Formalization of Refinement Calculus for Reactive Systems |
| Author: | Viorel Preoteasa (viorel /dot/ preoteasa /at/ aalto /dot/ fi) |
| Submission date: | 2014-10-08 |
| Abstract: | We present a formalization of refinement calculus for reactive systems. Refinement calculus is based on monotonic predicate transformers (monotonic functions from sets of post-states to sets of pre-states), and it is a powerful formalism for reasoning about imperative programs. We model reactive systems as monotonic property transformers that transform sets of output infinite sequences into sets of input infinite sequences. Within this semantics we can model refinement of reactive systems, (unbounded) angelic and demonic nondeterminism, sequential composition, and other semantic properties. We can model systems that may fail for some inputs, and we can model compatibility of systems. We can specify systems that have liveness properties using linear temporal logic, and we can refine system specifications into systems based on symbolic transitions systems, suitable for implementations. |
| BibTeX: |
@article{RefinementReactive-AFP,
author = {Viorel Preoteasa},
title = {Formalization of Refinement Calculus for Reactive Systems},
journal = {Archive of Formal Proofs},
month = oct,
year = 2014,
note = {\url{https://isa-afp.org/entries/RefinementReactive.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |