Blogs (1) >>
ICSE 2019
Sat 25 - Fri 31 May 2019 Montreal, QC, Canada
Mon 27 May 2019 14:25 - 14:40 at Foyer - Session 3 Chair(s): Eunsuk Kang

We consider the problem of model checking Variability-Intensive Systems (VIS) against non-functional requirements. These requirements are typically expressed as an optimization problem over quality attributes of interest, whose value is determined by the executions of the system. Identifying the optimal variant can be hard for two reasons. First, the state-explosion problem inherent to model checking makes it increasingly complex to find the optimal executions within a given variant. Second, the number of variants can grow exponentially with respect to the number of variation points in the VIS. In this paper, we lay the foundations for the application of smart sampling and statistical model checking to solve this problem faster. We design a simple method that samples variants and executions in a uniform manner from a featured weighted automaton and that assesses which of the sampled variants/executions are optimal. We implemented our approach on top of ProVeLines, a tool suite for model-checking VIS and carried out a preliminary evaluation on an industrial embedded system design case study. Our results tend to show that sampling-based approaches indeed holds the potential to improve scalability but should be supported by better sampling heuristics to be competitive.

Mon 27 May

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

14:00 - 15:30
Session 3FormaliSE at Foyer
Chair(s): Eunsuk Kang Carnegie Mellon University
Parallelizable Reachability Analysis Algorithms for Feed-Forward Neural Networks
Hoang-Dung Tran Vanderbilt University, Patrick Musau Vanderbilt University, Diego Manzanas Lopez Vanderbilt University, Xiao Dong Yang Vanderbilt University, Luan Nguyen University of Pennsylvania, Weiming Xiang Vanderbilt University, Taylor T Johnson Vanderbilt University
Towards Sampling and Simulation-Based Analysis of Featured Weighted Automata
Maxime Cordy SnT, University of Luxembourg, Axel Legay , Sami Lazreg Visteon Electronics and Universite Cote d Azur, Philippe Collet University of Nice
Verifying Channel Communication Correctness for a Multi-Core Cooperatively Scheduled Runtime Using CSP
Jan Pedersen University of Nevada Las Vegas, Kevin Chalmers Edinburgh Napier University
A Generalized Program Verification Workflow Based on Loop Elimination and SA Form
Cláudio Belo Lourenço LRI, Université Paris-Sud & INRIA Saclay, Maria João Frade HASLab/INESC TEC & Universidade do Minho, Portugal, Jorge Sousa Pinto HASLab/INESC TEC & Universidade do Minho, Portugal