Daedalux: An Extensible Platform for Variability-Aware Model Checking
This paper presents Daedalux, a new model-checking platform for variability-intensive systems based on \emph{Featured Transition System} theory developed in C++. Daedalux features a modular, flexible and extensible architecture, overcoming previous tools’ maintainability limitations. In addition, during verification, it provides visualizations of intermediate models and results. A key added value of Daedalux lies in its software architecture, which allows straightforward extension and integration of new formalisms and verification algorithms. We have ourselves implemented two recent FTS-based approaches, i.e. a statistical model checking algorithm for LTL properties and an exhaustive algorithm for multi-LTL properties. By reducing the entry barrier of understanding variability-aware model checking and facilitating the comprehension and extension of the software tools, we hope to increase the ambitions of the community in developing novel model-checking advances. A video demonstration of Daedalux can be found at \url{https://youtu.be/kirpOAlV-0w}.
Wed 17 AprDisplayed time zone: Lisbon change
14:00 - 15:30 | Dependability and Formal methods 1Software Engineering in Practice / Demonstrations / Research Track at Maria Helena Vieira da Silva Chair(s): Domenico Bianculli University of Luxembourg | ||
14:00 15mTalk | REDriver: Runtime Enforcement for Autonomous Vehicles Research Track Yang Sun Singapore Management University, Chris Poskitt Singapore Management University, Xiaodong Zhang , Jun Sun Singapore Management University Pre-print | ||
14:15 15mTalk | Scalable Relational Analysis via Relational Bound Propagation Research Track DOI Pre-print | ||
14:30 15mTalk | Kind Controllers and Fast Heuristics for Non-Well-Separated GR(1) Specifications Research Track Ariel Gorenstein Tel Aviv University, Shahar Maoz Tel Aviv University, Jan Oliver Ringert Bauhaus-University Weimar | ||
14:45 15mTalk | On the Difficulty of Identifying Incident-Inducing Changes Software Engineering in Practice Eileen Kapel ING & Delft University of Technology, Luís Cruz Delft University of Technology, Diomidis Spinellis Athens University of Economics and Business & Delft University of Technology, Arie van Deursen Delft University of Technology | ||
15:00 15mTalk | Autonomous Monitors for Detecting Failures Early and Reporting Interpretable Alerts in Cloud Operations Software Engineering in Practice Adha Hrusto Lund University, Sweden, Per Runeson Lund University, Magnus C Ohlsson System Verification | ||
15:15 7mTalk | nvshare: Practical GPU Sharing without Memory Size Constraints Demonstrations Pre-print | ||
15:22 7mTalk | Daedalux: An Extensible Platform for Variability-Aware Model Checking Demonstrations Sami Lazreg Visteon Electronics and Universite Cote d Azur, Maxime Cordy University of Luxembourg, Luxembourg, Simon Thrane Hansen SnT, University of Luxembourg, Axel Legay Université Catholique de Louvain, Belgium | ||