| タイトル | Analyzing Systems Dependent on Execution Speed with Model Checker |
| その他のタイトル | Analyzing Systems Dependent on Execution Speed with Model Checker |
| DOI | 10.1016/j.proeng.2012.10.059 |
| 参考URL | http://t2r2.star.titech.ac.jp/cgi-bin/publicationinfo.cgi?q_publication_content_number=CTT100658696 |
| 著者（日） | 水野, 孝久; 西崎, 真也 |
| 著者（英） | Mizuno, Takahisa; Nishizaki, Shin-ya |
| 発行日 | 2013-07-24 |
| 発行機関など | Elsevier |
| 刊行物名 | Procedia Engineering |
| 巻 | 50 |
| 開始ページ | 544 |
| 終了ページ | 554 |
| 刊行年月日 | 2012-11 |
| 言語 | en |
| 内容記述 | When computational resources are limited, system behavior depends on the execution speed of the processor(s). In such cases, it is difficult to exhaustively analyze system behavior via simulations. Model checking is a verification technique for reactive systems, which is widely used not only in academic research but also in industrial development. We describe a target system to be verified as a labeled transition system and its specification as temporal logic formulae. A model checker then automatically checks that the system satisfies the specification by exhaustively searching the execution paths. In this paper, we propose a technique for the exhaustive analysis of systems dependent on processor speed. We present a case study of a savings bank with an attached electronic coin counter controlled by a tiny microprocessor. We analyze the electronic savings bank using the SPIN model checker. The case study shows the effectiveness of this formal approach in finding the causes of troubles that depend on the execution speed. |
| キーワード | Model Checking; Fault Tolerance; Embedded System |
| 資料種別 | Conference Paper |
| ISSN | 1877-7058 |
| URI | https://repository.exst.jaxa.jp/dspace/handle/a-is/607615 |
