SMT-based verification of temporal properties for component-based software systems
conference paper
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.
Topics
TNO Identifier
956650
ISSN
24058963
Publisher
Elsevier B.V.
Source title
IFAC-PapersOnLine
Pages
493-500