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 journalConference articlepeer-review

1 Citation (Scopus)
61 Downloads (Pure)


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 languageEnglish
Pages (from-to)493-500
Number of pages8
Issue number4
Publication statusPublished - 2020
Event15th International Workshop on Discrete Event Systems (WODES 2020) - Virtual, Rio de Janeiro, Brazil
Duration: 11 Nov 202013 Nov 2020
Conference number: 15

Bibliographical note

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


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


Dive into the research topics of 'SMT-based verification of temporal properties for component-based software systems'. Together they form a unique fingerprint.

Cite this