Title
SMT-based verification of temporal properties for component-based software systems
Author
Jonk, R.
Voeten, J.
Geilen, M.
Basten, T.
Schiffelers, R.
Publication year
2020
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 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.
Subject
Verification
Compnent-based software system
Message Sequence Chart
Metric Temporal Logic
Modeling
To reference this document use:
http://resolver.tudelft.nl/uuid:4b2f89c3-5d03-4731-89e0-0a28f2117bf3
DOI
https://doi.org/10.1016/j.ifacol.2021.04.045
TNO identifier
956650
Publisher
Elsevier B.V.
ISSN
2405-8963
Source
IFAC-PapersOnLine, 53 (53), 493-500
Bibliographical note
21st IFAC World Congress 2020, 12 July 2020 through 17 July 2020
Document type
conference paper