SMT-based verification of temporal properties for component-based software systems
Ruben J. W. Jonk, Jeroen P. M. Voeten, Marc C. W. Geilen, Twan Basten, Ramon R. H. Schiffelers · IFAC-PapersOnLine · 2020
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.