Formal Simulation and Visualisation of Hybrid Programs

TL;DR

This paper enhances the Lince tool for simulating hybrid systems by adding practical features like richer syntax, better performance, and improved visualization, enabling more effective analysis of complex systems such as autonomous vehicles and electrical circuits.

Contribution

The work extends the theoretical foundations of hybrid system simulation with practical improvements to the Lince tool, making it more usable and effective for real-world applications.

Findings

Enhanced Lince supports more complex hybrid programs.

Improved visualization and error messaging aid user experience.

Successfully applied to autonomous driving and electrical systems examples.

Abstract

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.