2026-07-28T12:56:12Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:11445 2024-03-06T10:47:08Z ddc:004 open_access

Hybridisation of Institutions in HETS (Tool Paper) Codescu, Mihai hybrid logics formal verification institutions reconfigurable systems 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Mihai Codescu 2019 Is Part Of LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CALCO.2019.17 urn:nbn:de:0030-drops-114451 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.17 eng https://creativecommons.org/licenses/by/3.0/legalcode