Advertisement
Published in:
2010 | OriginalPaper | Chapter
Automatic Generation of Model Checking Scripts Based on Environment Modeling
Authors : Kenro Yatake, Toshiaki Aoki
Published in: Model Checking Software
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.