Automatic Generation of Model Checking Scripts Based on Environment Modeling

摘要

When applying model checking to the design models of the embedded systems, it is necessary to model not only the behavior of the target system but also that of the environment interacting with the system. In this paper, we present a method to model the environment and to automatically generate all possible environments from the model. In our method, we can flexibly model the structural variation of the environment and the sequences of the function calls using a class model and statechart models. We also present a tool to generate Promela scripts of SPIN from the environment model. As a practical experiment, we applied our tool to the verification of an OSEK/VDX RTOS design model.