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

Funding

This work was partially supported by the German Research Foundation DFG, as part of Collaborative Research Center (Sonderforschungsbereich) 1320 "EASE - Everyday Activity Science and Engineering", University of Bremen (http://www.ease-crc.org/) and by a grant of the Romanian National Authority for Scientific Research and Innovation, CNCS/CCCDI - UEFISCDI, project number PN-III-P2-2.1-PED-2016-0494, within PNCDI III.

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 As Get 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
    0
    Metadata Views

References

  1. D. Găină. Birkhoff style calculi for hybrid logics. Formal Asp. Comput., 29(5):805-832, 2017. URL: https://doi.org/10.1007/s00165-016-0414-y.
  2. M. Codescu and R. Diaconescu. Hspec language definition. URL: http://imar.ro/~diacon/forver/Hdef.pdf.
  3. M. Codescu and R. Diaconescu. The H system. URL: http://imar.ro/~diacon/forver/forver.html.
  4. R. Diaconescu. Grothendieck Institutions. Applied Categorical Structures, 10(4):383-402, 2002. URL: https://doi.org/10.1023/A:1016330812768.
  5. R. Diaconescu. Quasi-varieties and initial semantics for hybridized institutions. J. Log. Comput., 26(3):855-891, 2016. URL: https://doi.org/10.1093/logcom/ext016.
  6. R. Diaconescu and A. Madeira. Encoding hybridized institutions into first-order logic. Mathematical Structures in Computer Science, 26(5):745-788, 2016. URL: https://doi.org/10.1017/S0960129514000383.
  7. R. Diaconescu and P. S. Stefaneas. Ultraproducts and possible worlds semantics in institutions. Theor. Comput. Sci., 379(1-2):210-230, 2007. URL: https://doi.org/10.1016/j.tcs.2007.02.068.
  8. J. A. Goguen and R. M. Burstall. Institutions: Abstract Model Theory for Specification and Programming. Journal of the Association for Computing Machinery, 39:95-146, 1992. URL: https://doi.org/10.1145/147508.147524.
  9. A. Madeira, R. Neves, L. Soares Barbosa, and M. A. Martins. A method for rigorous design of reconfigurable systems. Sci. Comput. Program., 132:50-76, 2016. URL: https://doi.org/10.1016/j.scico.2016.05.001.
  10. M. A. Martins, A. Madeira, R. Diaconescu, and L. Soares Barbosa. Hybridization of Institutions. In CALCO, volume 6859 of Lecture Notes in Computer Science, pages 283-297. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22944-2_20.
  11. J. Meseguer. General logics. In H.-D. Ebbinghaus et al., editors, Proceedings, Logic Colloquium, 1987, pages 275-329. North-Holland, 1989. Google Scholar
  12. T. Mossakowski. Comorphism-based Grothendieck logics. In K. Diks and W. Rytter, editors, Mathematical foundations of computer science, volume 2420 of Lecture Notes in Computer Science, pages 593-604. Springer Verlag, London, 2002. URL: https://doi.org/10.1007/3-540-45687-2_49.
  13. T. Mossakowski, C. Maeder, and K. Lüttich. The Heterogeneous Tool Set. In O. Grumberg and M. Huth, editors, TACAS 2007, volume 4424 of Lecture Notes in Computer Science, pages 519-522. Springer, Heidelberg, 2007. URL: https://doi.org/10.1007/978-3-540-71209-1_40.
  14. R. Neves, A. Madeira, M. A. Martins, and L. Soares Barbosa. Hybridisation at Work. In R. Heckel and S. Milius, editors, CALCO 2013, volume 8089 of Lecture Notes in Computer Science, pages 340-345. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40206-7_28.
  15. R. Neves, A. Madeira, M. A. Martins, and L. Soares Barbosa. Proof theory for hybrid(ised) logics. Sci. Comput. Program., 126:73-93, 2016. URL: https://doi.org/10.1016/j.scico.2016.03.001.
  16. M. Nyberg. Safety analysis of autonomous driving using semi-Markov processes. In Stein Haugen, Anne Barros, Coen van Gulijk, Trond Kongsvik, and Jan Erik Vinnem, editors, Safety and Reliability-Safe Societies in a Changing World, pages 781-788. CRC Press, 2018. URL: https://doi.org/10.1201/9781351174664-97.
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact