Tsiplakiらの「EXPERIENCE WITH STATIC PLC CODE ANALYSIS AT CERN」をながしよみします。といいつつ、用語集を作ったら大体満足してしまったし、やってみた系の論文なのでそんなに内容はない。この界隈でどんな登場人物が出てくるかというまとめにはなった気がするので個人的には満足している。「この技法を産業応用してみたいぞ！」というときの参考にはなりそう。書誌情報はこちら:
@inproceedings{TsiplakiSpiliopoulou:2018avy,
author = "Tsiplaki Spiliopoulou, Christina and Blanco Viñuela,
Enrique and Fernández Adiego, Borja",
title = "{Experience with static PLC code analysis at CERN}",
booktitle = "{Proceedings, 16th International Conference on
Accelerator and Large Experimental Physics Control Systems
(ICALEPCS 2017): Barcelona, Spain, October 8-13, 2017}",
year = "2018",
pages = "THPHA160",
doi = "10.18429/JACoW-ICALEPCS2017-THPHA160",
SLACcitation = "%%CITATION = INSPIRE-1656449;%%"
}
用語集(しらべたり知ってることを書いたりしている。割と適当。)
- PLC: Programming Logic Controller。工場の機械を制御するのによく使われている制御装置(の規格？)。工業用や宇宙用の丈夫なArduinoだと思っている。このためのプログラミング言語*1があり、SiemensのSCLやSchneiderのSTといったものがある。もともとリレーをたくさん並べて機械を管理していたのをリッチにしていったらプログラミング言語になったみたいなやつらしい。この論文ではこの言語のことをPLC program languageとよんでいる。IEC 61131-3 標準規格で規格化されている。日本だとオムロンがやってるらしい。
- SCL: PLC用のプログラミング言語。Siemensが作っているらしい。CERNではSCLを使っていて、この論文もこちらを対象にする。
- UNICOS: UNified Industrial COntrol System。LHC(Large Hadron Collider, 大型ハドロン衝突型加速器)を制御するためのフレームワーク。この上でPLCの開発ができるらしい。 https://cds.cern.ch/record/1402490/files/WEPKS006.pdf?version=1
- static analysis: 静的解析。コードを解析して、そのコードを実際に実行することなくそのコードの性質(無限ループに落ちないかとか変なメモリ操作をしてないかとか)を調べること。プログラムの品質保証の技法としてよくテストなんかと対にされる。
- model checking: モデル検査。コードから数学的対象(大体ある種のオートマトン)を取り出して、その数学的対象を数学的に調べることでもとのコードの性質を調べる静的解析の一手法。コードについて網羅的に何かを調べることができてよい。
- PLCverif: PLC用のモデル検査器。CERNで作られたらしい。 http://ddarvas.web.cern.ch/ddarvas/publications/icalepcs2015/WEPGF092.pdf
- FB: function block。PLC言語での関数に相当するぽい。
- IM: intermediate representation。PLCverifはSCLのコードを一旦中間表現に変換する。
- CFG: control flow graph。オートマトンの一種で、普通の手続き型プログラムにオートマトン的な解析をしたいときは大体これに変換する。大体プログラムの各行がCFGの1状態に対応し、それらの遷移に条件分岐や代入の情報が載っていると思えばよいと思う。
- nuXmv: モデル検査器。https://nuxmv.fbk.eu/で公開されている。有名なモデル検査器としてNuSMVがあるが*2、これにSAT/SMTソルバとの連携をくっつけたものらしい。
- CBMC: C言語/C++用の有界*3モデル検査器。https://www.cprover.org/cbmc/から入手できる。Oxfordのグループが作っている。結構産業応用に意欲的で、そのために地味なことを高品質でやっているイメージがある。
- Xtext: プログラミング言語(特にDSL？)のための開発環境開発のためのフレームワークらしい。https://www.eclipse.org/Xtext/から入手できる。対象となるプログラミング言語の文法を書いてXtextに与えると、パーサ、コンパイラ、その言語のためのEclipse拡張、各種エディタ拡張が生成されるらしい。
アブストのアブスト
CERNで使われているPLCのやばそうなところを見つけるために、主に普通のプログラミング言語に使われている静的コード解析の技法を使ってみます。使ってみたツールややってみた経験を共有します。
内容
PLCverifを利用している。まずPLCverifの簡単な説明をしている。
PLCverifの説明
Figure2に書いてあるが、SCLのコードが与えられると、これは中間表現に変換される。このために、Xtext(というかXtextで生成されたツール)を使ってSCLコードをパースし、抽象構文木(AST)を得る。ASTの構造はFigure3に示されている。PLCverifには、このASTを解析するための「ルール」が定義されていて、その「ルール」に従っているか、あるいはviolateしているかを教えてくれるらしい。
適用例
この解析では、コードのやばい匂い(code smell)をみつけることを目的としていて、そのための「ルール」を検査している。この論文中ではうち2つの「UNICOS naming convention rule」と「Nested conditional if statements rule」を紹介している。
はじめの「UNICOS naming convention rule」は、変数名がUNICOSの命名規則(Table1)にしたがっているかを検査する。たとえば、Figure4のコード中の「AuMoSt」は、「Auto」をあらわす略語「Au」、「Mode」をあらわす「Mo」、「Status」をあらわす「St」を組合せたもので、これらの略称はちゃんと表のなかにあるので大丈夫だが、2行目の「E_FuStopI」は「Fu」が表にないので駄目である。
次の「Nested conditional if statements rule」は、深いIf文について警告を出すらしい。このルールはFigure5に示されている。
感想
タイトルで「Experience」と言っているとはいえもうちょっと検証の論文だと思っていたが、かなりソフトウェアエンジニアリングの論文でした。特に検証技法的に面白いところはなかったように思うのですが、エンジニアリング的には面白いんでしょうか…
よくわからんところ
- ここに書いてある「ルール」の検査だけだとCBMCもnuXmvもいらなそうなんですがどこで使ったんですか
英語的に勉強になったところ
- 「The large number of industrial control systems based on PLCs (Programmable Logic Controllers) available at CERN implies a huge number of programs and lines of code.」っていうんですが、implyに物理的な「含む」っていう意味あったんですか
