Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formal Simulation and Visualisation of Hybrid Programs

Pedro Mendes, Ricardo Correia, Renato Neves, José Proença

TL;DR

Improvements are made to Lince along several dimensions, including, to name a few, richer syntactic constructs, more operations, more informative plotting systems and errors messages, and a better performance overall.

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.

Formal Simulation and Visualisation of Hybrid Programs

TL;DR

Improvements are made to Lince along several dimensions, including, to name a few, richer syntactic constructs, more operations, more informative plotting systems and errors messages, and a better performance overall.

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.

Paper Structure

This paper contains 6 sections, 5 theorems, 30 equations, 10 figures, 1 table.

Table of Contents

  1. Introduction
  2. Lince's Foundations Extended with the Possibility of Failure
  3. An Improved Simulator for Hybrid Programs
  4. An Improved Visualiser for Hybrid Programs
  5. Lince at Work: a Showcase of the Overall List of Improvements
  6. Conclusion and Future Work

Key Result

Theorem 2.1

For every program ${\tt p\xspace}$, environment $\sigma$, and time instant $t$ there is at most one applicable reduction rule.

Figures (10)

  • Figure 1: Simulation of \ref{['eq:mot']}.
  • Figure 2: Extension of the big-step operational semantics in goncharov2020implementing with the possibility of failure.
  • Figure 3: Extension of the small-step operational semantics in goncharov2020implementing with the possibility of failure.
  • Figure 4: Hybrid program (left) and its plot (right) of two variations of an RLC circuit that tries to maintain the voltage in the capacitor at $10V$.
  • Figure 5: Plot of AEBOM using the traditional plotting system in Lince (left), and a new customised 2D plot (right) relating -1 x with -1 y (the robot's coordinates) and -1 xl with -1 yl (the obstacle's coordinates).
  • ...and 5 more figures

Theorems & Definitions (10)

  • Example 2.1
  • Theorem 2.1
  • Corollary 1: Determinism
  • proof
  • Lemma 2.1
  • proof
  • Proposition 1
  • proof
  • Theorem 2.2: Equivalence
  • proof