English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

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.

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