A CSP-based framework for the specification, verification, and implementation of adaptive systems

Abstract

The process algebra CSP is tailored for the specification and verification of reactive systems. Such systems react upon external stimuli by adjusting their internal behavior, e.g., to recover from errors. Adaptive systems can be regarded as a subclass of reactive systems in the sense that such systems react by adapting to changes propagated by some stimulus. In this paper, we use CSP for the specification, verification and implementation of adaptive systems. This enables us to use standard CSP tools such as FDR, ProB or the CSP-Prover for the verification of such systems. Furthermore, we present an approach for the implementation of systems specified in CSP.