Formal Simulation and Visualisation of Hybrid Programs
The design and analysis of systems that combine computational behaviour with physical processes' continuous dynamics -such as movement, velocity, and voltage -is a famous, challenging task.Several theoretical results from programming theory emerged in the last decades to tackle the issue; some of which are the basis of a proof-of-concept tool, called Lince, that aids in the analysis of such systems, by presenting simulations of their respective behaviours.However being a proof-of-concept, the tool is quite limited with respect to usability, and when attempting to apply it to a set of common, concrete problems, involving autonomous driving and others, it either simply cannot simulate them or fails to provide a satisfactory user-experience.The current work complements the aforementioned theoretical approaches with a more practical perspective, by improving Lince along several dimensions: to name a few, richer syntactic constructs, more operations, more informative plotting systems and errors messages, and a better performance overall.We illustrate our improvements via a variety of examples that involve both autonomous driving and electrical systems.
Authors
- José Elias de Proença
- Ricardo Mendes Correia (ORCID: https://orcid.org/0000-0002-2066-0335)
- Renato Neves (ORCID: https://orcid.org/0000-0002-8787-2551)
- Pedro Mendes (ORCID: https://orcid.org/0009-0003-2397-0720)
Institutions
- Universidade do Porto (PT)
- INESC TEC (PT)
- University of Minho (PT)
Publication Details
- Journal
- Electronic Proceedings in Theoretical Computer Science
- Published
- 2024-11-20
- DOI
- https://doi.org/10.4204/eptcs.411.2
- Citations
- 2
- Primary Topic
- Formal Methods in Verification
- Type
- article
- Field-Weighted Citation Impact
- 0.72
Funders
- Ministério da Ciência, Tecnologia e Ensino Superior
- Fundação para a Ciência e a Tecnologia