Safety verification of state/time-driven hybrid systems using barrier certificates

  • Guobin Wang
  • , Jing Liu
  • , Haiying Sun
  • , Jie Liu
  • , Zuohua Ding
  • , Miaomiao Zhang

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

7 Scopus citations

Abstract

This paper addresses formal safety verification issue of hybrid systems which resort either state-driven or time-driven strategies. Modeling hybrid systems as linear hybrid automata, we provide a formal method for safety verification by constructing barrier certificates whose existence guarantees the soundness of safety specifications. Barrier certificates for safety of state-driven hybrid systems are presented. Particularly, we propose a formal method for constructing time-dependent barrier certificates and show its sufficiency for safety of time-driven hybrid systems. Through formulating the search of time-dependent barrier certificates as a bilinear sum-of-squares programming problem, a computationally tractable method is proposed to derive a certification on safety in polynomial time. A numerical example illustrates the efficiency of the proposed approach.

Original languageEnglish
Title of host publicationProceedings of the 35th Chinese Control Conference, CCC 2016
EditorsJie Chen, Qianchuan Zhao, Jie Chen
PublisherIEEE Computer Society
Pages2483-2489
Number of pages7
ISBN (Electronic)9789881563910
DOIs
StatePublished - 26 Aug 2016
Event35th Chinese Control Conference, CCC 2016 - Chengdu, China
Duration: 27 Jul 201629 Jul 2016

Publication series

NameChinese Control Conference, CCC
Volume2016-August
ISSN (Print)1934-1768
ISSN (Electronic)2161-2927

Conference

Conference35th Chinese Control Conference, CCC 2016
Country/TerritoryChina
CityChengdu
Period27/07/1629/07/16

Keywords

  • Formal Methods
  • Hybrid System
  • Safety Verification

Fingerprint

Dive into the research topics of 'Safety verification of state/time-driven hybrid systems using barrier certificates'. Together they form a unique fingerprint.

Cite this