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

Research output: Contribution to journalConference articleAcademicpeer-review

14 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 languageEnglish
Pages (from-to)493-500
Number of pages8
JournalIFAC-PapersOnLine
Volume53
Issue number4
DOIs
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.

Keywords

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

Fingerprint

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