講演抄録/キーワード |
講演名 |
2005-06-23 14:15
状態遷移表における無効セルの検証方法 ○松本充広(福岡県産業・科学技術振興財団/九大)・山下直仁(福岡県産業・科学技術振興財団)・鈴木郁子(シャープ)・福田 晃(九大) |
抄録 |
(和) |
組み込みソフトウェアなどのシステムは,通常複数のサブシステム(タスク)から構成されている.各サブシステム(タスク)の状態遷移表を設計者が記述するとき,その中のセルの一部は無効セルと記述されるかもしれないが,組み合わせた全体のシステムではそのセルが無効セルになっていないという問題が生じる可能性がある.本研究では,状態遷移表検査ツールを用いてこの問題を発見する方法について議論する. |
(英) |
The system like embedded software is constructed from some subsystems (tasks). The state transition matrix of each subsystem (task) is specified by a designer. Some cells may be specified as invalid cells. From the view point of the whole system, some of those cells may not be invalid cells. In this paper, we discuss how to find this problem by using a stm check tool. |
キーワード |
(和) |
組み込みソフトウェア / 状態遷移表 / モデルチェッキング / / / / / |
(英) |
Embedded Software / State Transition Matrix / Model Checking / / / / / |
文献情報 |
信学技報, vol. 105, no. 128, SS2005-14, pp. 15-20, 2005年6月. |
資料番号 |
SS2005-14 |
発行日 |
2005-06-16 (SS) |
ISSN |
Print edition: ISSN 0913-5685 |
PDFダウンロード |
|