Analyzing Many Simulations of Hybrid Programs in Lince

TL;DR

The paper addresses the challenge of analyzing multiple simulations of hybrid programs, where overlapping trajectories hinder verification of temporal properties. It introduces a histogram-based extension to Lince that collects data during simulations and visualizes the frequency with which a given goal is satisfied over time across parameter variants. The adaptive cruise control case study demonstrates how histograms reveal safety-compliance patterns across different leader accelerations, providing clearer insight than traditional trajectory plots. Overall, the work delivers a browser-based, lightweight tool for executing, analyzing, and visualizing many simulations, with prospects for stochastic extensions and monitor-based testing.

Abstract

Hybrid systems are increasingly used in critical applications such as medical devices, infrastructure systems, and autonomous vehicles. Lince is an academic tool for specifying and simulating such systems using a C-like language with differential equations. This paper presents recent experiments that enhance Lince with mechanisms for executing multiple simulation variants and generating histograms that quantify the frequency with which a given property holds. We illustrate our extended Lince using variations of an adaptive cruise control system.

Figures (3)

• Figure 1: Modelling of a cruise control system in Lince
• Figure 2: Histogram plotting of Cruise Control with 5 and 50 simulations, respectively
• Figure 3: Simulations of the ACC in Lince, displaying the trajectories of the vehicles (left) and the histogram counting when $ct\le0$.