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 surrounding the system. In this paper, we present a UML-based method to model the environment and to generate environment instances from the model. In our method, we can flexibly model the variation of the environment structures and the sequences of the function calls using class diagrams andstatechart diagrams. We also present a tool to automatically generate Promela/Spin scripts from the environment model. In this paper, we explain the details of our method and the verification of an RTOS design model using the tool.
- 2010-02-10
著者
-
Yatake Kenro
Japan Advanced Institute of Science and Technology
-
Nishibata Hirokazu
Japan Advanced Institute of Science and Technology
-
Aoki Toshiaki
Japan Advanced Institute of Science and Technology
関連論文
- Automatic Generation of Model Checking Scripts based on Environment Modeling
- Highly Reliable Embedded Software Development Using Advanced Software Technologies(Software Engineering for Embedded Systems)
- Extracting threads from concurrent objects for the design of embedded systems
- Automated Adaptor Generation for Behavioral Mismatching Services Based on Pushdown Model Checking
- On Optimization of Minimized Assumption Generation Method for Component-Based Software Verification
- On Optimization of Minimized Assumption Generation Method for Component-Based Software Verification