本論文では組込み用制御システムの中でも，プログラムの応答時間が被制御系 の時間的応答と同程度のシステムであるリーンリアルタイムシステム(lean real-time system) の設計を対象とした設計・検証支援に関する研究について 述べる. 我々はリーンリアルタイムシステムのプログラム構造やその特性を 明らかにし, プログラムモデルとして形式化した. それに基づいて『支 援システム: 組込み工房』を開発した. 本論文では, システム開発の中で 用いている手法およびアルゴリズムについて議論する.
組込み工房は, 『組込み型制御システムプロトタイプ用設計言語: Schetch/M とその処理系』, および, 『ソフトウェア文書管理システム: Liaison 』か ら構成される. 設計言語Schetch/M は, 連続時間上で考えられている制御ア ルゴリズと同等な動作を離散時間上で記述するためのプロトタイプ記述言語で ある. そのため設計言語Schetch/Mは組込み型制御システムのソフトウェアが 簡潔に記述できるように周期実行やイベント駆動実行の機能や実時間データ表 現の機能を持つ． 周期実行やイベント駆動実行を制御する部分のみ実時間と の関連を与え, プログラムの通常の逐次部分では実時間表現のためのデータ （実時間時系列型データ）を介してのみ実時間との関連を持つことによって, プログラム各部の時間遅れを考慮せずに機能定義できるようにしている点に特 徴がある. また, 処理系としては, Matlab/Simulinkプラットホームでのエディ タ, シミュレータと『Cソースコード合成システム: Spoon』を作成した. ソ フトウェア文書管理システムLiaisonは既存の文書を構造化文書に変換する機 能と, 参照時に各設計工程で検索のキーとなる関係によって文書の表示ビュー を構成する機能を持つ. 参照時のLiaison はWWW CGI(Common Gateway Interface)形式の関数群として実現され, その機能はWWWクライアントからの 参照要求に応えて, 必要な文書を工程に適した形式で表示する.
一方, 検証についてはシステム化の前提として実時間処理を時間オートマトン を使った形式的検証の有効性を調べた. 我々の用いた検証器および時間オー トマトンの記述方針によって, 組込み型制御システ ムの持つ実時間処理機能が形式的に証明可能となる.
我々は開発した支援システムの性能や導入効果を自動車制御用ソフト ウェアのプログラム設計工程で適用評価した. その結果, プログラムのプロ トタイプ工程では設計言語Schetch/Mと合成システムSpoonを組み合せることに よって, 設計言語Schetch/Mによるプロトタイプ記 述から製品と同等性能のハードウェアで動作する実行形式のプログラムを得る ことができる.
ソフトウェア文書管理システムLiaisonは複数の設計工程で適用実験を行っ た. その結果, プログラム構文要素レベルの文書要素を検索キーとすることが 有効であること, また, Liaison の文書管理方式は文書の内部表現や工程で の文書表示ビューの違いに対して最小限度の変更で対応できているこを明らか にした.
形式的検証については, 時間オートマトンの到達可能性判定を用いて自動車 制御用アルゴリズムの実時間プロパティを検証した. この手法はプログラム設 計工程に適用可能なシステム支援にまでは至らなかった. しかし, 検証支援 システムを組込み用ソフトウェアの検証に適用する要件を明らかにした. 時 間オートマトン記述を作成する上ではデータの扱いや入力アルファベットの時 系列集合の定義方法などに課題があることや, プログラム各部の実行遅延によっ て, システム全体が受ける動作上の影響に関するプロパティが検証対象として 有効であることを示した.