Write a Blog >>
Fri 16 - Fri 23 October 2020
Wed 21 Oct 2020 15:20 - 15:40 at Room B - B3-Model Analysis and Validation Chair(s): Marsha Chechik

Automatically synthesizing consistent models is a key prerequisite for many testing scenarios in autonomous driving or software tool validation where model-based systems engineering techniques are frequently used to ensure a designated coverage of critical cornercases. From a practical perspective, an inconsistent model is irrelevant as a test case (e.g. false positive), thus each synthetic model needs to simultaneously satisfy various structural and attribute well-formedness constraints. While different logic solvers or dedicated graph solvers have recently been developed, they fail to handle either structural or attribute constraints in a scalable way. In the current paper, we combine a structural graph solver that uses partial models with an SMT-solver to automatically derive models with which simultaneously fulfill structural and attribute constraints while key theoretical properties of model generation like completeness or diversity are still ensured. This necessitates a sophisticated bidirectional interaction between different solvers which carry out consistency checks, decision, unit propagation, concretization steps. We evaluate the scalability and diversity of our approach in the context of three complex case studies.

Conference Day
Wed 21 Oct

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

15:00 - 16:15
B3-Model Analysis and ValidationTechnical Track at Room B
Chair(s): Marsha ChechikUniversity of Toronto, Canada
Semantic Comparisons of Alloy ModelsFT
Technical Track
Jan Oliver RingertUniversity of Leicester, Syed Waqee WaliUniversity of Leicester, UK
DOI Pre-print
Automated Generation of Consistent Models with Structural and Attribute ConstraintsFT
Technical Track
Oszkár SemeráthBudapest University of Technology and Economics, Aren BabikianMcGill University, Anqi Li, Kristóf Marussy, Daniel VarroMcGill University / Budapest University of Technology and Economics
Link to publication
mel - Model Extractor Language for Extracting Facts from ModelsFT
Technical Track
Robert Hackman, Joanne M. AtleeUniversity of Waterloo, Finn HacketComputer Science, University of Waterloo, Michael W. GodfreyUniversity of Waterloo, Canada
Strengthening Validation of Model Behavior through Filmstrip Templates in the tool USEDemo
Technical Track