抄録/ポイント：
抄録/ポイント
文献の概要を数百字程度の日本語でまとめたものです。
部分表示の続きは、JDreamⅢ(有料)でご覧頂けます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。
近年,社会活動が情報システムへの依存度を増しているため,情報システムに対して一層の信頼性が求められている。しかし従来のシステム開発では,システム仕様を人手でレビューしており,設計不具合が設計工程から流出する可能性があった。さらにシステム試験では,流出した設計不具合を含む仕様を正しいとして試験するため,不具合を検出できない危険がある。したがってシステムの高信頼性を実現するには,システム仕様中の設計不具合を網羅的に摘出する必要がある。そこで三菱電機では,設計品質の向上を目的に,システム仕様を網羅的に自動検査するツール“Desimoc”を開発した。システム設計者は,Desimocに対してシステムの動作仕様と,システムが満たすべき検査項目を入力する。Desimocは入力された動作仕様を基に,システムとして起こり得る動作シナリオを網羅的に探索し,検査項目に反する動作シナリオを検出する。Desimocで扱う検査内容を次に示す。1)到達可能性(初期状態から特定状態に到達できる)。2)安全性(デッドロックや無限ループがない)。3)活性(いつか必ず特定状況が発生する)。4)公平性(各々の並行処理が必ず進む)。Desimocが網羅的に動作シナリオを探索するため,人手のレビューでは検出困難な設計不具合も検出可能である。今回,Desimocを開発済みシステム仕様に対して試行適用し,マニュアル運用で回復すべき稀(まれ)な異常動作を検出できた。この試行によってDesimocで設計不具合をなくし,システムの信頼性が向上することを確認した。(著者抄録)
