今年度は2つの実験を行った
CPS(Cyber-Physical Systems)型の組込みシステムは制御対象プラントと制御ソフトウェアが複雑に関係することから、設計物の整合性確認が難しいという問題がある。本研究では、ダイアグラムに基づく記法SysMLで表現されたモデリング記述から数値制約を抽出し、制約系の整合性を自動検査する方法を考察した。特に、自動検査エンジンとして Yices を用いて実験を行うことで提案方式を確認した。この研究によって、茨城大学上田研究室の修士学生加藤氏がESS2010優秀論文賞を受賞した。
組込みシステムの高機能化、大規模・複雑化に対応することが必要になり、開発上流工程でのモデリングが重要になってきている。IT系ソフトウェアで使われているUML系のダイアグラムに基づく記法を、組込みシステム開発でも利用するという目的から、SysML等が提案された。SysMLはUMLを拡張した記法と考えることができ、その特徴は、制御ソフトウェアの側面に加えて、制御対象となるハードウェアや機械部品の性質を表現できることにある。特に、部品を表すブロック、ブロック間に課される制約関係を表現したパラメトリック図等が新たに追加された。ソフトウェアと異なり、機械系やハードウェアの構成部品であるブロックは、その属性値間に方程式や制約式によって数値的な関係を表現することが多い。SysMLのダイアグラム記述の上からは、直接関連する属性間の局所的な制約条件に注力してモデリングすることができる。一方、システム全体としては、制約式の集まりが関わる。制約式の与え方によっては、もともと解が存在しないような場合を含むかもしれない。SysMLダイアグラムをみただけでは、制約式群が充足するかの判定が困難である。
本研究では、SysMLのパラメトリック図を中心とするいくつかのダイアグラムを入力とする時、制約式を自動抽出し、獲得した制約式系を自動検証エンジン(SMTソルバ)を用いて自動解析する方法を考察した。SMTソルバとしては米国SRIが公開している Yices を用いた。この方式検討と実験結果によって、茨城大学上田研究室の修士学生である加藤秀明氏が、情報処理学会組込みシステムシンポジウム2010(ESS2010)の優秀論文賞を受賞した[文献1]。
文献1で提案した方法のポイントを整理する。第1に、多種多様なSysMLダイアグラムの定義を調査し、制約記述を与えるブロック定義図とパラメトリック図の構成要素をYices言語要素に変換する方法を考案した。第2に、制約式の作成方法から、仮説となる制約式と検査対象の制約式を分離することが必要と判明した。たとえば、外部から与えるデータは仮説となる。今、仮説をP、検査対象をSとする時、検査制約はP→Sとなる。Yices は制約式を満たす時、その理由となるモデルを返す。そこで、検査制約を満たさない場合のモデルを得るためには、¬(P→S)=P∧(¬S)をYicesへの入力とする。SysMLダイアグラム中で解析時に¬をつける式をマーキングすることを目的として、UMLで採用されている標準的な拡張方法であるステレオタイプの技法を用いた。
実験では、具体例として、二輪型倒立振子ロボットを選び、SysML記述からYices記述への変換、ならびに Yices を用いた制約充足性検査を行った。初期値の与え方によって、充足しない、すなわち、システムが不安定になる(ロボットが倒れる)場合があることがわかった。