 |
ミニ特集「安心・安全システム構築のための形式検証技術」家電機器，AV機器，通信機器から，自動車や航空機などの輸送機器，発電プラントなどに至るまで，広範囲に組込み制御システムが用いられている．しかし，組込みソフトウェアのバグによる，機器の不具合の発生が問題となっており，特に輸送機器や大規模プラントなどでは，人々の安全を脅かすことになりかねない． システムの安全性，性能の保証などの観点から，設計したシステムが仕様通りに動作するか否かを検証する必要がある．従来，想定される状況に対するテストにより，システムの動作検証を行うことが多かったが，より厳密に網羅的な検証を行うためには，数理的なアプローチが不可欠である．近年，そのような数理的アプローチとして形式検証が注目されている．形式検証に関しては，これまで情報工学の分野で多くの研究がなされてきた．しかし今後は，システム制御技術者も，制御則の導出だけでなく，それが組込みソフトウェアとして機器に実装された際の動作検証にまで関心をもつ必要があると考えられる．そういった意味で，形式検証は今後，システム制御などの分野においても重要な技術になってくると考えられる．形式検証で用いられる形式モデルとして，オートマトン，およびその拡張モデルなど離散事象システムモデルが適用されている．そこで，本企画では，形式検証には比較的なじみが薄いと思われる「計測と制御」の読者向けに，形式検証の入門的な解説に始まり，さまざまな離散事象システムモデルに基づく検証技術，検証技術による安心・安全システム構築への取組み，そして最後に検証技術の開発現場への導入事例について紹介する． |