最先端で使われはじめている仕様記述言語
情報処理推進機構のソフトウェア・エンジニアリング・センター（SEC）では、2007年から「高信頼性システム開発手法調査検討会」を開始している。この調査検討会の狙いは大学と産業界の委員がコラボレーションすることで、今後ますます社会にコンピュータが浸透していくときに必要となる高信頼システムの開発手法を具体化していくことである。
この調査検討会では2007年11月21日に最初の「高信頼性システム開発手法フォーラム」を企画しているのでその内容を簡単に紹介したい。
このフォーラムでは、筆者が調査検討会の活動状況を紹介して、九州大学の荒木 啓二郎教授から形式手法の適用事例について調査した内容を講演していただくこととなっている。形式手法とは、仕様記述言語によるソフトウェアの検証手法の1つである。ここでは、仕様記述言語を用いた形式手法を形式的仕様記述言語と定義する。
次いで、日本の産業界における形式手法の実践的な適用事例を、宇宙航空研究開発機構の片平 真史氏、フェリカネットワークスの栗田 太郎氏、富士ゼロックスの山本 訓稔氏から報告いただく予定だ。また米国の状況についてはThe Open GroupのJoseph I. Bergmann氏に紹介していただく。
その後、日本の適用事例を紹介していただいた方々に荒木教授とトヨタIT開発センターの見並 一明氏を加えて高信頼システム開発手法の将来についてパネル討論したいと考えている。
このように形式的仕様記述言語は、産業界への適用がいよいよ現実味を帯びてきている。本連載では、その中でも代表的な形式的仕様記述言語である「Z言語とVDM-SL」を取り上げて、その特徴を解説していく。また実際に適用する上での課題についても上述した調査検討会での議論なども参考にしながら紹介したい。
■形式的仕様記述言語の分類
形式的仕様記述言語を大きく分類すると、状態モデルに基づくVDM-SL、Z言語、Bなどと、プロセス代数などの代数的仕様に基づくLOTOS、OBJなどがある。
状態モデルに基づく仕様記述言語では、システムの性質をシステムの状態と操作に基づく2種類の条件式
状態モデルに基づく仕様記述言語の条件式
- 不変式：変数に関して常に成立する不変的な条件式である
- 事前条件と事後条件：システムの操作に関して、システムの入力状態に対して実行前に成立する条件が事前条件である。システム操作の実行後にシステムの出力状態に対して成立する条件が事後条件である
によって定義する。
代数的仕様記述言語では、システムを相互に通信するプロセスの集まりとしてモデル化する。代数的仕様記述では、抽象データ型ごとにそれを操作する関数仕様を方程式で記述する。
では、まず状態モデルに基づくZ言語ならびにVDM−SLを紹介し、次いでプロセス代数に基づくLOTOSを説明しよう。さらに、関連する仕様記述言語としてハードウェアの仕様記述に用いられるSpecCについても紹介していこう。 
次のページ
