LIPIcs.CALCO.2019.17.pdf
- Filesize: 444 kB
- 10 pages
Document
Hybridisation of Institutions in HETS (Tool Paper)
Author
Mihai Codescu 
-
Part of:
Volume:
8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Conference on Algebra and Coalgebra in Computer Science (CALCO) - License:
Creative Commons Attribution 3.0 Unported license
- Publication date: 2019-11-25
File
Document Identifiers
Author Details
Acknowledgements
Răzvan Diaconescu had major contributions to the implementation in HETS of his generic method of hybridisation of institutions. I wish to thank Till Mossakowski, Fabian Neuhaus and Ionuţ Ţuţu for valuable feedback on language design and implementation issues.
Cite AsGet BibTex
Mihai Codescu. Hybridisation of Institutions in HETS (Tool Paper). In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 17:1-17:10, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.CALCO.2019.17
https://doi.org/10.4230/LIPIcs.CALCO.2019.17
Abstract
We present a tool for the specification and verification of reconfigurable systems. The foundation of the tool is provided by a generic method, called hybridisation of institutions, of extending an arbitrary base institution with features characteristic to hybrid logic, both at the syntactic and the semantic level. Automated proof support for hybridised institutions is obtained via a generic lifting of encodings to first-order logic from the base institution to the hybridised institution. We describe how hybridisation and lifting of encodings to first-order logic are implemented in an extension of the Heterogeneous Tool Set in their full generality. We illustrate the formalism thus obtained with the specification and verification of an autonomous car driving system for highways.
Subject Classification
ACM Subject Classification
- Software and its engineering → Specification languages
- Theory of computation → Algebraic semantics
- Theory of computation → Logic and verification
Keywords
- hybrid logics
- formal verification
- institutions
- reconfigurable systems
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads