仏ALCATEL社、制御システム(PLC制御プログラム)に対してモデル検査手法を適用
MRI
情報源
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.7195
概要
ALCATEL社とEcole Normale Supérieureの2つの研究機関は、制御システム用のPLCプログラムに対するモデル検査による検証手法を開発した。旋盤のツールホルダータレットの制御のためのPLCプログラムについて、IEC61131-3で規定される5つの制御プログラム言語のうち、Ladder Diagram(LD), Sequentional Function Chart(SFC), Structured Text(ST)の言語を対象として、モデル検査システムCadence-SMVを適用した。目的は、PLCプログラムの安全性、ライブネス(可用性に関する性質)、機能要求の時間的な性質を満たすことを検証することである。
視点
発表時点では、研究段階という位置付けである。制御システムのPLCプログラムについては高い安全性、信頼性が要求されるため、フォーマルメソッドによる論理的な検証は、費用対効果の面で有効と考えられる。
このページの先頭へ戻る