Research in progress: Model Checking, for system explorers!
If, for the average person, it is difficult to find the common point between a Rover exploring Mars, the Parisian subway and a Rubik’s Cube, this is not the case for Model Checking specialists, and more particularly, the researchers at the Research and Development Laboratory of EPITA (LRDE), who will tell you that each of these entities represents a system to be explored.
Behind the scenes of the new video episode of the “Recherche en cours, EPITA Laboratoire d’innovation” (Research in progress, EPITA Laboratory of Innovation) series, this one dedicated to SPOT software, developed at the school, Alexandre Duret-Lutz, teacher-researcher at EPITA and head of the Automatons & Verification team at the LRDE, takes the time to explain what makes Model Checking an essential approach for computer science research today!
What does your work on Model Checking consist of?
I simply validate system behaviors. A system can be anything – a Rubik’s Cube, a program, a washing machine, a subway… – and each system develops its own behavior over time. My job is to examine all the possible futures of a system in order to verify that, for each branch of these futures, everything works well. It’s a bit like crash tests in the automotive world, where we send cars into a wall to see how they behave, except that these crash tests represent a certain cost, and they don’t allow us to test all possible scenarios. That is what makes Model Checking so interesting!
How does it work in theory?
To better explain this, we can take the Rubik’s Cube as an example. It has an initial configuration and can be rotated to change this configuration. These rotations are what we call “events”, which affect and modify the system. We can compare this to a “tree” of all possible futures, with multiple branches that, contrary to a classical tree, are not separated, in the sense that they eventually join each other – there are several ways of turning a Rubik’s Cube to return to the same configuration. We know that the configuration, which the Rubik’s Cube tree can reach is finite – for the 2x2x2 Rubik’s Cube, there are about 3 million configurations (or states, another term used). With Model Checking, the goal is to represent these 3 million configurations in the form of an “automaton”, i.e., a tree whose branches would have been bent so that they are attached to the places where the configurations end up being identical, and then to create algorithms able to walk through these 3 million states. Thus, these algorithms can explore all the potential paths from a given configuration to check the properties that interest us. In the case of the Rubik’s Cube, the properties we are interested in are, for example, to know if, from such or such configuration, we can solve the cube in less than N moves. If, instead of a Rubik’s Cube, we take the case of a subway line, it could be to know if an incoming passenger will succeed in exiting. This is what Model Checking is: making a model of the system, exploring the automaton (i.e., tree of futures) and hence all the behaviors of the system in order to check the safety properties of these behaviors. Let’s return to the example of the Rubik’s Cube 2x2x2… the 3 million configurations represent an infinite number of paths of infinite length – this is one of the characteristics of this puzzle: we can always rotate the faces! Model Checking allows us to verify that everything is going well on all paths and all possible behaviors.
Why is research essential in this area?
If I move to a bigger Rubik’s Cube like the classic 3x3x3 version – but there are bigger ones – then I have to represent 4×10¹⁹ configurations, which will not fit in the memory of a traditional computer. I then have to invent other, more advanced techniques to represent my automaton so that it will fit in that memory. This is a problem in Model Checking that we call “the explosion of the state space”: the bigger the systems we want to check, the more difficult it is to represent all of their possible configurations in memory. Based on the nature of the system, Model Checking techniques differ. As for me, I work on systems which are called “parallel” systems, with several processes that occasionally run at the same time on a computer, while exchanging messages. So, we can model communication protocols, like a client who wants to speak to a server – he would send a request, the server would answer, and we would check that for whatever request was sent, a response would be received in the future. We can also verify cryptographic protocols, to avoid possible flaws if X wants to send a message to Y and Z wants to intercept the message. At the LRDE, our research consists more broadly in improving all techniques used in Model Checking, in particular finding how to represent this immense state space even more efficiently by sharing memory and compressing data, how to explore this state space much more quickly by ignoring certain paths and how to represent the properties of the system.
Who uses Model Checking techniques?
As it allows for the analysis of all behaviors, one of the interests of Model Checking is to be able to modify a system in order to correct it, when we find a behavior that does not respect the safety property we wish to verify. Therefore, among the regular users of Model Checking, we find people who design critical systems, i.e., systems that can have a life or death impact on humans or are of extreme importance on a similar mission. When we are at these levels of criticality, we must do everything in our power to avoid these situations. We must therefore advance research to be able to verify these systems. Another approach would be to use simpler systems instead to facilitate these verifications, but the reality is that we are increasingly faced with using more and more complex systems. For example, at NASA, many parts of rockets and robots sent into space have been verified using Model Checking techniques. As research progresses, the techniques improve, which is important because the larger the system, the more time and memory it takes to verify it properly. For some systems, checking can take a day, a week, or even several months! Model Checking allows you to find as many bugs as possible – if there are any, of course.
The first 106 states of a state space for a small elevator model (which normally has 352 states) allows us to better visualize Model Checking
What do you enjoy most about research?
Without a doubt, the interactions with other researchers in the academic world. Indeed, many research teams work on Model Checking, like for example the team at Brno University in the Czech Republic with whom we have a special relationship and who share our interests, particularly in terms of automatons. I have quite a few colleagues abroad who work on subjects related to mine, and I know that they do not hesitate to use the algorithms that I develop. We also sometimes collaborate on the development of certain algorithms. These exchanges are always enriching, especially since research in Model Checking will never stop: we will always be looking for techniques that allow us to go faster, use less memory and check more and more complex systems and models.
Brno University of Technology
Speaking of exchanges, at the LRDE, you also occasionally work on different projects with EPITA students.
That’s right! At the moment, I am working with a student from EPITA who is trying to optimize a technique to reduce the automatons used to represent the properties we want to verify. To do this, he is trying to implement an algorithm developed by another research team in the most efficient way possible. Working on this subject allows him to learn new things while contributing to SPOT, our open source software in which we implement all our techniques. This gives him the opportunity to discover both the world of Model Checking and the world of automatons, but also to learn more about research, by becoming familiar with the daily life of researchers, learning to read and use scientific publications… Obviously, the students who join us also bring another viewpoint, and new relevant ideas. These are truly enriching moments in research!
SPOT software has a great reputation today. Is that something to be proud of?
Of course! All the Model Checking techniques we are working on are implemented in SPOT, free software distributed on the LRDE website. Anyone can download it and use it as they wish, but also contribute to the software by adding new features. Today, I am very happy to see SPOT being used by many people around the world, who use it to build even more complicated things! I am extremely proud of this software, although I am not the only one who developed it – colleagues and students are also working on it collectively. SPOT is recognized by the community. Getting feedback on software and seeing what people are doing with it always gives us lots of ideas for improving the tool. It’s something that we really enjoy!