Title: An SMT-based approach for generating trace examples and counter-examples of parametric properties

Authors: Salim Chehida; Yves Ledru; Yoann Blein; German Vega

Addresses: University Grenoble Alpes, CNRS, Grenoble INP, LIG, F-38000, Grenoble, France ' University Grenoble Alpes, CNRS, Grenoble INP, LIG, F-38000, Grenoble, France ' University Grenoble Alpes, CNRS, Grenoble INP, LIG, F-38000, Grenoble, France ' University Grenoble Alpes, CNRS, Grenoble INP, LIG, F-38000, Grenoble, France

Abstract: The ParTraP language has been designed to express temporal and timed properties on finite execution traces of parametric events. It aims to ease properties' expression for users not experienced in formal methods. In this paper, we propose an approach that allows generating trace examples and counter-examples in an understandable fashion in order to help such users to better express requirements. So, ParTraP properties are mapped into a satisfiability modulo theories (SMT) context to be fed to Z3 SMT solver to check satisfaction and produce interpretations. A tool named ParTraP-EG is dedicated to that purpose. We report experiments carried out on a set of properties from an industrial case study of computer-aided surgery system.

Keywords: runtime verification; parametric traces; temporal properties; timed properties; satisfiability modulo theories; SMT; trace examples; trace counter-examples.

DOI: 10.1504/IJCCBS.2021.117997

International Journal of Critical Computer-Based Systems, 2021 Vol.10 No.2, pp.143 - 183

Received: 09 Oct 2020
Accepted: 22 Mar 2021
Published online: 06 Oct 2021 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article