A unified framework for modeling and implementation of hybrid systems with synchronous controllers

TL;DR

This paper introduces a unified framework that integrates synchronous programming with hybrid automata to model, implement, and verify hybrid control systems with improved fidelity and support for non-instantaneous control transitions.

Contribution

It extends the SystemJ language for hybrid systems, providing a sound semantics and enabling verification with classical model-checking tools.

Findings

Higher fidelity in system design compared to traditional hybrid automaton methods

Enables verification of hybrid systems using existing model-checkers

Supports non-instantaneous discrete control transitions

Abstract

This paper presents a novel approach to including non-instantaneous discrete control transitions in the linear hybrid automaton approach to simulation and verification of hybrid control systems. In this paper we study the control of a continuously evolving analog plant using a controller programmed in a synchronous programming language. We provide extensions to the synchronous subset of the SystemJ programming language for modeling, implementation, and verification of such hybrid systems. We provide a sound rewrite semantics that approximate the evolution of the continuous variables in the discrete domain inspired from the classical supervisory control theory. The resultant discrete time model can be verified using classical model-checking tools. Finally, we show that systems designed using our approach have a higher fidelity than the ones designed using the hybrid automaton approach.