SMT-based verification of temporal properties for component-based software systems

R. Jonk; J. Voeten; M. Geilen; T. Basten; R. Schiffelers

doi:10.1016/j.ifacol.2021.04.045

SMT-based verification of temporal properties for component-based software systems

R. Jonk, J. Voeten, M. Geilen, T. Basten, R. Schiffelers

Research output: Contribution to journal › Conference article › peer-review

1 Citation (Scopus)

30 Downloads (Pure)

Abstract

We introduce a technique to verify temporal properties expressed in MTL on Interval Message Sequence Charts (IMSC), a model based on UML2.0 MSC that captures the timed execution of component-based software systems. We accomplish this by encoding the IMSC and the property of interest in a constraint satisfaction problem, which is then solved with an SMT solver. We demonstrate the scalability of this technique with a synthetic case study and a large-scale industrial case study.

Original language	English
Pages (from-to)	493-500
Number of pages	8
Journal	IFAC-PapersOnLine
Volume	53
Issue number	4
DOIs	https://doi.org/10.1016/j.ifacol.2021.04.045
Publication status	Published - 2020
Event	15th International Workshop on Discrete Event Systems (WODES 2020) - Virtual, Rio de Janeiro, Brazil Duration: 11 Nov 2020 → 13 Nov 2020 Conference number: 15

Bibliographical note

Publisher Copyright:
© 2020 Elsevier B.V.. All rights reserved.

Keywords

Component-based software system
Message Sequence Chart
Metric Temporal Logic
Modeling
Verification

Access to Document

10.1016/j.ifacol.2021.04.045

1-s2.0-S2405896321000951-mainFinal published version, 783 KB

Cite this

@article{d0ae55b54db14a3db74cac85518ddc20,

title = "SMT-based verification of temporal properties for component-based software systems",

abstract = "We introduce a technique to verify temporal properties expressed in MTL on Interval Message Sequence Charts (IMSC), a model based on UML2.0 MSC that captures the timed execution of component-based software systems. We accomplish this by encoding the IMSC and the property of interest in a constraint satisfaction problem, which is then solved with an SMT solver. We demonstrate the scalability of this technique with a synthetic case study and a large-scale industrial case study.",

keywords = "Component-based software system, Message Sequence Chart, Metric Temporal Logic, Modeling, Verification",

author = "R. Jonk and J. Voeten and M. Geilen and T. Basten and R. Schiffelers",

note = "Publisher Copyright: {\textcopyright} 2020 Elsevier B.V.. All rights reserved.; 15th International Workshop on Discrete Event Systems (WODES 2020), WODES 2020 ; Conference date: 11-11-2020 Through 13-11-2020",

year = "2020",

doi = "10.1016/j.ifacol.2021.04.045",

language = "English",

volume = "53",

pages = "493--500",

journal = "IFAC-PapersOnLine",

issn = "2405-8963",

publisher = "Elsevier",

number = "4",

}

TY - JOUR

T1 - SMT-based verification of temporal properties for component-based software systems

AU - Jonk, R.

AU - Voeten, J.

AU - Geilen, M.

AU - Basten, T.

AU - Schiffelers, R.

N1 - Conference code: 15

PY - 2020

Y1 - 2020

N2 - We introduce a technique to verify temporal properties expressed in MTL on Interval Message Sequence Charts (IMSC), a model based on UML2.0 MSC that captures the timed execution of component-based software systems. We accomplish this by encoding the IMSC and the property of interest in a constraint satisfaction problem, which is then solved with an SMT solver. We demonstrate the scalability of this technique with a synthetic case study and a large-scale industrial case study.

AB - We introduce a technique to verify temporal properties expressed in MTL on Interval Message Sequence Charts (IMSC), a model based on UML2.0 MSC that captures the timed execution of component-based software systems. We accomplish this by encoding the IMSC and the property of interest in a constraint satisfaction problem, which is then solved with an SMT solver. We demonstrate the scalability of this technique with a synthetic case study and a large-scale industrial case study.

KW - Component-based software system

KW - Message Sequence Chart

KW - Metric Temporal Logic

KW - Modeling

KW - Verification

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

U2 - 10.1016/j.ifacol.2021.04.045

DO - 10.1016/j.ifacol.2021.04.045

M3 - Conference article

AN - SCOPUS:85106557400

SN - 2405-8963

VL - 53

SP - 493

EP - 500

JO - IFAC-PapersOnLine

JF - IFAC-PapersOnLine

IS - 4

T2 - 15th International Workshop on Discrete Event Systems (WODES 2020)

Y2 - 11 November 2020 through 13 November 2020

ER -

SMT-based verification of temporal properties for component-based software systems

Abstract

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Cite this