抄録

○長田知之・原内　聡（三菱）

監視制御システムの生産性向上を阻害する要因の一つに，案件ごとの作りこみが発生することが挙げられる．監視制御システムによっては，案件特化の通信プロトコルを作りこむ必要がある．また通信プログラムは，送受信タイムアウトなどの例外が多い．このため，例外発生時に行うべき例外処理の漏れが発生する可能性がある．例外処理の漏れは，試験時に発見されることが多いため，工程の手戻り削減が課題になっている．本稿では，故障木図から，例外処理が適切に付加されているかを確認する線形時相論理式を導出する．例外処理が付加された通信シーケンスのモデルを記述し，モデルが式で示される性質を満たすか，モデル検査ツールで検査する．