Modular Design and Verification of Distributed Adaptive Real-Time Systems Based on Refinements and Abstractions

A promising way to cope with complexity in verifying large systems is to perform modular verification where components are verified separately. However, in the context of adaptive systems, it is difficult to apply this principle because adaptation behaviour and functional behaviour are often intertwined. In this paper, we present and apply a design pattern for distributed adaptive real-time systems using the process calculus Timed CSP. Our pattern explicitly differentiates between functional data and adaptive control data and thereby allows for a strict separation of adaptation and functional components. We enable the modular verification of functional and adaptation behaviour, respectively, based on the notion of process refinement in Timed CSP. The verification of refinements is automated using industrial-strength proof tools. As the notion of refinement can also be used to justify abstractions, we furthermore enable abstractionbased verification, where a detailed system is abstracted to facilitate more efficient verification efforts. This is especially important in the industrial development of adaptive systems using languages like SystemC where a designer not necessarily applies fine-grained refinements, but implements larger parts of the functional and adaptation logic possibly at the same time. Therefore, we discuss how common refinements and abstractions from the context of Timed CSP can be used as a formal basis for refinements and abstractions in SystemC.