Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic
| Autor: | Lunel, Simon, Mitsch, Stefan, Boyer, Benoit, Talpin, Jean-Pierre |
|---|---|
| Rok vydání: | 2019 |
| Předmět: | |
| Druh dokumentu: | Working Paper |
| Popis: | 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. Comment: Long version of an article accepted to the conference FM'19 |
| Databáze: | arXiv |
| Externí odkaz: |
|