MODELS 2022
Sun 23 - Fri 28 October 2022 Montréal, Canada
Thu 27 Oct 2022 11:15 - 11:37 at A-4502.1 - Validation & Verification II Chair(s): Øystein Haugen

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. While the synthesized system is guaranteed to be correct w.r.t. the specification, the specification itself may be incorrect w.r.t. the engineers’ intention or w.r.t. the environment in which the system should execute in. It thus requires validation.

Combinatorial coverage (CC) is a well-known coverage criterion. Its rationale and key for effectiveness is the empirical observation that in many cases, the presence of a defect depends on the interaction between a small number of features of the system at hand.

In this work we propose a validation approach for a reactive system specification, based on a systematic combinatorial exploration of the behaviors of a controller that was synthesized from it. Specifically, we present an algorithm to generate and execute a small scenario suite that covers all tuples of given variable value combinations over the reachable states of the controller.

We have implemented our work in the Spectra synthesis environment. We evaluated it over benchmarks from the literature using a mutation approach, specifically tailored for evaluating scenario suites of temporal specifications for reactive synthesis. The evaluation shows that for pairwise coverage, our CC algorithm is feasible and provide a 1.7 factor of improvement in mutation score compared to random scenario generation. We further report on a case study with students who have participated in a workshop class at our university and have used our tool to validate their specifications. The case study results demonstrate the potential effectiveness of our work in helping engineers detect real bugs in the specifications they write.

Thu 27 Oct

Displayed time zone: Eastern Time (US & Canada) change

10:30 - 12:00
Validation & Verification IITechnical Track / Journal-first at A-4502.1
Chair(s): Øystein Haugen Østfold University College
10:30
22m
Talk
A Domain-Specific Language for Simulation-Based Testing of IoT Edge-to-Cloud SolutionsP&I
Technical Track
Jia Li University of Ottawa, Shiva Nejati University of Ottawa, Mehrdad Sabetzadeh University of Ottawa, Michael McCallen Cheetah Networks
10:52
22m
Talk
Model-based ideal testing of hardware description language (HDL) programsJ1st
Journal-first
Onur Kilincceker , Ercument Turk , Fevzi Belli Paderborn University, Germany, Moharram Challenger University of Antwerp
Link to publication
11:15
22m
Talk
Validating the Correctness of Reactive Systems Specifications Through Systematic ExplorationFT
Technical Track
Dor Ma'ayan Tel Aviv University, Shahar Maoz Tel Aviv University, Israel, Roey Rozi Tel Aviv University
Pre-print
11:37
22m
Talk
Probabilistic modelling and verification using RoboChart and PRISMJ1st
Journal-first
Kangfeng Ye University of York, UK, Ana Cavalcanti University of York, Simon Foster University of York, Alvaro Miyazawa , Jim Woodcock
Link to publication