DROPS

Document

Tool Paper

DOI: 10.4230/LIPIcs.CALCO.2019.17

Hybridisation of Institutions in HETS (Tool Paper)

Authors: Mihai Codescu

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{codescu:LIPIcs.CALCO.2019.17,
  author =	{Codescu, Mihai},
  title =	{{Hybridisation of Institutions in HETS}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{17:1--17:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.17},
  URN =		{urn:nbn:de:0030-drops-114451},
  doi =		{10.4230/LIPIcs.CALCO.2019.17},
  annote =	{Keywords: hybrid logics, formal verification, institutions, reconfigurable systems}
}

Search Results

Documents authored by Codescu, Mihai

Hybridisation of Institutions in HETS (Tool Paper)

Abstract

Cite as

Thanks for your feedback!

Could not send message