A Formal Proof of the Soundness of the Hybrid CPS Clock Theory

Jianlin Wang, Chao Peng, Zhenbing Zeng

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

In this paper, we presented a formalization to the Clock Theory of He Jifeng in the Isabelle interactive theorem prover, we described the basic concepts of the theory in Isabelle and proved its soundness for programming hybrid systems.

Original languageEnglish
Title of host publicationProceedings - 2020 International Symposium on Theoretical Aspects of Software Engineering, TASE 2020
EditorsToshiaki Aoki, Qin Li
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages97-104
Number of pages8
ISBN (Electronic)9781728140865
DOIs
StatePublished - Dec 2020
Event14th International Symposium on Theoretical Aspects of Software Engineering, TASE 2020 - Hangzhou, China
Duration: 11 Dec 202013 Dec 2020

Publication series

NameProceedings - 2020 International Symposium on Theoretical Aspects of Software Engineering, TASE 2020

Conference

Conference14th International Symposium on Theoretical Aspects of Software Engineering, TASE 2020
Country/TerritoryChina
CityHangzhou
Period11/12/2013/12/20

Keywords

  • He Jifeng's clock theory
  • Isabelle/HOL formalization
  • Real number sequence
  • Soundness
  • Topology space

Fingerprint

Dive into the research topics of 'A Formal Proof of the Soundness of the Hybrid CPS Clock Theory'. Together they form a unique fingerprint.

Cite this