Edinburgh Research Explorer

Verifying safety and persistence properties of hybrid systems using flowpipes and continuous invariants

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Related Edinburgh Organisations

Open Access permissions

Open

Documents

http://link.springer.com/chapter/10.1007/978-3-319-57288-8_14
Original languageEnglish
Title of host publicationNASA Formal Methods
Subtitle of host publication9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings
PublisherSpringer, Cham
Pages194-211
Number of pages15
ISBN (Electronic)978-3-319-57288-8
ISBN (Print)978-3-319-57287-1
DOIs
Publication statusE-pub ahead of print - 9 Apr 2017
Event9th NASA Formal Methods Symposium - Moffett Field, United States
Duration: 16 May 201718 May 2017
https://ti.arc.nasa.gov/events/nfm-2017/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer, Cham
Volume10227
ISSN (Print)0302-9743

Conference

Conference9th NASA Formal Methods Symposium
Abbreviated titleNFM 2017
CountryUnited States
CityMoffett Field
Period16/05/1718/05/17
Internet address

Abstract

We propose a method for verifying persistence of nonlinear hybrid systems. Given some system and an initial set of states, the method can guarantee that system trajectories always eventually evolve into some specified target subset of the states of one of the discrete modes of the system, and always remain within this target region. The method also computes a time-bound within which the target region is always reached. The approach combines flow-pipe computation with deductive reasoning about invariants and is more general than each technique alone. We illustrate the method with a case study concerning showing that potentially destructive stick-slip oscillations of an oil-well drill eventually die away for a certain choice of drill control parameters. The case study demonstrates how just using flow-pipes or just reasoning about invariants alone can be insufficient. The case study also nicely shows the richness of systems that the method can handle: the case study features a mode with non-polynomial (nonlinear) ODEs and we manage to prove the persistence property with the aid of an automatic prover specifically designed for handling transcendental functions.

Event

9th NASA Formal Methods Symposium

16/05/1718/05/17

Moffett Field, United States

Event: Conference

Download statistics

No data available

ID: 31324616