| タイトル | Practical Formal Verification of Diagnosability of Large Models via Symbolic Model Checking |
| 本文（外部サイト） | http://hdl.handle.net/2060/20030064186 |
| 著者（英） | Cavada, Roberto; Pecheur, Charles |
| 著者所属（英） | Research Inst. for Advanced Computer Science; NASA Ames Research Center |
| 発行日 | 2003-01-01 |
| 言語 | eng |
| 内容記述 | This document reports on the activities carried out during a four-week visit of Roberto Cavada at the NASA Ames Research Center. The main goal was to test the practical applicability of the framework proposed, where a diagnosability problem is reduced to a Symbolic Model Checking problem. Section 2 contains a brief explanation of major techniques currently used in Symbolic Model Checking, and how these techniques can be tuned in order to obtain good performances when using Model Checking tools. Diagnosability is performed on large and structured models of real plants. Section 3 describes how these plants are modeled, and how models can be simplified to improve the performance of Symbolic Model Checkers. Section 4 reports scalability results. Three test cases are briefly presented, and several parameters and techniques have been applied on those test cases in order to produce comparison tables. Furthermore, comparison between several Model Checkers is reported. Section 5 summarizes the application of diagnosability verification to a real application. Several properties have been tested, and results have been highlighted. Finally, section 6 draws some conclusions, and outlines future lines of research. |
| NASA分類 | Computer Programming and Software |
| レポートNO | RIACS-TR-03.03 |
| 権利 | Copyright, Distribution under U.S. Government purpose rights |
|
