Refinement Checking for Multirate Hybrid ZIA

TL;DR

This paper introduces a new specification approach called MZIA for hybrid systems, combining interface automata, multirate hybrid automata, and Z language, along with an algorithm for refinement checking.

Contribution

It presents a novel combined specification framework and a refinement checking algorithm for multirate hybrid automata with finite domains.

Findings

Algorithm for refinement checking is correct

Framework effectively models hybrid systems

Enables formal verification of hybrid system refinements

Abstract

A hybrid system is a dynamical system with both discrete and continuous components. In order to study the modeling and verification aspects of hybrid system, in this paper we first introduce a specification approach combining interface automata, initialized multirate hybrid automata and Z language, which is named MZIA. Meanwhile we propose a refinement relation on MZIAs. Then we give an algorithm for checking refinement relation between MZIAs with finite domain and demonstrate the correctness of the algorithm.