ソフトウェアの検証、すなわちソフトウェアが設計者の想定している通りに動作するかを調べる方法は大きく分けて２つあります。一つは、現在最も一般的な手法であるソフトウェアテストです。これはいろいろな状況で実際にソフトウェアを実行しておかしなことが起こっていないかを調べる手法です（動的テスト）。ここで問題になるのは、どのような状況で動作を調べるかです。ソフトウェアの動作を変える要因は入力の値とタイミングです。入力の値を変えるとソフトウェアの動作が変わることはわかります。ただ、入力の値が多い場合はテストのためにどの値を選ぶのが良いかの判断が難しいです。大抵の場合、時間の関係でテストできる値は全体のごくわずかです。さらに難しいのがタイミングです。タイミングとは、どのような順番でどの入力を行うかです。入力は人が行ったり、実行されているソフトウェア同士が通信や共有のメモリを介して行います。タイミングのパターンに関しては、その数の多さはさることながら、どのような種類があるのかを見定めることが非常に難しいです。テストでは、いろいろな観点から実行のパターンを分類して、各分類の中の一つのパターンを選んで実行テストを行います。従って、問題は実行のパターンをうまく整理し良い分類、すなわち不具合の原因が別になる分類を見つけることが肝要になります。

もう一つの方法は形式手法と呼ばれるものです（ここでは形式手法の代表であるモデル検査と呼ばれるものを念頭に話をします）。これも実際にはソフトウェアを実行するのですが、テストとは実行のさせ方が違います。ここでは、ソフトウェアの動作記述を抽象化した論理モデルに変換し、その論理モデルの中で実行/推論させて、おかしなことが起こっていないかを調べます。テストではソフトウェアの実行を分類、すなわち抽象化するのに対して、形式手法ではソフトゥエアを抽象化してから実行するという関係になっています。２つの手法は一見すると大きく隔たっているように見えますが、よくその中身を考えた時、抽象化という観点から見ると大差はありません。実際、最近ではこの２つの手法を組み合わせた方式も現れています。 　

ソフトウェアテストも形式手法もいろいろなテクニックや理論が展開されていますが、現時点ではそれだけで大きな威力を発揮出来る レベルまでには達していません。そのようなテクニックや理論を実際に役立てるにはまずソフトウェアを抽象化する能力が必要になります。 そして、良い抽象化の仕方は対象としているソフトウェアの形で大きく異なってきます。ここでいうソフトウェアとは 単なるコードのことではありません。要求仕様からコードに至るまでの階層化された設計のことです。 当社では、お客様のコードを単純に実行テストするのではなく、その設計をもとにお客様と一緒に 適切な抽象化の方法を考え、お客様のソフトウェア開発に適した抽象化のノウハウと検証ツールの使い方を 提供したいと考えています。お客様のニーズにあった適切な設計の手法が確立していない場合は、その手法も同時に検討したいと思います。

システムの不意な故障に自動で対処するための代表的な方式は２つあります。一つはシステムの状態を信頼できるメモリに定期的に保存しておき、故障が起こった時、最新の保存状態からやり直す（ロールバック）方式です。これは銀行の預金システムなど、古くから利用されている方式です。ただし近年、銀行の預金システムのように閉じたネットワークでなく、インターネットのような流動的な世界で様々なタイプのシステムを動かす場合が多くなおり、そのような状況に対応出来るロールバック方式を個々の場合に合わせて考える必要が出てきている。

もう一つの方式はシステムのコピーを複数台作り（レプリケーション）それらを同時に実行させ、その中の一台が故障した時に 残りのシステムのどれかがシームレスに作業を引き継ぐ方式です。このレプリケーションの方式を厳密に実現することは効率の面で問題があると考えられ、これまであまり普及していませんでした。しかし近年では計算機やネットワークの性能も上がり、効率面での問題がかなり解消され、様々な大手のクラウドシステムの基幹部に導入されるようになっています。特に、システムの故障の中でクラッカーの侵入によるものが大きく懸念される現在、重要な方式になっていくと考えられます。

ロールバック方式もリプリケーション方式も歴史が古く、これまでに実用、学術の両面で様々な技術・理論が数多く構築されています。 当社では、この分野における豊富な知識と実装経験をもとに、お客様のニーズにお合わせてこれらの技術の導入をお手伝いいたします。