Open AccessFormal Verification of Multitask Hybrid Systems by the OTS/CafeOBJ Method
Author(s) -
Masaki Nakamura,
Kazutoshi Sakakibara,
Yuki Okura,
Kôichi Ogata
Publication year - 2021
Publication title -
international journal of software engineering and knowledge engineering
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.236
H-Index - 36
eISSN - 1793-6403
pISSN - 0218-1940
DOI - 10.1142/s0218194021400118
Subject(s) - computer science , algebraic specification , hybrid system , property (philosophy) , interpreter , proof assistant , programming language , theoretical computer science , mathematical proof , formal specification , mathematics , philosophy , geometry , epistemology , machine learning
Hybrid systems combine both continuous and discrete behaviors, which occur frequently in safety-critical applications in various domains including Internet-of-Things (IoT) and Cyber-Physical Systems (CPS) applications such as health care, transportation, and robotics. For safe and reliable information society with IoT and CPS technologies, it is important to establish a way to specify and verify hybrid systems formally. Formal descriptions of hybrid systems may help us to verify desired properties of a given system formally with computer supports. We propose a way to describe a formal specification of a given multitask hybrid system as an observational transition system (OTS) in CafeOBJ algebraic specification language. OTSs are models where systems behaviors are described through observations. CafeOBJ supports specification execution based on a rewrite theory. We verify that OTS/CafeOBJ specifications of hybrid systems satisfy desired property by the proof score method based on equational reasoning implemented in CafeOBJ interpreter. In this paper, we specify a signal control system with an arbitrary number of vehicles by our proposed method, and verify the system satisfies a safety property by the proof score method.