化学プラントや工場などの重要インフラでは、PLC(Programable Logic Controller)やDCS(Distributed Control System)といった制御機器を用いて運転をしている(参考1)。 これらの機器はドメイン固有プログラミング言語を用いてプログラミングされる(参考2)が、静的コード解析の技術はまだ浸透していない。 著者らはASE 2012で、Arcade.PLCというPLC用の静的コード解析、モデル検査を行うツールについて発表しており(参考3)、追加機能の報告と言える。 なお、制御系プログラムの静的コード解析の困難さを、正統派ではないプログラミングの慣習：
今回は、プログラムの再起動後にのみ発生するプログラミングエラーの検知をPLC独自の課題としている。 具体的には、再起動後も値が保持されるRETAIN変数に由来するエラーに着目し、解析対象となるプログラムの制御フローを構築する際、再起動による遷移の可能性を網羅した形にし、解析を実施する。 著者らは、抽象解釈とコードのコンプライアンスチェックを行う軽量分析によりPLCの再起動時の挙動によるエラーを検知する機能拡張を実施、と表現している。 Arcade.PLC自体は、CTL model checkingの機能等がEclipseベースのGUIツールとして提供されている(参考5)。
(参考1)
ABBは、主要なPLCベンダーの一つ。
Global PLC Market in Power Industry 2015-2019 - Research and Markets ,
PLC Market in the Oil and Gas Industry in the Americas 2015-2019
(参考2)
国際標準化が進められており(IEC 61131-3 Programmable Controllers Part 3: Programming languages)、国内でもPLCopen Japanが普及促進活動を実施している。
(参考3)
Arcade.PLC: a verification platform for programmable logic controllers ASE 2012 Proceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering
(参考4)
Static Analysis of Industrial Controller Code using ARCADE.PLC
The Fifth Workshop on Tools for Automatic Program Analysis / September 10, 2014 / Munich, Germany
(参考5)
Arcade.PLCの公式サイト
(関連)
仏ALCATEL社、制御システム(PLC制御プログラム)に対してモデル検査手法を適用
http://formal.mri.co.jp/news/2013/06/alcatelplc.html