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

Onderzoeksoutput: Bijdrage aan tijdschrift › Congresartikel › peer review

1 Citaat (Scopus)

71 Downloads (Pure)

Samenvatting

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.

Originele taal-2	Engels
Pagina's (van-tot)	493-500
Aantal pagina's	8
Tijdschrift	IFAC-PapersOnLine
Volume	53
Nummer van het tijdschrift	4
DOI's	https://doi.org/10.1016/j.ifacol.2021.04.045
Status	Gepubliceerd - 2020
Evenement	15th International Workshop on Discrete Event Systems (WODES 2020) - Virtual, Rio de Janeiro, Brazilië Duur: 11 nov. 2020 → 13 nov. 2020 Congresnummer: 15

Bibliografische nota

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

Toegang tot document

10.1016/j.ifacol.2021.04.045

1-s2.0-S2405896321000951-mainDefinitieve gepubliceerde versie, 783 KB

Andere bestanden en links

Link naar publicatie in Scopus

Citeer dit

@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

Samenvatting

Bibliografische nota

Toegang tot document

Andere bestanden en links

Vingerafdruk

Citeer dit