Theorem-Proving Analysis of Digital Control Logic Interacting with Continuous Dynamics
Autor: | Geoffrey C. Hulette, Robert C. Armstrong, Joseph. R. Ruthruff, Jackson R. Mayo |
---|---|
Rok vydání: | 2015 |
Předmět: |
Theoretical computer science
formal methods General Computer Science Computer science Dissipation Decision problem Formal methods hybrid systems cyber-physical systems Thermostat Formal proof law.invention Theoretical Computer Science Causality (physics) Automated theorem proving theorem proving law Hybrid system Digital control Computer Science(all) |
Zdroj: | Electronic Notes in Theoretical Computer Science. 317:71-83 |
ISSN: | 1571-0661 |
DOI: | 10.1016/j.entcs.2015.10.008 |
Popis: | This work outlines an equation-based formulation of a digital control program and transducer interacting with a continuous physical process, and an approach using the Coq theorem prover for verifying the performance of the combined hybrid system. Considering thermal dynamics with linear dissipation for simplicity, we focus on a generalizable, physically consistent description of the interaction of the real-valued temperature and the digital program acting as a thermostat. Of interest in this work is the discovery and formal proof of bounds on the temperature, the degree of variation, and other performance characteristics. Our approach explicitly addresses the need to mathematically represent the decision problem inherent in an analog-to-digital converter, which for rare values can take an arbitrarily long time to produce a digital answer (the so-called Buridan's Principle); this constraint ineluctably manifests itself in the verification of thermostat performance. Furthermore, the temporal causality constraints in the thermal physics must be made explicit to obtain a consistent model for analysis. We discuss the significance of these findings toward the verification of digital control for more complex physical variables and fields. |
Databáze: | OpenAIRE |
Externí odkaz: |