Document Open Access Logo

Hybridisation of Institutions in HETS (Tool Paper)

Author Mihai Codescu



PDF
Thumbnail PDF

File

LIPIcs.CALCO.2019.17.pdf
  • Filesize: 444 kB
  • 10 pages

Document Identifiers

Author Details

Mihai Codescu
  • University of Bremen, Collaborative Research Center EASE, Bremen, Germany
  • Institute of Mathematics "Simion Stoilow" of the Romanian Academy, Research Group of the project PED-0494, Bucharest, Romania

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

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)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail