Formal feature interpretation of hybrid systems

Antonio Anastasio Bruto Da Costa; Goran Frehse; Pallab Dasgupta

doi:10.1109/TCAD.2018.2857361

Formal feature interpretation of hybrid systems

Antonio Anastasio Bruto Da Costa, Goran Frehse, Pallab Dasgupta

Research output: Contribution to journal › Article › peer-review

Abstract

In current practice a formal analysis of hybrid system models is assertion-based. The work presented here is based on features that look beyond functional correctness toward a quantitative evaluation of behavioral attributes. A feature defines a real-valued evaluation function over a specific set of traces. This paper describes an improved method for the interpretation of features over hybrid automata models. It further demonstrates how satisfiability modulo theory solvers can be used for extracting behavioral traces corresponding to corner cases of a feature. Results are demonstrated on examples from the control and circuit domains.

Original language	English
Article number	8413134
Pages (from-to)	2474-2484
Number of pages	11
Journal	IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Volume	37
Issue number	11
DOIs	https://doi.org/10.1109/TCAD.2018.2857361
Publication status	Published - 1 Nov 2018
Externally published	Yes

Keywords

Features
hybrid automata (HA)
model checking
sequence expressions

Access to Document

10.1109/TCAD.2018.2857361

Cite this

@article{4361fb8cae4844458809e9ebe2ded8e4,

title = "Formal feature interpretation of hybrid systems",

abstract = "In current practice a formal analysis of hybrid system models is assertion-based. The work presented here is based on features that look beyond functional correctness toward a quantitative evaluation of behavioral attributes. A feature defines a real-valued evaluation function over a specific set of traces. This paper describes an improved method for the interpretation of features over hybrid automata models. It further demonstrates how satisfiability modulo theory solvers can be used for extracting behavioral traces corresponding to corner cases of a feature. Results are demonstrated on examples from the control and circuit domains.",

keywords = "Features, hybrid automata (HA), model checking, sequence expressions",

author = "\{Bruto Da Costa\}, \{Antonio Anastasio\} and Goran Frehse and Pallab Dasgupta",

note = "Publisher Copyright: {\textcopyright} 1982-2012 IEEE.",

year = "2018",

month = nov,

day = "1",

doi = "10.1109/TCAD.2018.2857361",

language = "English",

volume = "37",

pages = "2474--2484",

journal = "IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems",

issn = "0278-0070",

number = "11",

}

TY - JOUR

T1 - Formal feature interpretation of hybrid systems

AU - Bruto Da Costa, Antonio Anastasio

AU - Frehse, Goran

AU - Dasgupta, Pallab

PY - 2018/11/1

Y1 - 2018/11/1

N2 - In current practice a formal analysis of hybrid system models is assertion-based. The work presented here is based on features that look beyond functional correctness toward a quantitative evaluation of behavioral attributes. A feature defines a real-valued evaluation function over a specific set of traces. This paper describes an improved method for the interpretation of features over hybrid automata models. It further demonstrates how satisfiability modulo theory solvers can be used for extracting behavioral traces corresponding to corner cases of a feature. Results are demonstrated on examples from the control and circuit domains.

AB - In current practice a formal analysis of hybrid system models is assertion-based. The work presented here is based on features that look beyond functional correctness toward a quantitative evaluation of behavioral attributes. A feature defines a real-valued evaluation function over a specific set of traces. This paper describes an improved method for the interpretation of features over hybrid automata models. It further demonstrates how satisfiability modulo theory solvers can be used for extracting behavioral traces corresponding to corner cases of a feature. Results are demonstrated on examples from the control and circuit domains.

KW - Features

KW - hybrid automata (HA)

KW - model checking

KW - sequence expressions

U2 - 10.1109/TCAD.2018.2857361

DO - 10.1109/TCAD.2018.2857361

M3 - Article

AN - SCOPUS:85050411165

SN - 0278-0070

VL - 37

SP - 2474

EP - 2484

JO - IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

JF - IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

IS - 11

M1 - 8413134

ER -

Formal feature interpretation of hybrid systems

Abstract

Keywords

Access to Document

Fingerprint

Cite this