ICST 2021
Mon 12 - Fri 16 April 2021
Tue 13 Apr 2021 15:00 - 15:30 at Porto de Galinhas - Models, Testing and Verification Chair(s): Mike Papadakis

Writing formal specifications often requires users to abstract from the original problem. Especially when verification techniques such as model checking are used. Without applying abstraction the search space the model checker need to traverse tends to grow quickly beyond the scope of what can be checked within reasonable time.

The downside of this need to omit details is that it increases the distance to the implementation. Ideally, the created specifications could be used to generate software from (either manually or automatically). But having an incomplete description of the desired system is not enough for this purpose.

In this work we introduce the REBEL2 specification language. REBEL2 lets the user write full system specifications in the form of state machines with data without the need to apply abstraction while still preserving the ability to verify non-trivial properties. This is done by allowing the user to forget and mock specifications when running the model checker. The original specifications are untouched by these techniques.

We compare the expressiveness of REBEL2 and the effectiveness of mock and forget by implementing two case studies: one from the automotive domain and one from the banking domain. We find that REBEL2 is expressive enough to implement both case studies in a concise manner. Next to that, when performing checks in isolation, mocking can speed up model checking significantly.

Tue 13 Apr

Displayed time zone: Brasilia, Distrito Federal, Brazil change

15:00 - 16:30
Models, Testing and VerificationResearch Papers at Porto de Galinhas
Chair(s): Mike Papadakis University of Luxembourg, Luxembourg
15:00
30m
Paper
Modeling with Mocking
Research Papers
Jouke Stoel CWI, Jurgen Vinju CWI, Netherlands, Tijs van der Storm CWI & University of Groningen, Netherlands
Pre-print
15:30
30m
Paper
Uncertainty-aware Exploration in Model-based Testing
Research Papers
Matteo Camilli Free University of Bozen-Bolzano, Angelo Gargantini University of Bergamo, Patrizia Scandurra University of Bergamo, Italy, Catia Trubiani Gran Sasso Science Institute
Pre-print
16:00
30m
Paper
Demystifying the Challenges of Formally Specifying API Properties for Runtime Verification
Research Papers
Leopoldo Teixeira Federal University of Pernambuco, Breno Miranda Federal University of Pernambuco, Henrique Rebelo Universidade Federal de Pernambuco, Marcelo d'Amorim Federal University of Pernambuco
Pre-print