Wed 17 Jul 2024 12:12 - 12:30 at Pitanga - Formal Verification Chair(s): Yunja Choi

Simulation-based software testing supports engineers in finding faults in Simulink models. It typically relies on search algorithms that iteratively generate test inputs used to exercise models in simulation to detect design errors. While simulation-based software testing techniques are effective in many practical scenarios, they are typically not fully integrated within the Simulink environment and require additional manual effort. Many techniques require engineers to specify requirements using logical languages that are neither intuitive nor fully supported by Simulink, thereby limiting their adoption in industry.

This work presents HECATE, a testing approach for Simulink models using Test Sequence and Test Assessment blocks from Simulink Test. Unlike existing testing techniques, HECATE uses information from Simulink models to guide the search-based exploration. Specifically, HECATE relies on information provided by the Test Sequence and Test Assessment blocks to guide the search procedure. Across a benchmark of 18 Simulink models from different domains and industries, our comparison of HECATE with the state-of-the-art testing tool S-TALIRO indicates that HECATE is both more effective (more failure-revealing test cases) and efficient (less iterations and computational time) than S_TALIRO for $\approx94%$ and $\approx83%$ of benchmark models respectively. Furthermore, HECATE successfully generated a failure-revealing test case for a representative case study from the automotive domain demonstrating its practical usefulness.

Wed 17 Jul

Displayed time zone: Brasilia, Distrito Federal, Brazil change

11:00 - 12:30
Formal VerificationDemonstrations / Journal First / Research Papers / Industry Papers at Pitanga
Chair(s): Yunja Choi Kyungpook National University
11:00
18m
Talk
A Transferability Study of Interpolation-Based Hardware Model Checking to Software VerificationDistinguished Paper Award
Research Papers
Dirk Beyer LMU Munich, Po-Chun Chien LMU Munich, Marek Jankola LMU Munich, Nian-Ze Lee LMU Munich
DOI Media Attached
11:18
9m
Talk
CoqPyt: Proof Navigation in Python in the Era of LLMs
Demonstrations
Pedro Carrott Imperial College London, Nuno Saavedra INESC-ID and IST, University of Lisbon, Kyle Thompson University of California, San Diego, Sorin Lerner University of California at San Diego, João F. Ferreira INESC-ID and IST, University of Lisbon, Emily First University of California, San Diego
DOI Pre-print
11:27
9m
Talk
How We Built Cedar: A Verification-Guided Approach
Industry Papers
Craig Disselkoen Amazon Web Services, Aaron Eline Amazon, Shaobo He Amazon Web Services, Kyle Headley Unaffiliated, MIchael Hicks Amazon, Kesha Hietala Amazon Web Services, John Kastner Amazon Web Services, Anwar Mamat University of Maryland, Matt McCutchen , Neha Rungta Amazon Web Services, Bhakti Shah University of St. Andrews, Emina Torlak Amazon Web Services, USA, Andrew Wells Amazon Web Services
11:36
18m
Talk
Mission Specification Patterns for Mobile Robots: Providing Support for Quantitative Properties
Journal First
Claudio Menghi University of Bergamo; McMaster University, Christos Tsigkanos University of Bern, Switzerland, Mehrnoosh Askarpour McMaster University, Patrizio Pelliccione Gran Sasso Science Institute, L'Aquila, Italy, Gricel Vázquez University of York, UK, Radu Calinescu University of York, UK, Sergio García Volvo Cars Corporation, Sweden
11:54
18m
Talk
Rigorous Assessment of Model Inference Accuracy using Language Cardinality
Journal First
Donato Clun Imperial College London, Donghwan Shin University of Sheffield, Antonio Filieri AWS and Imperial College London, Domenico Bianculli University of Luxembourg
12:12
18m
Talk
Simulation-based Testing of Simulink Models with Test Sequence and Test Assessment Blocks
Journal First
Federico Formica McMaster University, Tony Fan McMaster University, Akshay Rajhans Mathworks, Vera Pantelic McMaster University, Mark Lawford McMaster University, Claudio Menghi University of Bergamo; McMaster University