Language Agnostic Model Checking for SDL
Emmanuel Gaudin, Eric Brunel, Mihal Brumbulli · 2023
SDL has been designed to describe communicating systems in a detailed and precise way. Due to its asynchronous nature, the behaviour is based on state machines running concurrently, making model checking of an SDL system a challenge. Creation and deletion of dynamic instances with PIDs randomly computed on the fly can create different system states that should be considered equivalent. The number of possible inputs creates such a number of system states that it is often too large to handle. Furthermore during exploration some internal variables, because of their values, might create new states while they actually do not influence the behavior of the system. Finally existing model checkers are based on their own language which is often not aligned with the modeling language, SDL for our concern. After four years of collaboration on several industrial projects, ENSTA Bretagne and PragmaDev came up with a new approach to system verification. In this paper we will present the result of this work. It combines four main ideas: 1) use an execution engine which is natively based on the modeling language and separated from the model checker 2) restrict the possible input values without modifying the system itself 3) identify internal variables that are irrelevant to the system state 4) re-assign PIDs and sort the instances to identify the system state.