図1: CPSの関連キーワード
ドイツagendaCPSで整理されたCPSのシステムイメージをベースとして、CPSの特徴的な性質ならびに信頼性向上を目的として研究が進められている技術の概要を紹介する。
CPSに関係する代表的なキーワードを図1に整理した。2つの観点で「学際的」であることがわかる。第1にシステム工学とコンピューティングが関わること(左右)、第2に欧州FP7-ICTチャレンジ領域の観点からサービス／ソフトウェアと組込みシステムが関わること(上下)である。ここでは、北米CPSフラワー(J. Wingによる)が示した3つ(「大容量、不確実なデータ」、「離散と連続」、「大規模化、複雑化への対応」)に「オープン性」を加えた4つを挑戦課題と考えて、図1を描いた。
図1: CPSの関連キーワード
最初に「オープン性」について少し考えてみる。SoSでは構成が動的に変化し、管理対象の範囲が刻一刻と変わるかもしれない。利用者を含む全体を対象としてシステムの機能や性質を論じる場合、人間の挙動、振る舞いを完璧に予測することは難しい。これを一般化すると、システム構築時に予測できない状況が存在するということになる。ソフトウェア開発の上流工程での技術は、システムの性質を如何にして精度よく予測できるか、に関わるといえる。たとえば、要求工学の目的は、システムに関わる様々なステークホルダが持つ「期待」を如何にして取りだすかである。聞き取りに失敗すると、開発の後工程で、要求機能の見直しが入ってしまう。一方で、要求を完璧に作ることは困難であり、さらに、システムへの要求は時と共に変化する。「システムのサービスイン後に起こる要求変化への対応」という課題解決から、要求の実行時監視や自己適応システムの研究がはじめられた。
自己適応あるいは自律システムといった考え方は耐故障でも重要であり、現在では大きな研究分野に成長している。拠り所とする技術背景の違いから、様々な呼び方をすることがあるが、最近では、self-* systemと総称することが多い。特に、インターネットを利用したサービス／ソフトウェアの技術として興味深い研究が世界的に続けられている。たとえば、文献[1]の研究がある。
CPSの関わりでのオープン性についての研究は今後の課題であろう。しかし、その重要性は十分に認識されているといえる。2010年初頭、北米で起きたトヨタに対する事件の後、車載ソフトウェアについて「信頼性(ディペンダビリティ)は説明責任(アカウンタビリティ)」である。利用者の誤使用も製造者の責任であり、その結果、誤使用を避けるような工夫の必要性が認識された。これは、ソフトウェアの技術では、要求仕様やモデリングに対応すると同時に、開発時に予測できない状況に対する実行時監視や実行時検証の技術を含む。
CPSフラワーの3つの挑戦課題を技術課題として整理する際には、対象を明確化する必要がある。本調査では昨年と同様にCPS型組込みシステムの課題(図1の下側)と捉える。以下では、CPS型組込みシステムが従来のハイブリッドシステムを、より一般化した計算系になっていることを述べ、最近の研究動向を紹介する。
本題に入る前に、「モデル」という言葉を再確認しておく。欧州(ArtistDesign)ではモデルベース開発と呼ぶ技術を中核に持ってこようとしており、関連文献を調査する際に正しい理解が必要になっている。図2に「モデル」の2つの使い方を図示した。「モデル」とは、具体的な対象を何らかの観点から抽象化して得られる記述のことである。どのような観点から抽象化するかは、モデルを作成する目的、モデルの使い方に依存する。
図2: 2つの「モデル」
図2の左側は、ソフトウェアの世界、特に、UMLの世界での「モデル」を説明する模式図である。UMLモデルとは、UMLで規定されているダイアグラム図式を用いた記述であって、プログラムを抽象化したものである。目的は、設計者間のコミュニケーション時の了解性向上にある。設計レビュー(読み合わせ)や流用可能性の検討を技術者が行う際に有用である。
一方、制御理論に端を発する組込みシステムでの「モデル」は制御対象装置(プラントと呼ぶ)などの物理的な実体を抽象化したものである。目的は、対象の時間的な振る舞いを予測することである。物理量の時間的な変化を論じるので、微分方程式系として表現されることが多い。ここでは、古典力学的描像と呼ぶことにする。物理学が教えるところによれば、すべての物理現象をこの描像で表現することが相応しいわけではない。統計的な描像が適切な場合もある。便宜上、後者を統計力学的描像と呼ぶ。いずれにしても、モデル化の対象は、物理学的な対象であり、その時間的な振る舞いを予測することがモデルの目的である。
CPS型組込みシステムでは、制御ソフトウェア(離散系)と制御対象プラント(連続系)の関係を議論することから、予測性(図2の右側)の「モデル」をベースに、離散系の考え方を導入した「ハイブリッドシステム」を取り扱う。以下では、産業界で標準的に用いられているSimulink/StateFlowが「モデル」の具体的な記述と考える。
図3: ハイブリッドシステム
図3にハイブリッドシステムの模式的な図を示した。プラント自身ならびに制御の方法は微分方程式系として表される。一方、制御ソフトウェアはプラント状態に応じて適切な制御の方法を選択できるようにモード切り替えの離散遷移を行う。このような「モデル」記述が与えられた時、シミュレーションによる振る舞いの確認(妥当性確認)、意図通りの振る舞いを示すように各種パラメータの初期値を決定(パラメータ設計)、エラー状態に至らないことを確認(安全性検査)、などを行って、作成した「モデル」の性質を確認する。ソフトウェア工学の観点から、これらの解析あるいは合成を行う技術の確立が重要となる。
Simulink/StateFlowの場合、数値計算シミュレーションが唯一の解析手段と考えられている。しかし、シミュレーションはプログラムのテスト実行と同じであり、非決定性を考慮した解析ができない。Simulink/StateFlowでは、初期状態の選択、プラントの偶発的故障などに起因するノイズ、が非決定性の要因となる。ソフトウェアの信頼性向上を考える立場からは、これらについての網羅性の高い解析を行いたい。シミュレーションだけが使える方法であれば、これを繰り返し用いることで(様々な初期状態を与えての実行することで)、パラメータ設計や安全性検査を行う。あきらかに、この方法は煩雑である。ここでは、形式検証の方法を用いる安全性検査、特に、アルゴリズミック検証の方法に限定して考える。対話的な証明技法は扱わない。
ハイブリッドシステムの安全性検査は1990年代初頭から研究が進められてきた。ハイブリッドシステムM、初期状態の集合I、安全な状態の集合Sが与えられた時、初期状態からはじまる全ての実行系列の状態がSに含まれることを調べる。記号安全性検査の方法は、n個の状態変数(実数値)が取り得る範囲をn次元の多角形で表し、状態遷移に伴う変化を、この多角形の変形として追跡することである。安全性検査の決定可能性は検査対象ハイブリッドシステムの表現力と関係する。ハイブリッドシステムMの記述要素は、ガード条件、変数更新、不変量、ダイナミックス、である．
安全性検査が決定可能なクラスとして、Alur-Dill時間オートマトン(TA)、線形ハイブリッドオートマトン(LHA)が知られている。いずれも、ガード条件、変数更新、不変量、は線形の式に限定するが、ダイナミックスが異なる。TAでは、クロック変数という時間微分すると定数になるという点で特別な変数を取り扱う。クロック変数が作るn次元矩形に着目して模倣等価なリージョン・オートマトンを構成する方法がある。実用的なモデル検査ツールとしてUPPAALがある。また、クロック制約やn次元矩形は差分論理(Difference Logic、DLと略す)で表現できる。DLは線形算術演算のサブクラスなので決定可能である。DLの決定手続きを持つSMTソルバを用いて有界モデル検査を実現することができる。一方、LHAのダイナミックスは1階微分に対する線形等式・不等式である。これに対しては、多角体(Polyhedra)を用いるHyTechがある。HybridSALは線形実数算術演算のSMTソルバYicesを用いるツールである。
一方、Simulink等のモデルでは線形微分方程式系(図3を参照)が必要になるが、安全性検査は決定不能問題である。線形ハイブリッドシステム(LHS)はLHAのダイナミックスを拡張して線形常微分方程式系を表現できるようにした。LHSでは多角体で状態の集合を記号表現することが不可能であることから、過大近似となる多角形を導入する。この方法を採用したツールCheckMateはSimulink/StateFlowサブセット（線形微分方程式）の解析に用いられた。
記号安全性検査の方法は、状態変数の個数に対して、スケーラビリティが悪い。様々な表現方法が工夫されているが、現状の「チャンピオンデータ」は28状態変数のLHSを扱ったSpaceExである。また、一般に、このような検証法では、抽象化の方法を導入することが考えられる。ハイブリッドシステムでは、離散系への抽象化、状態変数の次元の削減、非線形系を線形系に抽象化、など多様な方法が試みられている。一方、抽象化技法を用いる検証の結果について「安心感」を抱かない制御技術者も多いという。
以上、安全性検査のアルゴリズミック検証は多くの研究が進められたが、取り扱うことが可能なハイブリッドシステムのクラスが限定されることから、Simulink/StateFlowで表現された制御システム(図3)を対象とする自動検査の実用的な技術になっていない。計算可能性の原理的な壁がある。そこで、最近になって、シミュレーションと形式検証の方法を組み合わせる方向に研究が進んできている。
Simulink/StateFlowモデル記述の機能確認を行うシミュレーション支援ツールとして記号テスティングを用いる方法がある。Cプログラムを対象とした新しいテスティングに CONCOLIC(CONCrete SymbOLIC)と総称される方法が提案されている。動的テスティングとテストデータ自動生成を交互に行う方法で自動生成に記号的な方法(SMTツールなど)を用いる。これに触発された方法であって、Simulink/StateFlowシミュレーションの入力データ(初期値)生成を支援する方法であって、無駄なシミュレーション実行を行わないように実行経路カバレッジが向上するような入力データを選び出す。
最初に、Simulink/StateFlowシミュレーション実行を行って、離散変数値の実行履歴を離散時間ステップについて収集する。次に、(シミュレーションの)終了状態から逆像(inverse image)計算を記号的に行って初期時点まで戻る。得られた集合は、先と同じシミュレーション結果を導く初期状態の集まりとなるので、これらの要素を入力データとするシミュレーションを省略することができる。記号的な処理を行う方法としてLHSを用いるので、逆像計算は過小近似となる可能性がある。冗長な入力デ―タを排除できないかもしれないが見落とすことはない。ただし、Simulink/StateFlowからLHSへの変換が妥当なことが前提となる。
なお、Simulink/StateFlow記述を対象としたテストデータ自動生成ツールは、Reactis Testerなどの商用ツールがある。SimulinkあるいはStateFlowの記述要素に特化したカバレッジ基準やグラフカバレッジ基準を採用している。静的なカバレッジであり、粒度が粗い。
最初に欧州FP7-ICTのプロジェクトを2つ紹介する。1970年代から続く形式手法の研究成果をCPS型組込みシステムの設計支援に用いるというものである。形式手法を用いたモデルベース開発の流れとみることができる。
DESTECSはリアルタイム拡張されたVDM++(VDM-RT)を中心とする組込みシステムのモデルベース開発法とツールに関するプロジェクトである。コントローラ・プラントの考え方に基づき、コントローラに相当する制御ソフトウェアを開発する方法として、協調シミュレーション(Co-Simulation)を採用する。偶発的な故障を起こす装置に対する制御ソフトウェアの設計の妥当性を確認することを目的として、プラントに故障を埋め込む。
コントローラを実行可能設計言語VDM-RTで、またプラントを20-Simで記述する。ここで、20-SimはSimulink相当のシミュレーションシステムである。DESTECSは、比較的詳細な設計段階に適用する技術を目指す。コントローラはVDM-RTを用いた実行可能仕様記述であり、離散的な機能振る舞いに限定する。20-Simで作成したプラントを作動環境モデルとして流用すると考えても良い。協調シミュレーションの中心は、2つのシステム(VDM-RT、20-Sim)の実行あるいはシミュレーション進行の全体制御を行うフレームワークである。2010年1月から36ヵ月のプロジェクトとして実施されている。
ADVANCEはCPSを多様な構成要素からなるシステム、すなわち、SoSと見做し、全体構成を構築する方法を提供する。各々の構成要素は既存シミュレーションツールで作成されるとし、シミュレーションに必要な入力データの作成に形式手法(Event-B/ProB)による方法を採用する。全体システムをリファインメントに基づくモデリングで行い、構成要素に分解していく。構成要素の機能振る舞いは、個々のシミュレーションによって調べる。プロジェクトの成果は、モデルベース・テスティング(自動テスト生成)とシミュレーションツール統合フレームワークである。2011年10月から30ヵ月のプロジェクトとして実施されている。
上記の他にも協調解析の研究が進められている。文献[2]では、コントローラをSMTソルバYicesで形式検証し、プラントをSimulinkでシミュレーション実行する方法を論じている。2つの異なる解析系を協調させるという意味で、協調解析(Co-Analysis)である。偶発的な故障をSimulink記述に埋め込み、コントローラの故障耐性を解析するなどの応用を考えることができる。
Simulink/StateFlowモデル記述の安全性解析は3つの点で困難である。第1に、解析可能なクラスがLHSに限定されており、さらに検証結果は過大近似になる。第2に、Simulink/StateFlowの言語としての意味論が整備されていない。数値計算によるシミュレーション環境が動作意味を与える。したがって、Simulink/StateFlowをLHSに変換する標準的な方法がない。第3に、変換できたとしても、線形常微分方程式系(図3参照)に限定される。以上から、記号的な表現と解析法を用いないアプローチに期待が集まっている。ここでは、統計的モデル検査(Statistical Model-Checking)の考え方を紹介する。
最初に、関連する用語を整理する。個々の研究で言葉の使い方が若干異なるが、ここでは次のように考える。確率過程を対象とするモデル検査法を Stochastic Model-Checking、数値的な確率計算を用いるモデル検査法を Probabilistic Model-Checking(確率モデル検査)、経路のサンプリングに基づく統計的な推定を用いる方法を Statistical Model-Checking(統計的モデル検査)と呼ぶ。確率モデル検査と統計的モデル検査は、共に確率過程を対象とするモデル検査の方法であると考える。確率モデル検査は状態空間の記号的な表現とマルコフ連鎖確率の数値的な計算を組み合わせる方法で、代表的なツールとしてPRISMが知られている。
統計的モデル検査の基本的な考え方を紹介する。最初に問題設定を説明する。検査対象システムは確率的であるが決定性のある振る舞い(連続時間マルコフ連鎖など)を示す。検査性質は時間有界な時相論理とし、たとえば、「100秒以内に燃焼フロー速度が1秒の間0となる」を表す。具体的には、BLTL(Bounded Linear Temporal Logic)を用いて、
のように書き表す。今、検査対象システムを M とする時、統計的モデル検査の問題は、「確率過程Mが性質φを満たす確率を求めること」である。たとえば、確率モデル検査では、Mを遷移アークに確率を付与した状態遷移システムとする。確率的な要素を連続時間マルコフ連鎖などの具体的な「モデル」によって与える。
統計的モデル検査では、確率過程Mの(有限)実行列σが得られることだけを仮定する。 今、Ｂ 
(σ|=φ)とすると、成り立つ場合を1、成り立たない場合を0として、Ｂはベルヌーイ試行になる。Ｂが成り立つ確率(生起確率)pを求める問題なので、正規分布を基にした仮説検定を行う。仮説は、「M|=φが確率A以上で成り立つこと」として、試行(シミュレーションによる性質検査)を繰り返す。期待される有意水準で仮説が成り立つことが確認できるまで試行を順次続けていけば良い(Waldの方法)。応用事例では、103～105の試行を行っている。
この方法では、Simulink/StateFlowモデル記述が非線形性を持つ場合であっても、構成に確率的な要素があって、シミュレーションによって実行列を得ることができれば良い。上記の性質φは、センサの間欠故障をポアソン分布として表した燃焼制御のフォールトトレラントシステムをSimulink/StateFlowで表現した場合の例であった。通常のロジック・モデル検査の方法(確率モデル検査を含む)が、状態遷移システムの「モデル」を前提とする方法であるのに対して、実行列σを得る方法があれば良いという点で「モデルなし」のモデル検査ともいえる。また、これは自己適応システムにおける実行監視の方法と共通点がある。
なお、確率モデル検査の方法は、待ち行列システムの性能解析などに用いられた。統計的モデル検査は、離散シミュレータが利用できればよく、同様な応用に適用することも可能である。
Simulink/StateFlowモデル記述への応用を想定して、いくつかの方法を紹介した。安全性検査の問題は決定不能であることから、実行経路カバレッジを改善するシミュレーションデータを自動生成する記号的な方法や過大近似による検査の方法が工夫されている。いずれも性質検証よりは反例発見に重きをおいたアプローチである。これに対して、統計的モデル検査は、確率的であるが決定性を示す振る舞いを持つ対象に限定するが、与えられた性質が成り立つ確率を求める方法である。ところが、成り立つ確率を求めるということは、成り立たない確率を求めることでもある。なお、離散時間の有界解析の範囲で考えることが共通しており、これはシミュレーションを用いることから生じる。従来の並行システムに対するロジック・モデル検査とは趣が異なることがわかる。