Automated machine-checked hybrid system safety proofs
| Autor: | Kaufmann, M., Paulson, L., Geuvers, H., Koprowski, A., Synek, D., Weegen, E.E. van der |
|---|---|
| Přispěvatelé: | Formal System Analysis |
| Jazyk: | angličtina |
| Rok vydání: | 2010 |
| Předmět: |
Theoretical computer science
Computer science Programming language Computation Data Science Classical logic 0102 computer and information sciences 02 engineering and technology computer.software_genre Mathematical proof Monad (functional programming) 01 natural sciences Constructive Decidability 010201 computation theory & mathematics Reachability Hybrid system TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS 0202 electrical engineering electronic engineering information engineering Double negation Lecture Notes in Computer Science 020201 artificial intelligence & image processing Hybrid automaton computer |
| Zdroj: | Interactive Theorem Proving ISBN: 9783642140518 ITP Lecture Notes in Computer Science ; 6172, 259-274. Berlin / Heidelberg : Springer STARTPAGE=259;ENDPAGE=274;TITLE=Lecture Notes in Computer Science ; 6172 Interactive Theorem Proving, pp. 259-274 Interactive Theorem Proving (First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings), 259-274 STARTPAGE=259;ENDPAGE=274;TITLE=Interactive Theorem Proving (First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings) |
| Popis: | We have developed a hybrid system safety prover, implemented in Coq using the abstraction method introduced by [2]. The development includes: a formalisation of the structure of hybrid systems; a framework for the construction of an abstract system (consisting of decidable “over-estimators” of abstract transitions and initiality) faithfully representing a concrete hybrid system; a translation of abstract systems to graphs, enabling the decision of abstract state reachability using a certified graph reachability algorithm; a proof of the safety of an example hybrid system generated using this tool stack. To produce fully certified safety proofs without relying on floating point computations, the development critically relies on the computable real number implementation of the CoRN library of constructive mathematics formalised in Coq. The development also features a nice interplay between constructive and classical logic via the double negation monad. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|