# Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic

## TL;DR

This paper introduces a modular framework within differential dynamic logic for modeling and verifying computer-controlled hybrid systems, emphasizing parallel composition and timing guarantees to facilitate safety proofs.

## Contribution

It develops a component-based approach in differential dynamic logic that enables modular modeling and automated safety verification of parallel, timing-critical hybrid systems.

## Key findings

- Framework supports parallel component composition with timing guarantees
- Automated safety proofs derived from modular component properties
- Applicable to safety-critical computer-controlled systems

## Abstract

Computer-Controlled Systems (CCS) are a subclass of hybrid systems where the periodic relation of control components to time is paramount. Since they additionally are at the heart of many safety-critical devices, it is of primary importance to correctly model such systems and to ensure they function correctly according to safety requirements. Differential dynamic logic $d\mathcal{L}$ is a powerful logic to model hybrid systems and to prove their correctness. We contribute a component-based modeling and reasoning framework to $d\mathcal{L}$ that separates models into components with timing guarantees, such as reactivity of controllers and controllability of continuous dynamics. Components operate in parallel, with coarse-grained interleaving, periodic execution and communication. We present techniques to automate system safety proofs from isolated, modular, and possibly mechanized proofs of component properties parameterized with timing characteristics.