Analyzing Many Simulations of Hybrid Programs in Lince

TL;DR

This paper introduces enhancements to the Lince tool, enabling it to run multiple simulations and generate histograms to analyze the frequency of properties in hybrid systems, demonstrated through adaptive cruise control models.

Contribution

The paper presents new mechanisms in Lince for executing multiple simulation variants and quantifying property frequencies, improving analysis of hybrid systems.

Findings

Enhanced Lince can run multiple simulations efficiently.

Histograms effectively quantify property satisfaction frequencies.

Demonstration on adaptive cruise control shows practical applicability.

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.