Write a Blog >>
ICSE 2021
Mon 17 May - Sat 5 June 2021
Wed 26 May 2021 11:40 - 12:00 at Blended Sessions Room 3 - 2.1.3. Model Checking Chair(s): Oscar Dieste
Wed 26 May 2021 23:40 - 00:00 at Blended Sessions Room 3 - 2.1.3. Model Checking

Parametric model checking (PMC) computes algebraic formulae that express key non-functional properties of a system (reliability, performance, etc.) as rational functions of the system and environment parameters. In software engineering, PMC formulae can be used during design, e.g., to analyse the sensitivity of different system architectures to parametric variability, or to find optimal system configurations. They can also be used at runtime, e.g., to check if non-functional requirements are still satisfied after environmental changes, or to select new configurations after such changes. However, current PMC techniques do not scale well to systems with complex behaviour and more than a few parameters. Our paper introduces a fast PMC (fPMC) approach that overcomes this limitation, extending the applicability of PMC to a broader class of systems than previously possible. To this end, fPMC partitions the Markov models that PMC operates with into fragments whose reachability properties are analysed independently, and obtains PMC reachability formulae by combining the results of these fragment analyses. To demonstrate the effectiveness of fPMC, we show how our fPMC tool can analyse three systems (taken from the research literature, and belonging to different application domains) with which current PMC techniques and tools struggle.

Wed 26 May

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

11:20 - 12:20
2.1.3. Model CheckingTechnical Track / Journal-First Papers at Blended Sessions Room 3 +12h
Chair(s): Oscar Dieste Universidad Politécnica de Madrid
11:20
20m
Paper
Adversarial Specification MiningJournal-First
Journal-First Papers
Hong Jin Kang , David Lo Singapore Management University
DOI Pre-print Media Attached
11:40
20m
Paper
Fast Parametric Model Checking through Model FragmentationTechnical Track
Technical Track
Xinwei Fang University of York, UK, Radu Calinescu University of York, UK, Simos Gerasimou University of York, UK, Faisal Alhwikem University of York, UK
Pre-print Media Attached
12:00
20m
Paper
Trace-Checking CPS Properties: Bridging the Cyber-Physical GapArtifact ReusableTechnical TrackArtifact Available
Technical Track
Claudio Menghi University of Luxembourg, Enrico Viganò University of Luxembourg, Domenico Bianculli University of Luxembourg, Lionel Briand University of Luxembourg and University of Ottawa
Pre-print Media Attached
23:20 - 00:20
23:20
20m
Paper
Adversarial Specification MiningJournal-First
Journal-First Papers
Hong Jin Kang , David Lo Singapore Management University
DOI Pre-print Media Attached
23:40
20m
Paper
Fast Parametric Model Checking through Model FragmentationTechnical Track
Technical Track
Xinwei Fang University of York, UK, Radu Calinescu University of York, UK, Simos Gerasimou University of York, UK, Faisal Alhwikem University of York, UK
Pre-print Media Attached
00:00
20m
Paper
Trace-Checking CPS Properties: Bridging the Cyber-Physical GapArtifact ReusableTechnical TrackArtifact Available
Technical Track
Claudio Menghi University of Luxembourg, Enrico Viganò University of Luxembourg, Domenico Bianculli University of Luxembourg, Lionel Briand University of Luxembourg and University of Ottawa
Pre-print Media Attached