Conservative Hybrid Automata from Development Artifacts

TL;DR

This paper introduces an automatic method for constructing conservative hybrid automata for cyber-physical systems using existing development artifacts, enhancing scalability and safety verification accuracy.

Contribution

It presents a novel hybrid approach that combines top-down and bottom-up techniques to build conservative models from development artifacts without extra costs.

Findings

The algorithm scales well for large systems.

It produces conservative models ensuring safety.

Utilizes existing artifacts without additional overhead.

Abstract

The verification of cyber-physical systems operating in a safety-critical environment requires formal system models. The validity of the verification hinges on the precision of the model: possible behavior not captured in the model can result in formally verified, but unsafe systems. Yet, manual construction is delicate and error-prone while automatic construction does not scale for large and complex systems. As a remedy, this paper devises an automatic construction algorithm that utilizes information contained in artifacts of the development process: a runtime monitoring specification and recorded test traces. These artifacts incur no additional cost and provide sufficient information so that the construction process scales well for large systems. The algorithm uses a hybrid approach between a top-down and a bottom-up construction which allows for proving the result conservative, while limiting the level of over-approximation.