The experiences of developing the industrial-strength tools for modeling, testing and verification: a formal methods perspective
FM-related techniques are very helpful to ensure the quality of software. For instance, the model checking technique has been successfully applied in hardware/software verification and it becomes the key element for EDA tool chains. In this talk, I will share the experiences of developing the industrial-strength tools for modeling, testing and verification from the formal methods perspective. We will show how to find the real problems about testing and verification from the industry and also show how the formal methods can guide to solve these problems by developing tools. We will illustrate our experiences and insights by three interesting tools under development. The first one is a formal modeling and verification tool for the formal verification of Interlock system of the train, that is key part of signal systems in railway. The second one is a testing tool for embedded systems, where the symbolic execution technique plays an important role. The last one is a new model checking solver for hardware verification, and its performance is tuned effectively by the new observations on the search process in the state space. These tools are successfully applied in our industry partners and their effectiveness is also proved by large scale examples. Last but not least, we will also share the lessons we have learned during the tool development.