MODELS 2022
Sun 23 - Fri 28 October 2022 Montréal, Canada
Wed 26 Oct 2022 13:30 - 13:52 at A-3502.1 - Validation & Verification I Chair(s): Marsha Chechik

Multiverse debugging is an extension of classical debugging methods, particularly adapted to non-deterministic systems. Recently, a language-independent formalization was proposed. Moreover, multiverse debugging is particularly beneficial for specification and design languages, such as UML. However, this method suffers from scalability issues during breakpoint lookup. This problem arises due to the exhaustive exploration performed on the potentially infinite state-space of the system.

In this paper, we tackle this problem by introducing Reduced Multiverse Debugging, an extension proposing a way for the user to define reducing policies used during breakpoint lookup. We enrich the formalization of multiverse debugging with a modular breakpoint lookup strategy, which allows the integration of the reduction policy. We validate our approach by implementing a practical UML Statechart debugger in the AnimUML web framework. We show several ways the reduction can be applied, using methods such as predicate abstraction for breakpoint lookup on an infinite state-space, removing irrelevant variables, or creating classes of equivalent values. Moreover, we show the possibility to integrate probabilistic reduction strategies. Relying on hash collisions, these strategies can be iteratively refined to increase precision.

Wed 26 Oct

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

13:30 - 15:00
Validation & Verification ITechnical Track at A-3502.1
Chair(s): Marsha Chechik University of Toronto
13:30
22m
Talk
Practical Multiverse Debugging through User-defined Reductions: Application to UML ModelsFT
Technical Track
Matthias Pasquier Ertosgener, Ciprian Teodorov ENSTA Bretagne, Frédéric Jouault ERIS Team, ESEO , France, Matthias Brun TRAME Team, ESEO, Luka Le Roux Lab-STICC CNRS UMR 6285, ENSTA Bretagne, Loïc Lagadec Lab-STICC CNRS UMR 6285, ENSTA Bretagne
13:52
22m
Talk
Modelling Program Verification Tools for Software EngineersP&I
Technical Track
Sophie Lathouwers University of Twente, Vadim Zaytsev University of Twente, Netherlands
File Attached
14:15
22m
Talk
Automatic Test Amplification for Executable ModelsFT
Technical Track
Faezeh Khorram IMT Atlantique, Nantes, France, Erwan Bousse Nantes Université, Jean-Marie Mottu Université de Nantes, LS2N, IMT Atlantique, Gerson Sunyé Université de Nantes, LS2N, Pablo Gómez-Abajo Universidad Autónoma de Madrid, Pablo C Canizares Autonomous University of Madrid, Spain, Esther Guerra Universidad Aut�noma de Madrid, Juan de Lara Autonomous University of Madrid
Pre-print
14:37
22m
Talk
Feedback on the Formal Verification of UML Models in an Industrial Context: The Case of a Smart Device Life Cycle Management SystemP&I
Technical Track
Maxime Méré STMicroelectronics, Frédéric Jouault ERIS Team, ESEO , France, Loïc Pallardy STMicroelectronics, Richard Perdriau ESEO