ソフトウェアコンポーネントの信頼性評価方法および装置
【課題】ソフトウェアコンポーネントの仕様から、ソフトウェアコンポーネントにおける故障がどのように伝播するかを評価する技術を提供する。
【解決手段】モデルの形式検証機能を有するコンピュータが、ソフトウェアコンポーネントの入力インタフェース仕様、出力インタフェース仕様、内部仕様を含む仕様情報を取得する仕様情報取得ステップと、前記仕様情報中の入力インタフェース仕様を正常値以外に変更した仕様情報に従って、前記形式検証機能によって前記ソフトウェアコンポーネントを検証する検証ステップと、前記検証ステップにおいて前記出力インタフェース仕様を満足しない出力値となる例が発見された場合には、前記正常値以外に変更した入力と、前記出力インタフェース仕様を満たさない出力とを、対応づけて記憶する故障伝播路記憶ステップと、を実行する。
【解決手段】モデルの形式検証機能を有するコンピュータが、ソフトウェアコンポーネントの入力インタフェース仕様、出力インタフェース仕様、内部仕様を含む仕様情報を取得する仕様情報取得ステップと、前記仕様情報中の入力インタフェース仕様を正常値以外に変更した仕様情報に従って、前記形式検証機能によって前記ソフトウェアコンポーネントを検証する検証ステップと、前記検証ステップにおいて前記出力インタフェース仕様を満足しない出力値となる例が発見された場合には、前記正常値以外に変更した入力と、前記出力インタフェース仕様を満たさない出力とを、対応づけて記憶する故障伝播路記憶ステップと、を実行する。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ソフトウェアコンポーネントの信頼性を評価するための技術に関する。
【背景技術】
【０００２】
大規模なシステム開発では、一般的にソフトウェアを適当なサイズに分割してコンポーネント（ソフトウェアコンポーネント）を構成し、これらの組合せとしてソフトウェア全体を構成する方法が取られる。開発対象のシステムが非常停止装置などの安全に関するシステムである場合には、ソフトウェアにも高い信頼性が求められる。従来、このような安全システムにおけるソフトウェア開発では、開発プロセスの改善による品質向上によって、信頼性を高める手法が取られてきた。また、ソフトウェアアーキテクチャを対象とした信頼性評価が行われる場合でも、評価者が経験に基づいて評価を行うのが一般的であり、コンポーネントの内部構造を詳細に分析して評価を行うことは難しい。これらは手作業のために作業量が多く、また、技術者の経験に強く依存するという問題点もある。
【０００３】
これに対して、近年は数学をベースにした、形式的検証と呼ばれるシステム開発手法が取られるようになってきている。形式的検証では、仕様を数学的に記述し、コンピュータを用いて全ての状態を網羅して矛盾が無いか検査を行う。これらを自動化する技術としては、自動定理証明やモデル検査といった技術が研究されている。これらの技術では、自動で全ての条件や状態を調べるので、モデルの完全性が保障されるという利点がある。例えば、形式的検証ツールの一つであるAlloy Analyzerでは、集合論と述語論理を理論基盤に持ち、与えられた仕様に対して指定されたプロパティを満たす例を探したり（述語の検証）や指定されたプロパティを満たさない判例を探したり（表明の検証）することができる。
【先行技術文献】
【特許文献】
【０００４】
【特許文献１】特開２０１０−２３７８５５号公報
【発明の概要】
【発明が解決しようとする課題】
【０００５】
上記のような形式的検証によるモデル検査は、設計されたモデルが仕様を満足するかどうかを検証することに力点が置かれている。すなわち、ソフトウェアコンポーネントに異常な入力が与えられた場合、すなわち故障（バグ）が与えられた場合にどのように振る舞うのかを明確にすることはできない。外来の故障に対してソフトウェアコンポーネントがどのように振る舞うかが分かれば、故障がどのように伝播するかが分かる。このような情報は、システム全体の評価に用いることができ、例えば、安全性を損なうイベントがどのソフトウェアコンポーネントの故障（バグ）によって引き起こされる可能性があるか等を分析できる。
【０００６】
本発明は、ソフトウェアコンポーネントの仕様から、ソフトウェアコンポーネントにおいて故障がどのように伝播するかを評価することを目的とする。
【課題を解決するための手段】
【０００７】
本発明のソフトウェアコンポーネントの信頼性評価方法では、
モデルの形式検証機能を有するコンピュータが、
ソフトウェアコンポーネントの入力インタフェース仕様、出力インタフェース仕様、内部仕様を含む仕様情報を取得する仕様情報取得ステップと、
前記仕様情報中の入力インタフェース仕様を正常値以外に変更した仕様情報に従って、前記形式検証機能によって前記ソフトウェアコンポーネントを検証する検証ステップと、
前記検証ステップにおいて前記出力インタフェース仕様を満足しない出力値となる例が発見された場合には、前記正常値以外に変更した入力と、前記出力インタフェース仕様を満たさない出力とを、対応づけて記憶する故障伝播路記憶ステップと、
を実行する。
【０００８】
このように、入力インタフェース仕様を正常値以外に変更した仕様情報を用いて形式検証を行うことで、異常（故障）入力があった場合のソフトウェアコンポーネントの振る舞いを調べることができる。形式検証では、出力仕様を満たさない例（反例）を見つけることができる。ここで、どの出力から異常出力があるかを対応づけて記憶することで、異常値が入力された場合に、この異常がどの出力に伝播するかという情報を蓄積することができる。
【０００９】
本発明において、前記ソフトウェアコンポーネントは、複数の入力値をとるものであることが好ましく、
前記検証ステップでは、入力値のそれぞれについて、入力インタフェース仕様を正常値以外に変更した仕様情報に従って、ソフトウェアコンポーネントの検証を行うことが好ましい。
【００１０】
複数ある入力を１つずつ正常値以外とすることで、個々の異常入力がどの出力に伝播するかを把握することができる。
【００１１】
また、本発明において、前記コンピュータが、前記仕様情報取得ステップで取得した仕様情報から、入力値ごとに入力インタフェース仕様を正常値以外にした異常仕様情報を作成するステップ、をさらに含むことも好ましい。
【００１２】
仕様情報は形式検証機能が読み取り可能な形式でコンピュータに提供される。ここで、入力値ごとに入力インタフェース仕様を正常値以外にした異常仕様情報をコンピュータが自動的に作成することで、ユーザの手間を省くことができる。
【００１３】
また、本発明において、前記コンピュータが、
複数のソフトウェアコンポーネントを含むシステムの各ソフトウェアコンポーネントに対して、前記仕様情報取得ステップ、検証ステップ、故障伝播路記憶ステップを実行し、
前記故障伝播路記憶ステップにおいて関連づけて記憶された入力と出力とに基づいて、前記システムの故障伝播路を表示する、ことが好ましい。
【００１４】
個々のソフトウェアコンポーネントについて異常の伝播路を格納しているので、複数のソフトウェアコンポーネントから構成されるシステム全体に対して故障伝播路を表示することができる。これにより、あるソフトウェアコンポーネントで検出された異常の原因が、どのソフトウェアコンポーネントにあるのかをユーザが容易に理解できるようになる。
【００１５】
なお、本発明は、上記処理の少なくとも一部を行う信頼性評価方法、またはこの方法を実現するためのプログラムとして捉えることもできる。また、本発明は、上記処理を実行するための各手段を有する信頼性評価装置として捉えることもできる。上記手段および処理の各々は可能な限り互いに組み合わせて本発明を構成することができる。
【発明の効果】
【００１６】
本発明によれば、ソフトウェアコンポーネントの仕様から、ソフトウェアコンポーネントにおいて故障がどのように伝播するかを評価することができる。
【図面の簡単な説明】
【００１７】
【図１】本実施形態によるソフトウェアコンポーネントの信頼評価手法の概要。
【図２】本実施形態にかかるソフトウェアコンポーネントの信頼性評価装置の機能構成。
【図３】形式記述言語Ａｌｌｏｙで記述された仕様情報の例。
【図４】形式記述言語Ａｌｌｏｙで記述された異常仕様の例であり、図３の仕様情報から入力仕様の一部が正常値以外に変更されている。
【図５】本実施形態にかかるソフトウェアコンポーネントの信頼性評価処理のフローチャート。
【発明を実施するための形態】
【００１８】
以下に図面を参照して、この発明の好適な実施の形態を例示的に詳しく説明する。
【００１９】
図１は、本実施形態にかかる信頼性評価技術の概要を示す図である。ここでは、ｘとｙの２つを入力とし、ａ，ｂの２つを出力とするソフトウェアコンポーネント１００の信頼性を評価する場合を例として説明している。ソフトウェアコンポーネント１００の、インタフェース仕様および内部仕様を形式記述言語で記述し、まず第１段階としてこの仕様を基に、形式検証機能を用いて網羅的な検証を行う。これにより、ソフトウェアコンポーネント１００にインタフェース仕様および内部仕様に矛盾が無いことが検証される。このような検証方法が、一般的な形式検証機能の利用方法である。
【００２０】
本実施形態では、次に、入力仕様を正常値以外に変更する。なお、「正常値」というのは取得したインタフェース仕様で指定された値のことを言う。ここでは、ソフトウェアコンポーネント１００はｘとｙの２つの入力を取るが、いずれか１つの入力を正常値以外に変更する。このように変更した仕様情報に基づいて、形式検証機能を用いて網羅的な検証を行う。ここで、出力インタフェース仕様を満たさないようなインスタンス（反例）が見つかった場合には、仕様を変更した入力に対して異常（故障）が入力された場合に、上記の出力に故障が伝播しうることが分かる。図１では、入力ｙを正常値以外にした場合に、出力ａにおいて出力仕様を満たさない反例が存在することが分かる。従って、入力ｙに対する故障入力が出力ａに伝播することが分かる。
【００２１】
このようなソフトウェアコンポーネントに対する異常伝播解析を、システムを構成する複数ソフトウェアコンポーネントに対して実行して、故障伝播路を記憶部に記憶しておく。この解析結果から、ソフトウェアコンポーネント間での故障伝播路を計算可能である。すなわち、システム全体の信頼性も評価することが可能となる。
【００２２】
〈構成概要〉
図２は、本実施形態にかかる信頼性評価装置１の機能構成を示す図である。信頼性評価装置１は、ハードウェアとしては、ＣＰＵ、ＲＡＭなどの主記憶装置、ＨＤＤやＤＶＤ−ＲＯＭ等の補助記憶装置、キーボードやマウスなどの入力装置、ディスプレイなどの表示装置を含むコンピュータとして構成することができる。ＨＤＤなどに記憶されているオペレーティングシステム（ＯＳ）やアプリケーションプログラム（ＡＰ）がメモリ上に展開されてＣＰＵが実行することで、図２に示す各機能部が実現される。ここでは、一台のコンピュータから信頼性評価装置１が構成される場合の例を説明したが、ネットワーク等を介して接続された複数のコンピュータが連動することで信頼性評価装置１が構成されても良い。また、各機能部の一部または全部を専用のハードウェアによって構成してもかまわない。
【００２３】
仕様情報取得部２は、形式記述言語で記述された仕様情報を信頼性評価装置１へ取り込
むための機能部である。図３に形式記述言語Ａｌｌｏｙで記述された仕様情報の例を示している。仕様情報の取得方法は種々の態様が考えられる。例えば、ＨＤＤやＤＶＤ−ＲＯＭなどに格納されている仕様情報ファイルを読み込んで取得することが考えられるし、ネットワークを経由して仕様情報ファイルを取得することが考えられる。また、ユーザが入力装置から直接入力してもかまわない。また、アーキテクチャ記述言語（ＡＤＬ）等で記述された設計情報を取得し、この設計情報から自動的に生成してもかまわない。ＡＤＬで記述された設計情報から形式記述言語で記述された仕様情報を作成することは、当業者であれば容易に理解できるであろう。
【００２４】
異常仕様作成部３は、仕様情報取得部２が取得した仕様情報のうち、いずれかの入力を正常値以外にした仕様情報（以下、異常仕様と呼ぶ）を作成する機能部である。図４に形式記述言語Ａｌｌｏｙで記述された異常仕様の例を示している。異常仕様は、正常仕様における入力インタフェースの制約のうちの一つを反転する（論理否定演算）ことにより作成することができる。なお、入力が取り得る値の範囲が指定されていれば、正常な入力を反転することで一意の異常仕様が得られる。
【００２５】
モデル検査部４は、形式記述言語で記述された仕様（モデル）が満たされるかどうかを、数学的手法により網羅的に検証する機能部である。モデル検査部４としては、Ａｌｌｏｙ Ａｎａｌｙｚｅｒなどの既知のモデル検査ツールを利用することができる。
【００２６】
故障伝播路記憶部５には、異常仕様に基づいてモデル検査を行った場合に出力インタフェース仕様を満たさない出力を、異常な入力と関連づけて記憶する記憶部である。例えば、入力ｙと出力ａを関連づけて記憶することで、入力ｙに異常な入力があった場合に出力ａに故障が伝播する可能性があることが分かる。この情報は、システムの信頼性評価に用いることができる。
【００２７】
故障伝播路表示部６は、故障伝播路記憶部５に記憶されている各ソフトウェアコンポーネントの故障伝播路と、システムを構成するソフトウェアコンポーネント間の接続関係とから、システム全体にわたる故障伝播路を表示部に表示させるための機能部である。
【００２８】
〈仕様記述〉
図３は、図１に示してある入出力インタフェースおよび内部仕様を形式記述言語Ａｌｌｏｙで記述したものである。ここでは、非常に単純な場合を例に採用しているが、より複雑な仕様も記述できる。例えば、複数の出力が同時に取るべき値の条件や、ある出力の時系列的な制約などを記述しても良いし、また、ソフトウェアコンポーネントの内部状態に依存して正常値の範囲が変わるようにしても良い。
【００２９】
図４は、図３に示す仕様を基に異常仕様作成部３が作成した異常仕様である。図４は、入力のうちｙ（ＩｎＹ）を正常値以外に変更した場合の異常仕様である。基本的に、正常な仕様のうち入力に関する制約に対して論理否定を作用させることで、異常仕様の作成ができる。
【００３０】
〈処理フロー〉
図５は、本実施形態におけるソフトウェアコンポーネントの信頼性評価処理方法の流れを示すフローチャートである。図５は、一つのソフトウェアコンポーネント、すなわち、一つの仕様記述に対する信頼性評価のフローである。
【００３１】
ステップＳ２において、仕様情報取得部２が検査対象ソフトウェアコンポーネントのインタフェース仕様情報（正常仕様）を取得する。典型的には仕様記述ファイルの読み込みであるが、ＡＤＬ等で記述された設計情報から自動的に仕様記述ファイルを作成してもか
まわない。
【００３２】
ステップＳ４では、取得した正常仕様情報に基づいて、モデル検査部４を用いて網羅的な検証によるモデル検査を行う。これにより、インタフェース仕様として記述された要件をソフトウェアコンポーネントが満足するか否かが検証される。これは、従来のモデル検査部（Ａｌｌｏｙ Ａｎａｌｙｚｅｒ等）の利用方法である。この時点で反例が発見された場合には、仕様を再考する。
【００３３】
ステップＳ６においてソフトウェアコンポーネントの入力のうち１つを選択し、ステップＳ８において選択した入力の仕様を正常値以外を示すように変更した異常仕様を異常仕様作成部３が作成する。ステップＳ１０で、作成した異常仕様を用いてモデル検査を行う。このモデル検査の結果として、反例が見つかったか場合（Ｓ１２−ＹＥＳ）は、ステップＳ１４で、正常値以外にした入力と仕様を満たさない出力とを関連づけて、故障伝播路記憶部５に記憶する。例えば、入力ｙと出力ａとを関連づけて記憶する。
【００３４】
ステップＳ１６で、このソフトウェアコンポーネントについて、全ての入力について入力仕様を正常値以外にしたか判断し、まだ正常値以外にしていない入力がある場合にはステップＳ６に戻る。次回の検査では、新たな入力だけを正常値以外にした異常仕様を作成する。例えば、入力ｘのみを正常値以外にしてモデル検査を行った後は、入力ｙのみを正常値以外にして、入力ｘについては正常な仕様にしてモデル検査を行う。全ての入力について正常値以外にしたモデル検査を実行した後は、このソフトウェアコンポーネントについての信頼性評価を終了する。
【００３５】
このソフトウェアコンポーネントの信頼性評価は、一つのみのコンポーネントに対して行うだけでなく、システムを構成する複数のコンポーネントに対して順次行うことも好ましい。すなわち、各ソフトウェアコンポーネントに対して、図５のフローチャートに示す処理、具体的には、仕様情報の取得、異常仕様の作成、異常仕様に基づくモデル検査、および故障伝播路の記憶を実行する。その結果、各ソフトウェアコンポーネントについて、故障伝播路となる入力と出力の組合せが故障伝播路記憶部５に格納される。
【００３６】
このようにして各ソフトウェアコンポーネントに対して異常の伝播路が算出されると、故障伝播路記憶部５に関連づけて記憶された入力と出力に基づいて、システム全体における故障伝播路を把握することができる。例えば、故障伝播路表示部６は、ある個所で発生した故障がどのように伝播するかを表示することができる。また、故障伝播路表示部６は、ある個所で検出された故障の真の原因となり得る個所を表示することもできる。このように、故障に対してシステム全体がどのように振る舞うかを明確にすることができるので、複数のソフトウェアコンポーネントから構成されるシステム（ソフトウェア）全体の評価にも用いることができる。例えば、安全性を損なうようなイベントが、どのソフトウェアコンポーネントの故障（バグ）によって引き起こされる可能性があるか等を分析できる。
【００３７】
〈変形〉
ここでは、形式記述言語としてＡｌｌｏｙ、モデル検査ツールとしてＡｌｌｏｙ Ａｎａｌｙｚｅｒを例として説明したが、入力仕様、内部仕様、出力仕様を記述可能であり、数学的手法によって上記の仕様が満足するかどうかを検証可能なツールであれば、任意の手法を採用することができる。たとえば、ＳＰＩＮ、Ｐｒｏｍｅｌａ、ＳＭＶ，ＬＴＳＡなどを利用可能である。
【００３８】
上記の説明では、取得した仕様に基づくモデル検査（図５のステップＳ４）と、入力を正常値以外に変更した仕様に基づくモデル検査（図５のステップＳ１０）の両方を行って
いるが、前者は必ずしも行わなくてもかまわない。すなわち、作成した仕様が無矛盾であることが保障されているならば、異常仕様に基づくモデル検査のみを行って故障がどのように伝播するかだけを調べてもかまわない。
【００３９】
また、上記では入力を一つずつ異常に設定する場合のみを説明したが、複数の入力を同時に異常に設定してモデル検査を行ってもかまわない。
【符号の説明】
【００４０】
１ 信頼性評価装置
２ 仕様情報取得部
３ 異常仕様作成部
４ モデル検査部
５ 故障伝播路記憶部
６ 故障伝播路表示部
【技術分野】
【０００１】
本発明は、ソフトウェアコンポーネントの信頼性を評価するための技術に関する。
【背景技術】
【０００２】
大規模なシステム開発では、一般的にソフトウェアを適当なサイズに分割してコンポーネント（ソフトウェアコンポーネント）を構成し、これらの組合せとしてソフトウェア全体を構成する方法が取られる。開発対象のシステムが非常停止装置などの安全に関するシステムである場合には、ソフトウェアにも高い信頼性が求められる。従来、このような安全システムにおけるソフトウェア開発では、開発プロセスの改善による品質向上によって、信頼性を高める手法が取られてきた。また、ソフトウェアアーキテクチャを対象とした信頼性評価が行われる場合でも、評価者が経験に基づいて評価を行うのが一般的であり、コンポーネントの内部構造を詳細に分析して評価を行うことは難しい。これらは手作業のために作業量が多く、また、技術者の経験に強く依存するという問題点もある。
【０００３】
これに対して、近年は数学をベースにした、形式的検証と呼ばれるシステム開発手法が取られるようになってきている。形式的検証では、仕様を数学的に記述し、コンピュータを用いて全ての状態を網羅して矛盾が無いか検査を行う。これらを自動化する技術としては、自動定理証明やモデル検査といった技術が研究されている。これらの技術では、自動で全ての条件や状態を調べるので、モデルの完全性が保障されるという利点がある。例えば、形式的検証ツールの一つであるAlloy Analyzerでは、集合論と述語論理を理論基盤に持ち、与えられた仕様に対して指定されたプロパティを満たす例を探したり（述語の検証）や指定されたプロパティを満たさない判例を探したり（表明の検証）することができる。
【先行技術文献】
【特許文献】
【０００４】
【特許文献１】特開２０１０−２３７８５５号公報
【発明の概要】
【発明が解決しようとする課題】
【０００５】
上記のような形式的検証によるモデル検査は、設計されたモデルが仕様を満足するかどうかを検証することに力点が置かれている。すなわち、ソフトウェアコンポーネントに異常な入力が与えられた場合、すなわち故障（バグ）が与えられた場合にどのように振る舞うのかを明確にすることはできない。外来の故障に対してソフトウェアコンポーネントがどのように振る舞うかが分かれば、故障がどのように伝播するかが分かる。このような情報は、システム全体の評価に用いることができ、例えば、安全性を損なうイベントがどのソフトウェアコンポーネントの故障（バグ）によって引き起こされる可能性があるか等を分析できる。
【０００６】
本発明は、ソフトウェアコンポーネントの仕様から、ソフトウェアコンポーネントにおいて故障がどのように伝播するかを評価することを目的とする。
【課題を解決するための手段】
【０００７】
本発明のソフトウェアコンポーネントの信頼性評価方法では、
モデルの形式検証機能を有するコンピュータが、
ソフトウェアコンポーネントの入力インタフェース仕様、出力インタフェース仕様、内部仕様を含む仕様情報を取得する仕様情報取得ステップと、
前記仕様情報中の入力インタフェース仕様を正常値以外に変更した仕様情報に従って、前記形式検証機能によって前記ソフトウェアコンポーネントを検証する検証ステップと、
前記検証ステップにおいて前記出力インタフェース仕様を満足しない出力値となる例が発見された場合には、前記正常値以外に変更した入力と、前記出力インタフェース仕様を満たさない出力とを、対応づけて記憶する故障伝播路記憶ステップと、
を実行する。
【０００８】
このように、入力インタフェース仕様を正常値以外に変更した仕様情報を用いて形式検証を行うことで、異常（故障）入力があった場合のソフトウェアコンポーネントの振る舞いを調べることができる。形式検証では、出力仕様を満たさない例（反例）を見つけることができる。ここで、どの出力から異常出力があるかを対応づけて記憶することで、異常値が入力された場合に、この異常がどの出力に伝播するかという情報を蓄積することができる。
【０００９】
本発明において、前記ソフトウェアコンポーネントは、複数の入力値をとるものであることが好ましく、
前記検証ステップでは、入力値のそれぞれについて、入力インタフェース仕様を正常値以外に変更した仕様情報に従って、ソフトウェアコンポーネントの検証を行うことが好ましい。
【００１０】
複数ある入力を１つずつ正常値以外とすることで、個々の異常入力がどの出力に伝播するかを把握することができる。
【００１１】
また、本発明において、前記コンピュータが、前記仕様情報取得ステップで取得した仕様情報から、入力値ごとに入力インタフェース仕様を正常値以外にした異常仕様情報を作成するステップ、をさらに含むことも好ましい。
【００１２】
仕様情報は形式検証機能が読み取り可能な形式でコンピュータに提供される。ここで、入力値ごとに入力インタフェース仕様を正常値以外にした異常仕様情報をコンピュータが自動的に作成することで、ユーザの手間を省くことができる。
【００１３】
また、本発明において、前記コンピュータが、
複数のソフトウェアコンポーネントを含むシステムの各ソフトウェアコンポーネントに対して、前記仕様情報取得ステップ、検証ステップ、故障伝播路記憶ステップを実行し、
前記故障伝播路記憶ステップにおいて関連づけて記憶された入力と出力とに基づいて、前記システムの故障伝播路を表示する、ことが好ましい。
【００１４】
個々のソフトウェアコンポーネントについて異常の伝播路を格納しているので、複数のソフトウェアコンポーネントから構成されるシステム全体に対して故障伝播路を表示することができる。これにより、あるソフトウェアコンポーネントで検出された異常の原因が、どのソフトウェアコンポーネントにあるのかをユーザが容易に理解できるようになる。
【００１５】
なお、本発明は、上記処理の少なくとも一部を行う信頼性評価方法、またはこの方法を実現するためのプログラムとして捉えることもできる。また、本発明は、上記処理を実行するための各手段を有する信頼性評価装置として捉えることもできる。上記手段および処理の各々は可能な限り互いに組み合わせて本発明を構成することができる。
【発明の効果】
【００１６】
本発明によれば、ソフトウェアコンポーネントの仕様から、ソフトウェアコンポーネントにおいて故障がどのように伝播するかを評価することができる。
【図面の簡単な説明】
【００１７】
【図１】本実施形態によるソフトウェアコンポーネントの信頼評価手法の概要。
【図２】本実施形態にかかるソフトウェアコンポーネントの信頼性評価装置の機能構成。
【図３】形式記述言語Ａｌｌｏｙで記述された仕様情報の例。
【図４】形式記述言語Ａｌｌｏｙで記述された異常仕様の例であり、図３の仕様情報から入力仕様の一部が正常値以外に変更されている。
【図５】本実施形態にかかるソフトウェアコンポーネントの信頼性評価処理のフローチャート。
【発明を実施するための形態】
【００１８】
以下に図面を参照して、この発明の好適な実施の形態を例示的に詳しく説明する。
【００１９】
図１は、本実施形態にかかる信頼性評価技術の概要を示す図である。ここでは、ｘとｙの２つを入力とし、ａ，ｂの２つを出力とするソフトウェアコンポーネント１００の信頼性を評価する場合を例として説明している。ソフトウェアコンポーネント１００の、インタフェース仕様および内部仕様を形式記述言語で記述し、まず第１段階としてこの仕様を基に、形式検証機能を用いて網羅的な検証を行う。これにより、ソフトウェアコンポーネント１００にインタフェース仕様および内部仕様に矛盾が無いことが検証される。このような検証方法が、一般的な形式検証機能の利用方法である。
【００２０】
本実施形態では、次に、入力仕様を正常値以外に変更する。なお、「正常値」というのは取得したインタフェース仕様で指定された値のことを言う。ここでは、ソフトウェアコンポーネント１００はｘとｙの２つの入力を取るが、いずれか１つの入力を正常値以外に変更する。このように変更した仕様情報に基づいて、形式検証機能を用いて網羅的な検証を行う。ここで、出力インタフェース仕様を満たさないようなインスタンス（反例）が見つかった場合には、仕様を変更した入力に対して異常（故障）が入力された場合に、上記の出力に故障が伝播しうることが分かる。図１では、入力ｙを正常値以外にした場合に、出力ａにおいて出力仕様を満たさない反例が存在することが分かる。従って、入力ｙに対する故障入力が出力ａに伝播することが分かる。
【００２１】
このようなソフトウェアコンポーネントに対する異常伝播解析を、システムを構成する複数ソフトウェアコンポーネントに対して実行して、故障伝播路を記憶部に記憶しておく。この解析結果から、ソフトウェアコンポーネント間での故障伝播路を計算可能である。すなわち、システム全体の信頼性も評価することが可能となる。
【００２２】
〈構成概要〉
図２は、本実施形態にかかる信頼性評価装置１の機能構成を示す図である。信頼性評価装置１は、ハードウェアとしては、ＣＰＵ、ＲＡＭなどの主記憶装置、ＨＤＤやＤＶＤ−ＲＯＭ等の補助記憶装置、キーボードやマウスなどの入力装置、ディスプレイなどの表示装置を含むコンピュータとして構成することができる。ＨＤＤなどに記憶されているオペレーティングシステム（ＯＳ）やアプリケーションプログラム（ＡＰ）がメモリ上に展開されてＣＰＵが実行することで、図２に示す各機能部が実現される。ここでは、一台のコンピュータから信頼性評価装置１が構成される場合の例を説明したが、ネットワーク等を介して接続された複数のコンピュータが連動することで信頼性評価装置１が構成されても良い。また、各機能部の一部または全部を専用のハードウェアによって構成してもかまわない。
【００２３】
仕様情報取得部２は、形式記述言語で記述された仕様情報を信頼性評価装置１へ取り込
むための機能部である。図３に形式記述言語Ａｌｌｏｙで記述された仕様情報の例を示している。仕様情報の取得方法は種々の態様が考えられる。例えば、ＨＤＤやＤＶＤ−ＲＯＭなどに格納されている仕様情報ファイルを読み込んで取得することが考えられるし、ネットワークを経由して仕様情報ファイルを取得することが考えられる。また、ユーザが入力装置から直接入力してもかまわない。また、アーキテクチャ記述言語（ＡＤＬ）等で記述された設計情報を取得し、この設計情報から自動的に生成してもかまわない。ＡＤＬで記述された設計情報から形式記述言語で記述された仕様情報を作成することは、当業者であれば容易に理解できるであろう。
【００２４】
異常仕様作成部３は、仕様情報取得部２が取得した仕様情報のうち、いずれかの入力を正常値以外にした仕様情報（以下、異常仕様と呼ぶ）を作成する機能部である。図４に形式記述言語Ａｌｌｏｙで記述された異常仕様の例を示している。異常仕様は、正常仕様における入力インタフェースの制約のうちの一つを反転する（論理否定演算）ことにより作成することができる。なお、入力が取り得る値の範囲が指定されていれば、正常な入力を反転することで一意の異常仕様が得られる。
【００２５】
モデル検査部４は、形式記述言語で記述された仕様（モデル）が満たされるかどうかを、数学的手法により網羅的に検証する機能部である。モデル検査部４としては、Ａｌｌｏｙ Ａｎａｌｙｚｅｒなどの既知のモデル検査ツールを利用することができる。
【００２６】
故障伝播路記憶部５には、異常仕様に基づいてモデル検査を行った場合に出力インタフェース仕様を満たさない出力を、異常な入力と関連づけて記憶する記憶部である。例えば、入力ｙと出力ａを関連づけて記憶することで、入力ｙに異常な入力があった場合に出力ａに故障が伝播する可能性があることが分かる。この情報は、システムの信頼性評価に用いることができる。
【００２７】
故障伝播路表示部６は、故障伝播路記憶部５に記憶されている各ソフトウェアコンポーネントの故障伝播路と、システムを構成するソフトウェアコンポーネント間の接続関係とから、システム全体にわたる故障伝播路を表示部に表示させるための機能部である。
【００２８】
〈仕様記述〉
図３は、図１に示してある入出力インタフェースおよび内部仕様を形式記述言語Ａｌｌｏｙで記述したものである。ここでは、非常に単純な場合を例に採用しているが、より複雑な仕様も記述できる。例えば、複数の出力が同時に取るべき値の条件や、ある出力の時系列的な制約などを記述しても良いし、また、ソフトウェアコンポーネントの内部状態に依存して正常値の範囲が変わるようにしても良い。
【００２９】
図４は、図３に示す仕様を基に異常仕様作成部３が作成した異常仕様である。図４は、入力のうちｙ（ＩｎＹ）を正常値以外に変更した場合の異常仕様である。基本的に、正常な仕様のうち入力に関する制約に対して論理否定を作用させることで、異常仕様の作成ができる。
【００３０】
〈処理フロー〉
図５は、本実施形態におけるソフトウェアコンポーネントの信頼性評価処理方法の流れを示すフローチャートである。図５は、一つのソフトウェアコンポーネント、すなわち、一つの仕様記述に対する信頼性評価のフローである。
【００３１】
ステップＳ２において、仕様情報取得部２が検査対象ソフトウェアコンポーネントのインタフェース仕様情報（正常仕様）を取得する。典型的には仕様記述ファイルの読み込みであるが、ＡＤＬ等で記述された設計情報から自動的に仕様記述ファイルを作成してもか
まわない。
【００３２】
ステップＳ４では、取得した正常仕様情報に基づいて、モデル検査部４を用いて網羅的な検証によるモデル検査を行う。これにより、インタフェース仕様として記述された要件をソフトウェアコンポーネントが満足するか否かが検証される。これは、従来のモデル検査部（Ａｌｌｏｙ Ａｎａｌｙｚｅｒ等）の利用方法である。この時点で反例が発見された場合には、仕様を再考する。
【００３３】
ステップＳ６においてソフトウェアコンポーネントの入力のうち１つを選択し、ステップＳ８において選択した入力の仕様を正常値以外を示すように変更した異常仕様を異常仕様作成部３が作成する。ステップＳ１０で、作成した異常仕様を用いてモデル検査を行う。このモデル検査の結果として、反例が見つかったか場合（Ｓ１２−ＹＥＳ）は、ステップＳ１４で、正常値以外にした入力と仕様を満たさない出力とを関連づけて、故障伝播路記憶部５に記憶する。例えば、入力ｙと出力ａとを関連づけて記憶する。
【００３４】
ステップＳ１６で、このソフトウェアコンポーネントについて、全ての入力について入力仕様を正常値以外にしたか判断し、まだ正常値以外にしていない入力がある場合にはステップＳ６に戻る。次回の検査では、新たな入力だけを正常値以外にした異常仕様を作成する。例えば、入力ｘのみを正常値以外にしてモデル検査を行った後は、入力ｙのみを正常値以外にして、入力ｘについては正常な仕様にしてモデル検査を行う。全ての入力について正常値以外にしたモデル検査を実行した後は、このソフトウェアコンポーネントについての信頼性評価を終了する。
【００３５】
このソフトウェアコンポーネントの信頼性評価は、一つのみのコンポーネントに対して行うだけでなく、システムを構成する複数のコンポーネントに対して順次行うことも好ましい。すなわち、各ソフトウェアコンポーネントに対して、図５のフローチャートに示す処理、具体的には、仕様情報の取得、異常仕様の作成、異常仕様に基づくモデル検査、および故障伝播路の記憶を実行する。その結果、各ソフトウェアコンポーネントについて、故障伝播路となる入力と出力の組合せが故障伝播路記憶部５に格納される。
【００３６】
このようにして各ソフトウェアコンポーネントに対して異常の伝播路が算出されると、故障伝播路記憶部５に関連づけて記憶された入力と出力に基づいて、システム全体における故障伝播路を把握することができる。例えば、故障伝播路表示部６は、ある個所で発生した故障がどのように伝播するかを表示することができる。また、故障伝播路表示部６は、ある個所で検出された故障の真の原因となり得る個所を表示することもできる。このように、故障に対してシステム全体がどのように振る舞うかを明確にすることができるので、複数のソフトウェアコンポーネントから構成されるシステム（ソフトウェア）全体の評価にも用いることができる。例えば、安全性を損なうようなイベントが、どのソフトウェアコンポーネントの故障（バグ）によって引き起こされる可能性があるか等を分析できる。
【００３７】
〈変形〉
ここでは、形式記述言語としてＡｌｌｏｙ、モデル検査ツールとしてＡｌｌｏｙ Ａｎａｌｙｚｅｒを例として説明したが、入力仕様、内部仕様、出力仕様を記述可能であり、数学的手法によって上記の仕様が満足するかどうかを検証可能なツールであれば、任意の手法を採用することができる。たとえば、ＳＰＩＮ、Ｐｒｏｍｅｌａ、ＳＭＶ，ＬＴＳＡなどを利用可能である。
【００３８】
上記の説明では、取得した仕様に基づくモデル検査（図５のステップＳ４）と、入力を正常値以外に変更した仕様に基づくモデル検査（図５のステップＳ１０）の両方を行って
いるが、前者は必ずしも行わなくてもかまわない。すなわち、作成した仕様が無矛盾であることが保障されているならば、異常仕様に基づくモデル検査のみを行って故障がどのように伝播するかだけを調べてもかまわない。
【００３９】
また、上記では入力を一つずつ異常に設定する場合のみを説明したが、複数の入力を同時に異常に設定してモデル検査を行ってもかまわない。
【符号の説明】
【００４０】
１ 信頼性評価装置
２ 仕様情報取得部
３ 異常仕様作成部
４ モデル検査部
５ 故障伝播路記憶部
６ 故障伝播路表示部
【特許請求の範囲】
【請求項１】
モデルの形式検証機能を有するコンピュータが、
ソフトウェアコンポーネントの入力インタフェース仕様、出力インタフェース仕様、内部仕様を含む仕様情報を取得する仕様情報取得ステップと、
前記仕様情報中の入力インタフェース仕様を正常値以外に変更した仕様情報に従って、前記形式検証機能によって前記ソフトウェアコンポーネントを検証する検証ステップと、
前記検証ステップにおいて前記出力インタフェース仕様を満足しない出力値となる例が発見された場合には、前記正常値以外に変更した入力と、前記出力インタフェース仕様を満たさない出力とを、対応づけて記憶する故障伝播路記憶ステップと、
を実行する、ソフトウェアコンポーネントの信頼性評価方法。
【請求項２】
前記ソフトウェアコンポーネントは、複数の入力値をとるものであり、
前記検証ステップでは、入力値のそれぞれについて、入力インタフェース仕様を正常値以外に変更した仕様情報に従って、ソフトウェアコンポーネントの検証を行う、
請求項１に記載のソフトウェアコンポーネントの信頼性評価方法。
【請求項３】
前記コンピュータが、前記仕様情報取得ステップで取得した仕様情報から、入力値ごとに入力インタフェース仕様を正常値以外にした異常仕様情報を作成するステップ、をさらに実行する、
請求項２に記載のソフトウェアコンポーネントの信頼性評価方法。
【請求項４】
前記コンピュータが、
複数のソフトウェアコンポーネントを含むシステムの各ソフトウェアコンポーネントに対して、前記仕様情報取得ステップ、検証ステップ、故障伝播路記憶ステップを実行し、
前記故障伝播路記憶ステップにおいて関連づけて記憶された入力と出力とに基づいて、前記システムの故障伝播路を表示する、
請求項１〜３のいずれかに記載のソフトウェアコンポーネントの信頼性評価方法。
【請求項５】
記憶手段と、
ソフトウェアコンポーネントの入力インタフェース仕様、出力インタフェース仕様、内部仕様を含む仕様情報を取得する仕様情報取得手段と、
前記仕様情報中の入力インタフェース仕様を正常値以外に変更した仕様情報に従って、前記ソフトウェアコンポーネントを形式的検証によって検証し、該検証において前記出力インタフェース仕様を満足しない出力値となる例が発見された場合には、前記正常値以外に変更した入力と、前記出力インタフェース仕様を満たさない出力とを、対応づけて前記記憶手段に記憶する検証手段と、
を備える、ソフトウェアコンポーネントの信頼性評価装置。
【請求項６】
前記ソフトウェアコンポーネントは、複数の入力値をとるものであり、
前記検証手段は、入力値のそれぞれについて、入力インタフェース仕様を正常値以外に変更した仕様情報に従って、ソフトウェアコンポーネントの検証を行う、
請求項５に記載のソフトウェアコンポーネントの信頼性評価装置。
【請求項７】
前記仕様情報取得手段が取得した仕様情報から、入力値ごとに入力インタフェース仕様を正常値以外にした異常仕様情報を作成する異常仕様情報作成手段をさらに備える、
請求項６に記載のソフトウェアコンポーネントの信頼性評価装置。
【請求項８】
複数のソフトウェアコンポーネントを含むシステムの各ソフトウェアコンポーネントに対して、前記検証手段による検証を行い、
前記記憶手段において関連づけて記憶された入力と出力とに基づいて、前記システムの故障伝播路を表示する、
請求項５〜７のいずれかに記載のソフトウェアコンポーネントの信頼性評価装置。
【請求項１】
モデルの形式検証機能を有するコンピュータが、
ソフトウェアコンポーネントの入力インタフェース仕様、出力インタフェース仕様、内部仕様を含む仕様情報を取得する仕様情報取得ステップと、
前記仕様情報中の入力インタフェース仕様を正常値以外に変更した仕様情報に従って、前記形式検証機能によって前記ソフトウェアコンポーネントを検証する検証ステップと、
前記検証ステップにおいて前記出力インタフェース仕様を満足しない出力値となる例が発見された場合には、前記正常値以外に変更した入力と、前記出力インタフェース仕様を満たさない出力とを、対応づけて記憶する故障伝播路記憶ステップと、
を実行する、ソフトウェアコンポーネントの信頼性評価方法。
【請求項２】
前記ソフトウェアコンポーネントは、複数の入力値をとるものであり、
前記検証ステップでは、入力値のそれぞれについて、入力インタフェース仕様を正常値以外に変更した仕様情報に従って、ソフトウェアコンポーネントの検証を行う、
請求項１に記載のソフトウェアコンポーネントの信頼性評価方法。
【請求項３】
前記コンピュータが、前記仕様情報取得ステップで取得した仕様情報から、入力値ごとに入力インタフェース仕様を正常値以外にした異常仕様情報を作成するステップ、をさらに実行する、
請求項２に記載のソフトウェアコンポーネントの信頼性評価方法。
【請求項４】
前記コンピュータが、
複数のソフトウェアコンポーネントを含むシステムの各ソフトウェアコンポーネントに対して、前記仕様情報取得ステップ、検証ステップ、故障伝播路記憶ステップを実行し、
前記故障伝播路記憶ステップにおいて関連づけて記憶された入力と出力とに基づいて、前記システムの故障伝播路を表示する、
請求項１〜３のいずれかに記載のソフトウェアコンポーネントの信頼性評価方法。
【請求項５】
記憶手段と、
ソフトウェアコンポーネントの入力インタフェース仕様、出力インタフェース仕様、内部仕様を含む仕様情報を取得する仕様情報取得手段と、
前記仕様情報中の入力インタフェース仕様を正常値以外に変更した仕様情報に従って、前記ソフトウェアコンポーネントを形式的検証によって検証し、該検証において前記出力インタフェース仕様を満足しない出力値となる例が発見された場合には、前記正常値以外に変更した入力と、前記出力インタフェース仕様を満たさない出力とを、対応づけて前記記憶手段に記憶する検証手段と、
を備える、ソフトウェアコンポーネントの信頼性評価装置。
【請求項６】
前記ソフトウェアコンポーネントは、複数の入力値をとるものであり、
前記検証手段は、入力値のそれぞれについて、入力インタフェース仕様を正常値以外に変更した仕様情報に従って、ソフトウェアコンポーネントの検証を行う、
請求項５に記載のソフトウェアコンポーネントの信頼性評価装置。
【請求項７】
前記仕様情報取得手段が取得した仕様情報から、入力値ごとに入力インタフェース仕様を正常値以外にした異常仕様情報を作成する異常仕様情報作成手段をさらに備える、
請求項６に記載のソフトウェアコンポーネントの信頼性評価装置。
【請求項８】
複数のソフトウェアコンポーネントを含むシステムの各ソフトウェアコンポーネントに対して、前記検証手段による検証を行い、
前記記憶手段において関連づけて記憶された入力と出力とに基づいて、前記システムの故障伝播路を表示する、
請求項５〜７のいずれかに記載のソフトウェアコンポーネントの信頼性評価装置。
【図１】
【図２】
【図３】
【図４】
【図５】
【図２】
【図３】
【図４】
【図５】
【公開番号】特開２０１２−１２８７２７（Ｐ２０１２−１２８７２７Ａ）
【公開日】平成２４年７月５日（２０１２．７．５）
【国際特許分類】
【出願番号】特願２０１０−２８０６０２（Ｐ２０１０−２８０６０２）
【出願日】平成２２年１２月１６日（２０１０．１２．１６）
【出願人】（５０２０８７４６０）株式会社トヨタＩＴ開発センター (232)
【出願人】（０００００３２０７）トヨタ自動車株式会社 (59,920)
【Ｆターム（参考）】
【公開日】平成２４年７月５日（２０１２．７．５）
【国際特許分類】
【出願日】平成２２年１２月１６日（２０１０．１２．１６）
【出願人】（５０２０８７４６０）株式会社トヨタＩＴ開発センター (232)
【出願人】（０００００３２０７）トヨタ自動車株式会社 (59,920)
【Ｆターム（参考）】
[ Back to top ]