モデル検査

NuSMVをUbuntu9.04にインストールしてみた

モデル検査を長くやっている人から、Spinより状態爆発に強いという話を聞いたので、もう一つのモデル検査ソフトウェアであるNuSMVを、Ubuntu9.04にインストールしてみた。

configureでつまづいたが、なんとかインストール成功だ。

早速、4日で学ぶ本の最初のサンプルを動かしてみた。

きちんと動いている。

Spinと違って、NuSMVにはGUIアプリケーションがないようだが、コマンドラインから動かすのも、すっきりしていて好きだ。

最初に取り組もうと思っているC言語のソースコードのモデル検査については、SPINの場合は、比較的簡単にC言語からPromela言語に変換できそうなのに対して、NuSMVの場合は、プログラムカウンタを表す変数を一つ作って、それで状態を表すといった一工夫が必要になるようだ。

Spinは並行プロセスの検証に強いという話も聞いているので、しばらくは両方のシステムを調べることになりそうだ。

★WOZ★

モデル検査 初級編―基礎から実践まで4日で学べる Book モデル検査 初級編―基礎から実践まで4日で学べる

著者:産業技術総合研究所システム検証研究センター
販売元:ナノオプトメディア
Amazon.co.jpで詳細を確認する

| | コメント (0) | トラックバック (0)

デバッグツールとしてのモデル検査ソフトウェア

こんな話を聞いた。
あるソフトウェア開発会社では、モデル検査ソフトウェアを強力なデバッグツールとして使っており、これまでの不具合解析では100%の欠陥検出率だそうだ。

また、その会社ではモデル検査により品質を向上させるとは、あえて言わないそうだが、この点では全く同意だ。
モデル検査対象のモデルのコードと、製品の実装コードが異なるので、製品の品質を直接向上させるとは言えないからだ。

あくまでも、ソフトウェア妥当性確認テストの前に、その時点で残ってしまった不具合を解析するのがモデル検査だという考え方だ。しかし将来的には、モデル検査を要求分析や基本設計段階にも適用したいと考えている。

ソフトウェア開発エンジニアの観点からは、モデル検査と従来の検証(レビューとテスト)の組み合わせは、開発者が、よりクリエイティブな作業に専念するための支援技術だ。現時点では導入にあたり制約があるものの、積極的に使っていきたい技術だ。

★WOZ★

| | コメント (0) | トラックバック (0)

モデル検査の課題~モデルの構築

モデル検査では、モデルの構築を容易にすることと状態爆発を防ぐことが重要だという。このうち、モデルの構築を容易にする方法として、例えば実装言語をC言語に特定し、さらに使える構文を限定するコーディング規約をつくり、その制約の下で開発を行うというものがある。
この方法は最初は不便だが、徐々に使える構文や言語を増やしていけば良いのではないか?
この方法はとても実践的だと思うし、実際こういう方法の実用化を目指す企業は多いようだ。

★WOZ★

| | コメント (0) | トラックバック (0)

捨てるプロトタイプと育てるプロトタイプ(2)

1月4日に捨てるプロトタイプと育てるプロトタイプの話を書いたが、Promelaで書いてSPINで動かすソフトウェアは典型的な「捨てるプロトタイプ」だ。

Promelaで書くソフトウェアは、UMLモデルや設計書、あるいは実装済みのソースコードにある、論理的に確認したい要素を取り出して抽象化したプロトタイプだ。

モデルや設計が論理的に正しいことを確認したり、実装済みのソースコードにあるバグを見つけた後は、捨ててしまう。

ただし、ここでいう「捨てる」というのは、製品には組み入れないという意味だ。Promelaで書いたプロトタイプは、モデル検証のエビデンスとして構成管理する。

モデル検証のエビデンスを構成管理するというのは、テストデータやテストコードを構成管理するというのと同じだ。

★WOZ★

| | コメント (0) | トラックバック (0)

SPINを使うモデル検査

「4日で学ぶモデル検査 初級編」の後、「SPINモデル検査」を読み、SPINの理論的な背景と動作の仕組み、およびSPINを現実の問題に適用する場合のケーススタディを学んだ。

この時点で、「4日で学ぶモデル検査 初級編」を始めて読んだ時のブログを読み返してみると、モデル検査を誤って理解していたことがわかる。

まず、モデル検査用の言語を、実装用の言語と同じようにみていた。次のように書いている。

//当時の記述1 ここから

SPINの場合、専用言語はPromelaなのだが、

・Promelaのコードから実装言語のコードを自動生成

・実装言語のコードからPromelaのコードを自動生成

することができれば、システム設計レベルでかなり使えるツールだと思う。

//ここまで

次に、設計時にすることが増える、あるいは、違う質の設計をしなければならないことが、導入を妨げるのではないかと漠然と感じていたようだ。

//当時の記述2 ここから

ただ、きちんと検証をするには、システム設計レベルで、モデルと検査項目の仕様を、Promelaなどのプログラミング言語で書く必要があるので、従来の、ワードやエクセルで設計文書を作るという、そういう設計スタイルに慣れている人には、受け入れにくいだろうな、とも思う。

//ここまで

今の理解では、まず言語については、モデル検査が対象とするのは、システムのある特徴を抽象化したモデルであるので、そのモデルを表現しやすいものであれば良いということだ。

SPINは、チャネルで通信する並行プロセスについて、到達性、進行性、線形時相論理を検証するツールであるので、それらを過不足なく表現できる言語であれば良い。それがPromelaというわけだ。そして、それはあくまでもシステムのある特徴を抽象化したものであるので、そのまま実装言語に変換したり、あるいは実装言語からPromelaに変換できる性質のものではない。

次に、設計で行う作業についてだが、SPINで行うモデル検査は、本来、設計時に行うべきことであり、それをやっていないことがバグにつながっているのだと理解した。つまり、システムのある特徴を抽象化したモデルを使って、設計が正しいことを検証する作業は、必要な作業なのだ。この作業は、現在でもUMLのモデルをレビューすることにより不完全であるが行っている。それをレビューではなくモデル検査という数学的手法で行おうというのだ。素晴らしい。

また一歩、モダンなソフトウェア開発に近づいたと感じている。

★WOZ★

| | コメント (0) | トラックバック (0)