Specification description and verification of multitask hybrid systems in the OTS/CafeOBJ method

TL;DR

This paper presents a formal method for specifying and verifying multitask hybrid systems, combining continuous and discrete data, using the OTS/CafeOBJ approach to improve reliability assurance.

Contribution

It introduces a novel way to describe multitask hybrid systems as observational transition systems in CafeOBJ and verifies properties through equational reasoning.

Findings

Formal specification of hybrid systems in CafeOBJ

Verification of system properties using proof scores

Addresses complexity of multitask hybrid system verification

Abstract

To develop IoT and/or CSP systems, we need consider both continuous data from physical world and discrete data in computer systems. Such a system is called a hybrid system. Because of density of continuous data, it is not easy to do software testing to ensure reliability of hybrid systems. Moreover, the size of the state space increases exponentially for multitask systems. Formal descriptions of hybrid systems may help us to verify desired properties of a given system formally with computer supports. In this paper, we propose a way to describe a formal specification of a given multitask hybrid system as an observational transition system in CafeOBJ algebraic specification language and verify it by the proof score method based on equational reasoning implemented in CafeOBJ interpreter.