An SMT-based approach for generating trace examples and counter-examples of parametric properties
by Salim Chehida; Yves Ledru; Yoann Blein; German Vega
International Journal of Critical Computer-Based Systems (IJCCBS), Vol. 10, No. 2, 2021

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.

Online publication date: Wed, 06-Oct-2021

The full text of this article is only available to individual subscribers or to users at subscribing institutions.

 
Existing subscribers:
Go to Inderscience Online Journals to access the Full Text of this article.

Pay per view:
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.

Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of Critical Computer-Based Systems (IJCCBS):
Login with your Inderscience username and password:

Username:        Password:          Forgotten your password?

Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.

If you still need assistance, please email subs@inderscience.com