Mining parametric temporal logic properties in model-based design for cyber-physical systems

Bardh Hoxha, Adel Dokhanchi, Georgios Fainekos

Research output: Contribution to journalArticle

5 Citations (Scopus)

Abstract

One of the advantages of adopting a model-based development process is that it enables testing and verification at early stages of development. However, it is often desirable to not only verify/falsify certain formal system specifications, but also to automatically explore the properties that the system satisfies. In this work, we present a framework that enables property exploration for cyber-physical systems. Namely, given a parametric specification with multiple parameters, our solution can automatically infer the ranges of parameters for which the property does not hold on the system. In this paper, we consider parametric specifications in metric or Signal Temporal Logic (MTL or STL). Using robust semantics for MTL, the parameter mining problem can be converted into a Pareto optimization problem for which we can provide an approximate solution by utilizing stochastic optimization methods. We include algorithms for the exploration and visualization of multi-parametric specifications. The framework is demonstrated on an industrial size, high-fidelity engine model as well as examples from related literature.

Original languageEnglish (US)
Pages (from-to)1-15
Number of pages15
JournalInternational Journal on Software Tools for Technology Transfer
DOIs
StateAccepted/In press - Feb 3 2017

Fingerprint

Temporal logic
Specifications
Visualization
Semantics
Engines
Cyber Physical System
Testing

Keywords

  • Cyber-physical systems
  • Metric Temporal Logic
  • Multiple parametric specification mining
  • Robustness
  • Signal Temporal Logic
  • Testing
  • Verification

ASJC Scopus subject areas

  • Software
  • Information Systems

Cite this

@article{ec1d2ba3bb8f478f9480d4c51dd10536,
title = "Mining parametric temporal logic properties in model-based design for cyber-physical systems",
abstract = "One of the advantages of adopting a model-based development process is that it enables testing and verification at early stages of development. However, it is often desirable to not only verify/falsify certain formal system specifications, but also to automatically explore the properties that the system satisfies. In this work, we present a framework that enables property exploration for cyber-physical systems. Namely, given a parametric specification with multiple parameters, our solution can automatically infer the ranges of parameters for which the property does not hold on the system. In this paper, we consider parametric specifications in metric or Signal Temporal Logic (MTL or STL). Using robust semantics for MTL, the parameter mining problem can be converted into a Pareto optimization problem for which we can provide an approximate solution by utilizing stochastic optimization methods. We include algorithms for the exploration and visualization of multi-parametric specifications. The framework is demonstrated on an industrial size, high-fidelity engine model as well as examples from related literature.",
keywords = "Cyber-physical systems, Metric Temporal Logic, Multiple parametric specification mining, Robustness, Signal Temporal Logic, Testing, Verification",
author = "Bardh Hoxha and Adel Dokhanchi and Georgios Fainekos",
year = "2017",
month = "2",
day = "3",
doi = "10.1007/s10009-017-0447-4",
language = "English (US)",
pages = "1--15",
journal = "International Journal on Software Tools for Technology Transfer",
issn = "1433-2779",
publisher = "Springer Verlag",

}

TY - JOUR

T1 - Mining parametric temporal logic properties in model-based design for cyber-physical systems

AU - Hoxha, Bardh

AU - Dokhanchi, Adel

AU - Fainekos, Georgios

PY - 2017/2/3

Y1 - 2017/2/3

N2 - One of the advantages of adopting a model-based development process is that it enables testing and verification at early stages of development. However, it is often desirable to not only verify/falsify certain formal system specifications, but also to automatically explore the properties that the system satisfies. In this work, we present a framework that enables property exploration for cyber-physical systems. Namely, given a parametric specification with multiple parameters, our solution can automatically infer the ranges of parameters for which the property does not hold on the system. In this paper, we consider parametric specifications in metric or Signal Temporal Logic (MTL or STL). Using robust semantics for MTL, the parameter mining problem can be converted into a Pareto optimization problem for which we can provide an approximate solution by utilizing stochastic optimization methods. We include algorithms for the exploration and visualization of multi-parametric specifications. The framework is demonstrated on an industrial size, high-fidelity engine model as well as examples from related literature.

AB - One of the advantages of adopting a model-based development process is that it enables testing and verification at early stages of development. However, it is often desirable to not only verify/falsify certain formal system specifications, but also to automatically explore the properties that the system satisfies. In this work, we present a framework that enables property exploration for cyber-physical systems. Namely, given a parametric specification with multiple parameters, our solution can automatically infer the ranges of parameters for which the property does not hold on the system. In this paper, we consider parametric specifications in metric or Signal Temporal Logic (MTL or STL). Using robust semantics for MTL, the parameter mining problem can be converted into a Pareto optimization problem for which we can provide an approximate solution by utilizing stochastic optimization methods. We include algorithms for the exploration and visualization of multi-parametric specifications. The framework is demonstrated on an industrial size, high-fidelity engine model as well as examples from related literature.

KW - Cyber-physical systems

KW - Metric Temporal Logic

KW - Multiple parametric specification mining

KW - Robustness

KW - Signal Temporal Logic

KW - Testing

KW - Verification

UR - http://www.scopus.com/inward/record.url?scp=85011589663&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85011589663&partnerID=8YFLogxK

U2 - 10.1007/s10009-017-0447-4

DO - 10.1007/s10009-017-0447-4

M3 - Article

SP - 1

EP - 15

JO - International Journal on Software Tools for Technology Transfer

JF - International Journal on Software Tools for Technology Transfer

SN - 1433-2779

ER -