(57)【要約】【課題】シーケンス図における時間断片に割り当てられる時間制約の不整合を検出する。【解決手段】  本発明の方法は、シーケンス図において、複数の時間断片（σｉ）を含む少なくとも１つ以上の集合（Ｕｊ）を設定するステップと、集合（Ｕｊ）の各々において、シーケンス制約（ＣＳ）と、複数の時間断片（σｉ）の各々に割り当てられる時間制約（ＣＴｉ）とを含む論理式（Ｙ）を設定するステップと、論理式（Ｙ）が充足可能である場合、複数の割り当てられた時間制約（ＣＴｉ）のうちの少なくとも１つの時間制約（ＣＴｉ）を否定する否定時間制約（Ｃ´Ｔｉ）とを含む少なくとも１つ以上の集合（Ｕ´ｊｋ）を設定するステップと、集合（Ｕ´ｊｋ）の各々において、シーケンス制約（ＣＳ）と複数の否定時間制約（Ｃ´Ｔｉ）とを含む論理式（Ｙ´）を設定するステップと、論理式（Ｙ´）の充足可能性を判定するステップと、を含む。【選択図】図１
2015087880.tif 000002
【特許請求の範囲】
【請求項１】
コンピュータを用いて、シーケンス図における時間断片に割り当てられる時間制約の不整合を検出する方法であって、
複数のイベントの発生順を意味するシーケンス制約（ＣＳ）と、複数のイベントの中から選択される２つのイベントの発生時点間の時間を意味する時間断片（σｉ）の各々に割り当てられる時間制約（ＣＴｉ）とを含むシーケンス図を準備するステップと、
複数の時間断片（σｉ）を含む少なくとも１つ以上の集合（Ｕｊ）を設定するステップと、
集合（Ｕｊ）の各々において、シーケンス制約（ＣＳ）と、複数の時間断片（σｉ）の各々に対応する時間制約（ＣＴｉ）とを含む論理式（Ｙ）を設定するステップと、
論理式（Ｙ）の充足可能性を判定するステップと、
前記判定の結果が充足可能の場合、複数の前記対応する時間制約（ＣＴｉ）のうちの少なくとも１つの時間制約（ＣＴｉ）を否定する否定時間制約（Ｃ´Ｔｉ）を含む少なくとも１つ以上の集合（Ｕ´ｊｋ）を設定するステップと、
集合（Ｕ´ｊｋ）の各々において、シーケンス制約（ＣＳ）と複数の否定時間制約（Ｃ´Ｔｉ）とを含む論理式（Ｙ´）を設定するステップと、
論理式（Ｙ´）の充足可能性を判定するステップと、を含む方法。
【請求項２】
前記集合（Ｕｊ）を設定するステップは、
前記複数の時間断片（σｉ）を含む全体的な集合（Ｕ）を設定するステップと、
全体的な集合（Ｕ）を少なくとも２つ以上の部分集合（Ｕｊ）に分割するステップと、を含む、請求項１に記載の方法。
【請求項３】
前記集合（Ｕｊ）を設定するステップは、前記複数の時間断片（σｉ）の間の接続関係または順序関係を示す２つのグラフのうちの少なくとも１つを作成するステップを含む、請求項２に記載の方法。
【請求項４】
前記論理式（Ｙ）の充足可能性を判定するステップは、当該判定の結果が充足不可能の場合、エラーメッセージを出力するステップを含み、
前記論理式（Ｙ´）の成立／不成立を判定するステップは、当該判定の結果が充足不可能の場合、エラーメッセージを出力するステップを含む、請求項１〜３のいずれか１項に記載の方法。
【請求項５】
前記論理式（Ｙ）の充足可能性を判定するステップは、制約ソルバーを用いて前記論理式（Ｙ）の充足可能性を判定するステップを含み、
前記論理式（Ｙ´）の充足可能性を判定するステップは、制約ソルバーを用いて前記論理式（Ｙ´）の充足可能性を判定するステップを含む、請求項１〜４のいずれか１項に記載の方法。
【請求項６】
請求項１〜５のいずれか一項に記載の各ステップをコンピュータに実行させるためのコンピュータ・プログラム。
【請求項７】
請求項１〜５のいずれか一項に記載の各ステップを実行するコンピュータ。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、シーケンス図における時間制約の不整合の検出方法に関する。
【背景技術】
【０００２】
ＵＭＬ等で使われるシーケンス図は、設計者がイベントの発生順序と各イベント間の処理時間とを設定するために用いられる。シーケンス図において、イベント間の時間断片（時間幅）に対して時間制約が設定される。この時間制約は、発注者（顧客）によって要求として与えられ、その後随時変更／更新される。設計者は、顧客による時間制約の要求を満たすように、対象となるシステムの仕様として、イベントの発生順序と各イベント間の処理時間に対する時間制約の詳細を設定する必要がある。
【０００３】
しかし、手作業での時間制約の更新では、しばしばミスなどにより不整合のある時間制約が設定されることがある。特に、その不整合の問題は、イベント数が多い複雑なシーケンス図において顕著になる傾向がある。例えば、下記の非特許文献１では、不整合には以下の３種類のケースがあることが述べられている。
（ａ）時間的非一貫性: 全ての時間制約を同時に満たすような処理時間は実現し得ないこと
（ｂ）図的不一致: 時間制約を満たすとシーケンス図のイベント順序を実現し得ないこと
（ｃ）時間的不一致: 仕様として設定された時間制約を満たしていても要求として設定された時間制約を満たさないような処理時間があり得ること
【０００４】
この時間制約の不整合を機械的に検出する従来方法として、例えば、下記の非特許文献２に例示されるような、制約ソルバー（プログラミング）を利用して、時間制約間の矛盾の有無を充足可能性の問題（可否）として検出する方法が知られている。また先の非特許文献１では、仕様から処理時間の最悪値／最善値を計算することで不整合を検出する手法を開示している。
【０００５】
しかし、従来の充足可能性検査を利用した方法では、上記の（ａ）時間的非一貫性および（ｂ）図的不一致のタイプの不整合しか検出できない上に、顧客による時間制約と設計者が設定する時間制約との区別が不十分であり、両者が矛盾するケースを必ずしも適切に抽出することができないという問題がある。
【０００６】
また、従来の最悪値／最善値を計算する手法では、上記の（ｃ）時間的不一致を検出することができるが、全ての時間の区間に独立に時間制約を設定する必要があり、シーケンス図で一般的に見られるような時間制約が未指定の区間を含む場合に対応できないという問題がある。
【先行技術文献】
【非特許文献】
【０００７】
【非特許文献１】“An Analyzer for Message Sequence Chart”、Software Conceptsand Tools (1996) 17、pp.70−77
【非特許文献２】“多項式制約間の矛盾検出法”、数式処理J.JSSAC (2003) Vol.9、No.4、pp.36−51
【発明の概要】
【発明が解決しようとする課題】
【０００８】
したがって、本発明の目的は、シーケンス図において、顧客による時間制約の要求に矛盾することなく、設計者がイベントの発生順序と時間制約の詳細な設計をおこなうことを容易にするために、時間制約間の不整合を機械的に検出することである。
【課題を解決するための手段】
【０００９】
本発明は、コンピュータを用いて、シーケンス図における時間断片に割り当てられる時間制約の不整合を検出する方法を提供する。その方法は、ａ）複数のイベントの発生順を意味するシーケンス制約（ＣＳ）と、複数のイベントの中から選択される２つのイベントの発生時点間の時間を意味する時間断片（σｉ）の各々に割り当てられる時間制約（ＣＴｉ）とを含むシーケンス図を準備するステップと、ｂ）複数の時間断片（σｉ）を含む少なくとも１つ以上の集合（Ｕｊ）を設定するステップと、ｃ）集合（Ｕｊ）の各々において、シーケンス制約（ＣＳ）と、複数の時間断片（σｉ）の各々に対応する時間制約（ＣＴｉ）とを含む論理式（Ｙ）を設定するステップと、ｄ）論理式（Ｙ）の充足可能性を判定するステップと、ｅ）判定の結果が充足可能の場合、複数の前記対応する時間制約（ＣＴｉ）のうちの少なくとも１つの時間制約（ＣＴｉ）を否定する否定時間制約（Ｃ´Ｔｉ）を含む少なくとも１つ以上の集合（Ｕ´ｊｋ）を設定するステップと、ｆ）集合（Ｕ´ｊｋ）の各々において、シーケンス制約（ＣＳ）と複数の否定時間制約（Ｃ´Ｔｉ）とを含む論理式（Ｙ´）を設定するステップと、ｇ）論理式（Ｙ´）の充足可能性を判定するステップと、を含む。
【００１０】
本発明の一態様では、集合（Ｕｊ）を設定するステップは、複数の時間断片（σｉ）を含む全体的な集合（Ｕ）を設定するステップと、全体的な集合（Ｕ）を少なくとも２つ以上の部分集合（Ｕｊ）に分割するステップと、を含む。
【００１１】
本発明の一態様では、集合（Ｕｊ）を設定するステップは、複数の時間断片（σｉ）の間の接続関係、及び順序関係の各々を示す２つのグラフのうちの少なくとも１つを作成するステップを含む。
【００１２】
本発明の別の一態様では、論理式（Ｙ）の充足可能性を判定するステップは、判定の結果が不成立の場合、エラーメッセージを出力するステップを含み、論理式（Ｙ´）の充足可能性を判定するステップは、当該判定の結果が充足不可能の場合、エラーメッセージを出力するステップを含む。
【００１３】
本発明の別の一態様では、論理式（Ｙ）の充足可能性を判定するステップは、制約ソルバーを用いて論理式（Ｙ）の充足可能性を判定するステップを含み、論理式（Ｙ´）の充足可能性を判定するステップは、制約ソルバーを用いて論理式（Ｙ´）の充足可能性を判定するステップを含む。制約ソルバーとしては、例えばＳＭＴ（Satisfiability Modulo
Theory）ソルバーを用いることができる。
【図面の簡単な説明】
【００１４】
【図１】本発明の方法の一実施形態のフローを示す図である。
【図２】本発明のシーケンス図（ＳＤ）の一部を例示する図である。
【図３】本発明の集合Ｕの設定（分割）を説明するための図である。
【図４】本発明の集合Ｕの分割方法の一実施例を示す図である。
【図５】図４のステップＡ２の詳細を示す図である。
【図６】図４のステップＡ２の詳細を示す図である。
【図７】図４のステップＡ３の詳細を示す図である。
【図８】図４のステップＡ３の詳細を示す図である。
【図９】図４のステップＡ３の詳細を示す図である。
【図１０】本発明の一実施例のシーケンス図（ＳＤ）を示す図である。
【図１１】本発明の一実施例のシーケンス図（ＳＤ）を示す図である。
【図１２】本発明の一実施例のシーケンス図（ＳＤ）を示す図である。
【図１３】本発明の方法を実行するコンピュータの構成例を示すブロック図である。
【発明を実施するための形態】
【００１５】
図面を参照しながら本発明の実施の形態を説明する。図１は、本発明の方法のフローを示す図である。図１のフローは、コンピュータが当該方法のためのプログラム（ソフトウェア）を実行することにより実施される。
【００１６】
ユーザが入力として与えたシーケンス図（ＳＤ）には、複数のイベントの中から選択される２つのイベントの発生時点間の時間を意味する時間断片（σｉ）の各々に割り当てられる時間制約（ＣＴｉ）が記載されている。ステップＳ１において、入力されたシーケンス図（ＳＤ）に対して、複数のイベントの発生順を意味するシーケンス制約（ＣＳ）と時間制約（ＣＴｉ）とを設定する。
【００１７】
図２は、シーケンス図（ＳＤ）の一部を例示する図である。図２において、シーケンス制約（ＣＳ）として、複数のイベントｂ３、ｂ１、・・・、ｅ２、ｅ３が矢印１０上で時系列に発生している。イベントとは、ある処理の開始や終了など、処理の区切りを意味する。シーケンス制約（ＣＳ）におけるイベントの順番は、各イベントでの処理の機能、連続性等を考慮して設定される。σ１、σ２、σ３は、時間断片（σｉ）の例である。Ｔ１は、イベントｂ１とｅ１の間の区間からなる時間断片σ１に指定された時間制約ＣＴ１の制約値である。Ｔ２は、イベントｂ２とｅ３の間の区間からなる時間断片σ２に指定された時間制約ＣＴ２の制約値である。Ｔ＊３は、イベントｂ３とｅ３の間の区間からなる時間断片σ３に指定された時間制約ＣＴ３の制約値である。Ｔ＊３の“＊”は、その区間の時間断片が外部（顧客）からの時間制約（ＣＴｉ）の設定を受ける時間断片であることを意味する。
【００１８】
時間断片σ１、σ２、σ３には、それぞれ時間制約（ＣＴｉ）として、ＣＴ１、ＣＴ２、ＣＴ３＊が設定される。ＣＴ３＊の“＊”は、上述したＴ＊３の場合と同様に、外部（顧客）から要求される時間制約（ＣＴｉ）であることを意味する。時間制約（ＣＴｉ）は、一般に論理式として設定される。図２では、ＣＴ１、ＣＴ２、ＣＴ３＊は、順番に
ＣＴ１：ｔ（ｅ１）−ｔ（ｂ１）＜Ｔ１
ＣＴ２：ｔ（ｅ２）−（ｂ２）＜Ｔ２
ＣＴ３＊：ｔ（ｅ３）−ｔ（ｂ３）＜Ｔ＊３
として設定される。ｔ（ｅ１）、ｔ（ｂ１）等は、それぞれイベントｅ１、ｂ１等の発生時刻である。時間制約ＣＴｉは２つのイベント間の時間断片σｉの処理時間が制約値Ｔｉ未満であることを意味する。制約値Ｔ１、Ｔ２、Ｔ３の値は、図２の例ではＴ１＝１０、Ｔ２＝３０、Ｔ３＝３０となっている。数字１０、３０の単位は、秒、分、時間、日、週、月等の中から任意に選択できる。
【００１９】
図１に戻って、ステップＳ２において、ステップＳ１で設定された全ての時間断片（σｉ）を含む少なくとも１つ以上の集合（Ｕｊ）を設定する。集合（Ｕｊ）は、例えば、シーケンス図（ＳＤ）に含まれる複数の時間断片（σｉ）を含む１つの全体的な集合（Ｕ）を設定し、その全体的な集合（Ｕ）を分割することにより得ることができる。
【００２０】
図３は、集合（Ｕｊ）の設定（集合（Ｕ）の分割）を説明するための図である。図３において、（ａ）はシーケンス図（ＳＤ）の一部を示し、（ｂ）は（ａ）のＳＤにおける分割後の集合（Ｕｊ）の表示例を示す。（ａ）において、シーケンス制約（ＣＳ）として、白丸で示される複数のイベントの発生が時系列に設定されている。Ｔ１〜Ｔ１２＊は、図２の場合と同様に、それぞれ対応するイベント発生間の区間における時間断片（σ１〜σ１２＊）にかかる制約値を表す。以後、各時間断片の時間制約の表記を図から省略し、制約値Ｔｉのみ記載する。この例の場合、上述した全体的な集合（Ｕ）は、
Ｕ＝｛σ１、σ２、・・・、σ１１＊、σ１２＊｝      （１）
と表すことができる。
【００２１】
図３（ｂ）に集合（Ｕｉ）の例を示す。この例では、破線で囲まれた１１個の集合、Ｕ１〜Ｕ１１に分割されている。なお、各集合において、他の集合との部分的な重複は許される。例えば、図の左下側の集合Ｕ１は時間断片σ１とσ６を含むが、σ１は同時に隣の集合Ｕ５にも含まれる。またこの図には、後に説明する手法でこの分割を得る際に使用した、複数の時間断片（σｉ）の集合についての順序関係および接続関係の有向非循環グラフ（Directed Acyclic Graph、DAG）もあわせて示している。実線の矢印は順序関係および接続関係を表し、σ４からσ５へ向かう一点鎖線の矢印は順序関係のみであることを表す。
【００２２】
図１のステップＳ７からＳ１２の繰り返しにおいて現れる集合Ｕ´ｊｋの個数は、時間断片の数に対して非線形に増加するため、不整合の検出に見逃しが発生しない限り時間断片集合Ｕを複数の小さな集合Ｕｊに分割し、それぞれにステップＳ７からＳ１２を適用した方が計算時間を節約できる。そのような分割方法には様々な方法が考えられるが、ここでは時間断片集合の被覆を使った方法を記述する。
【００２３】
図４は、本発明の集合Ｕの分割方法の一実施例を示す図である。図４は、時間断片集合の被覆を使った方法の１例である。ステップＡ１においてイベントの順序及び時間断片集合Ｕから順序関係のグラフＧＯおよび接続関係のグラフＧＣを作成する。
【００２４】
順序関係のグラフＧＯとは、集合Ｕの時間断片を頂点とし、集合Ｕの任意の２つの時間断片σｈ、σｉについて、σｈの開始イベントの時刻がσｉの開始イベントの時刻より早く、かつσｈの終了イベントの時刻がσｉの終了イベントの時刻より早いならば、σｈからσｉの方へ向き付けられた辺を設定した有向非循環グラフ（ＤＡＧ）である。またσｈとσｉの間に上記の有向辺を作成する条件が成り立つとき、σｈからσｉへ順序関係があるという。 
【００２５】
接続関係のグラフＧＣとは、集合Ｕの時間断片を頂点とし、集合Ｕの任意の２つの時間断片σｈ、σｉについて、σｈからσｉへ順序関係があり、かつ両者に重複する時間の区間があるとき、σｈからσｉの方へ向き付けられた辺を設定した有向非循環グラフ（ＤＡＧ）である。またσｈからσｉに上記の有向辺を作成する条件が成り立つとき、σｈからσｉへ接続関係があるという。
【００２６】
上記の順序関係、接続関係のグラフは推移律が成り立つため、順序関係のグラフＧＯおよび接続関係のグラフＧＣはそれぞれの推移簡約のグラフに変換することができる。推移簡約のグラフとはあるＤＡＧから推移律で存在が示せる辺を全て省略（消去）したものである。以降、これらのグラフは推移簡約であるとする。
【００２７】
図４のステップＡ２において、時間断片の集合Ｕから、全ての可能な連続断片列Ｖの集合Ｒを求める。連続断片列Ｖとは、時間断片の集合であって、その要素の時間断片は少なくとも１つの他のＶの要素の時間断片と互いに隣接するか、一部の区間に重なりを持つものであり、さらに以下の条件を満たす。
・連続性：Ｖ中の全ての時間断片が被覆する区間は連続。
・極小性：どの時間断片σをＶから取り除いても、連続性を失うか、元のＶの被覆する範囲より狭くなる。
例えば図３（ａ）において、Ｔ２、Ｔ８、Ｔ９という制約値の表示に対応する時間断片の集合｛σ２、σ８、σ９｝は連続断片列である。一方、Ｔ２、Ｔ６、Ｔ８という制約値の表示に対応する時間断片の集合｛σ２、σ６、σ８｝は連続断片列ではない。何故ならばσ８を取り除いても被覆範囲が変わらないため極小性を満たさないからである。
【００２８】
図５と図６は図４のステップＡ２の詳細を示す図である。上記の接続関係のグラフＧＣを利用し、全時間断片の集合Ｕのそれぞれの時間断片σｉについて、それを始点として接続関係にある時間断片を次々と深さ優先探索で求め、探索が１歩進むたびに始点σｉから現在の時間断片までの経由した全ての時間断片の集合を連続時間断片列として、集合Ｒに追加する。
【００２９】
図４のステップＡ３において、連続断片列の集合Ｒ中のそれぞれの連続断片列Ｖについて、Ｖの被覆範囲における、全ての可能な非重複断片集合Ｗを求め、ＶとＷの組（Ｖ、Ｗ）の集合Ｐを作成する。非重複断片集合Ｗとは、時間断片の集合であって、ある連続な時間区間の範囲において、以下の性質を持つものである。
・包含性：全ての要素の時間断片がこの範囲に含まれる。
・非重複性：Ｗ中のどの時間断片σも、Ｗからσを除いた集合によって被覆されない。
・極大性：Ｗ以外のＵ中のどの時間断片を加えても、包含性と非重複性の一方または両方を満たさない。
例えば図３（ａ）において、Ｔ３、Ｔ７、Ｔ９という制約値の表記がある時間制約に対応した時間断片σ３、σ７、σ９のうち、｛σ３、σ９｝、｛σ７、σ９｝はそれぞれ非重複断片集合であり、｛σ３｝は極大性を満たさず、｛σ３、σ７｝は非重複性を満たさないので両者とも非重複断片集合ではない。
【００３０】
図７〜図９はステップＡ３の詳細を示す図である。時間断片の集合Ｕと、全ての連続断片列の集まりＲから、Ｒ中のそれぞれの連続断片列Ｖについて、Ｖの被覆範囲における、全ての可能な非重複断片集合Ｗを求める。この作業を全てのＶについて繰り返すことによりＶとＷの組（Ｖ、Ｗ）の集合Ｐを作成する。
【００３１】
図８と図９は上記した図７のＶの被覆範囲における全ての可能な非重複断片集合Ｗを求める手続きを示す図である。全時間断片の集合Ｕのうち、Ｖの被覆範囲に含まれ、かつＶに含まれない全ての時間断片の集合Ｑを求め、この中から探索の始点となる時間断片σｉを選ぶ。先に求めておいた順序関係グラフＧＯを用いて、Ｑの中でσｉと順序関係にある時間断片を次々求め、探索が１歩進むたびに、始点σｉから現在の時間断片までの経由した全ての時間断片の集合を、Ｖの被覆範囲における非重複断片集合Ｗとし、（Ｖ、Ｗ）の組の形でＰに追加する。
【００３２】
図４のステップＡ４において、Pの個々の（Ｖ、Ｗ）の組について、ＶとＷの和集合Ｇを求めて、これを分割後の時間断片集合Ｕｊとする。よって時間断片集合の全ての集合Ｈ＝｛Ｕｊ｝の個数は、Ｐの要素数、すなわち（Ｖ、Ｗ）の組の数となる。
【００３３】
図１に戻って、ステップＳ３〜Ｓ６において、上記した段落０００３の（ａ）時間的非一貫性および（ｂ）図的不一致を検出する。ステップＳ３において、集合（Ｕｊ）の各々において、シーケンス制約（ＣＳ）と、複数の時間断片（σｉ）の各々に対応する時間制約（ＣＴｉ）とを含む論理式（Ｙ）を設定する。論理式（Ｙ）は、図３（ｂ）で例示されるような集合ＵＴ６〜ＵＴ１２の各々において設定される。例えば、図２のシーケンス図（ＳＤ）の一部の例示を用いて、論理式（Ｙ）を表現すると以下のようになる。
Y＝CS∧CT1∧CT2∧CT3*              （２）
ただし、
CS＝t(b3)＜t(b1) ∧・・・∧t(e2) ＜t(e3)
CT1＝t(e1)−t(b1)＜T1（＝10）
CT2＝t(e2) −t(b2)＜T2（＝30）
CT3*＝t(e3) −t(b3)＜T3*（＝30）
論理式（Ｙ）の長さは、集合（Ｕｉ）に含まれる時間制約（ＣＴｉ）の数に応じて増減する。一般的には、Ｎ個の時間制約があるとして、論理式（Ｙ）は、次式で表すことができる。
Y＝CS∧CT1∧CT2∧・・・∧CTN          （３） 
【００３４】
次のステップＳ４において、論理式Ｙの充足可能性を判定する。この判定は、例えば、論理式ＹをＳＭＴソルバーに入力して、その出力である充足可能性の結果により判断する。すなわち、充足可能性がない場合は論理式Ｙが成立し得ない（時間制約を全て同時には満たせない）ことになる。次のステップＳ５において判定結果の判断をおこなう。論理式Ｙが充足不可能の場合、ステップＳ６においてエラーを出力して、本プログラムを停止する。
【００３５】
次のステップＳ７からＳ１２において、上記した段落０００３の（ｃ）時間的不一致を検出する。まず時間制約の集合（Ｕｊ）を要求である時間制約の集合Ｒと設計者による仕様としての時間制約の集合Ｄに分割する。集合ＲとＤの全ての要素の論理積をそれぞれＣＲ、ＣＤで定義する。
ＣＲ＝（∧ＲＣＴｉ）
ＣＤ＝（∧ＤＣＴｉ）
従来手法で使われている時間的不一致の定義は以下の論理式が充足可能なことである。
ＣＳ∧ＣＤ∧¬ＣＲ            （４）
しかしこの定義は先に述べたように、設計仕様としての時間制約が与えられない区間ｓがある場合、すなわち集合Ｒの時間制約には含まれる区間ｓが集合Ｄの時間制約では制約されないとき、設計仕様の内容とは無関係にｓの長さ次第でＣＲは真にも偽にもなる場合がある。この場合も充足可能となり時間的不一致ありと判定されるが、これでは設計仕様として与えた時間制約が原因の不整合なのかがはっきりせず、誤検出となる可能性があった。
【００３６】
このようなケースを除外するため、本発明ではより条件の厳しい時間的不一致の定義を用い、実用上明確に設計仕様として与えた時間制約が原因の不整合といえる場合のみを検出する。その定義は以下の論理式が充足不可能なことである。
ＣＳ∧ＣＲ∧ＣＤ´      （５）
ただし、ＣＤ´は集合Ｄの全ての時間制約の否定の論理積である。
ＣＤ´＝（∧Ｄ¬ＣＴｉ）
この論理式（５）が充足不可能なとき、上記の設計仕様としての時間制約が与えられない区間ｓがあったとしても、ｓの値によらずに式（４）を充足する（ＣＲが偽になる）ような区間の取り方が存在する。この性質は時間制約が上記した段落００１８で示されるような線形な不等式の場合に成り立つ。すなわち設計仕様として与えた時間制約Ｄによる要求としての時間制約Ｒの間の不整合であると確定できる。
【００３７】
上記の、時間制約の集合（Ｕｊ）を要求である時間制約の集合Ｒと設計者による仕様としての時間制約の集合Ｄに分割する方法であるが、例えばＲとして前述の外部（顧客）からの制約、Ｄとしてそれ以外を取るという方法が考えられる。しかし一般には設計仕様としての制約どうしでの不整合も検出するというニーズがあるため、ここではＲとしてＵｊの任意の部分集合Ｒ∈２Ｕｊ、Ｄとしてそれ以外Ｄ＝Ｕｊ−Ｒと取り、全てのＲのとり方について検査を行うこととする。この手順を以下の節で具体的に示す。
【００３８】
ステップＳ７において、ステップＳ４の判定の結果が充足可能の場合、複数の対応する時間制約（ＣＴｉ）のうちの少なくとも１つの時間制約（ＣＴｉ）を否定する否定時間制約（Ｃ´Ｔｉ）を含む少なくとも１つ以上の集合（Ｕ´ｊｋ）を設定する。図３（ｂ）で例示されるような集合ＵＴ６を例にとると、集合（Ｕ´ｊｋ）は、例えば、下記の各式のように表すことができる。なお、式中の記号“¬”は、時間制約を否定することを意味する。否定時間制約（Ｃ´Ｔｉ）は、“¬ＣＴｉ”と表すことができる。
Ｕ´Ｔ６１＝｛ＣＴ１、¬ＣＴ６｝            （６）
Ｕ´Ｔ６２＝｛¬ＣＴ１、ＣＴ６｝            （７）
Ｕ´Ｔ６３＝｛¬ＣＴ１、¬ＣＴ６｝          （８）
【００３９】
次のステップＳ８において、集合（Ｕ´ｊｋ）の各々において、シーケンス制約（ＣＳ）と複数の否定時間制約（Ｃ´Ｔｉ）とを含む論理式（Ｙ´）を設定する。例えば、上記の式（４）、（５）、（６）の集合Ｕ´Ｔ６１、Ｕ´Ｔ６２、Ｕ´Ｔ６３を例にとると、論理式（Ｙ´）は、以下のように表すことができる。
Y’＝CS∧CT1∧¬CT6                  （９） 
Y’＝CS∧¬CT１∧CT6                （１０） 
Y’＝CS∧¬CT１∧¬CT6              （１１）
一般的には、Ｎ個の時間制約があるとして、論理式（Ｙ´）は、次式で表すことができる。否定時間制約&not;CTiの数は、１づつ増加させる等、必要に応じて設定することができる。
Y’＝CS ∧CT1∧¬CT2∧・・・∧CTN        （１２）
【００４０】
次のステップＳ９において、論理式（Ｙ´）の充足可能性を判定する。この判定は、ステップＳ４の場合と同様に、例えば、論理式Ｙ´をＳＭＴソルバーに入力して、その出力である充足可能性の結果により判断する。次のステップＳ１０において判定結果の判断をおこなう。論理式Ｙ´が充足不可能の場合、ステップＳ１１においてエラーを出力して、本プログラムを停止する。
【００４１】
次のステップＳ１２において、ステップＳ１０の判定の結果が充足可能の場合、否定時間制約（Ｃ´Ｔｉ）を含む他の集合（Ｕ´ｊｋ）を設定するか否かを判定する。すなわち、さらに否定時間制約（Ｃ´Ｔｉ）を設定する組み合わせがあるか（残っているか）を判定する。この判定がＹｅｓの場合、ステップＳ７に戻って、設定される他の集合（Ｕ´ｊｋ）について、ステップＳ８〜Ｓ１０までの処理を行う。ステップＳ１２の判定がＮｏの場合、ステップＳ１３において、他の集合（Ｕｉ）が残っているか、すなわち、一連の処理をすべき集合（Ｕｊ）があるか否かを判定する。この判定がＹｅｓの場合、ステップＳ３に戻って、他の集合（Ｕｊ）について、ステップＳ３〜Ｓ１２までの処理を行う。ステップＳ１２の判定がＹｅｓの場合、一連の処理を終了する。
【実施例１】
【００４２】
図１０〜図１２を参照しながら、本発明の実施例について説明する。以下に説明する実施例は、同じテスト条件（シーケンス制約及び時間制約）において、本発明の方法と従来の２つの方法とを実行し、そのテスト結果を比較したものである。使用した従来方法は、ＯＡ−２法とＣＳ−２法で、各法の概要は以下の通りである。
【００４３】
（１）ＯＡ−２法
ある時間断片σｉに包含される時間断片の集合のうち、互いに重なりのない時間断片の集合を選ぶ。選び方は様々あるがその処理時間の合計の最大値が時間断片σｉの処理時間を越えていればエラーとする。処理時間の最悪値の推定を使った既存手法の一つである。
（２）ＣＳ−２法
全ての時間制約の集合からひとつの時間制約ＣＴｉを選び、その制約を否定した制約式Ｙ‘＝ＣＳ∧ＣＴ１∧ＣＴ２∧・・・ＣＴｉ−１∧¬ＣＴｉ∧ＣＴｉ＋１∧・・・∧ＣＴｎの充足可能性を制約ソルバーで検査する。充足不可能であればエラーとする。充足可能性を使った既存手法の一つで、エラーとなる制約ＣＴｉは冗長な制約と呼ばれる。
【００４４】
ウェッブ上でユーザ認証およびその認証したユーザに記事の見出しを表示して見せる際の一連のイベントを含むシーケンス図において、シーケンス制約（Ｃｓ）及び時間制約（ＣＴｉ）を備える時間断片（σｉ）を設定して、テストを行った。その際、時間制約の設定を変えた３つのケースでテストを行った。テスト１は、時間制約に充足可能性がある（エラー無し）設定、テスト２及び３は、わざと時間制約に充足可能性がない（エラー有り）場合を含ませた設定である。
【００４５】
図１０〜図１２は、テスト１〜３で使用したシーケンス図のシーケンス制約及び時間断片／時間制約を示す。各図において、“Secure process”はユーザの認証プロセスであることを示し、“News process”は認証後のユーザに対して記事を表示するプロセスであることを示す。図１２の“PI process”は個人情報の表示プロセスであることを示す。各図において、矢印（＜―＞）は時間断片（σｉ）を示し、Ｔｉ＝＊＊（数字）は、各時間断片に設定された時間制約（ＣＴｉ）の制約値を示す。図１１と図１２において、楕円で囲まれた時間制約は、時間制約に充足可能性がない（エラー有り）場合を作るためにわざと入れた無理な設定（数値）である。
【００４６】
図１０〜図１２の３つのテスト条件においてテストをおこなった結果を下記の表に示す。本発明の方法では、予めエラーを含ませたテスト２及び３で、テスト結果としてエラー（ＥＲ）を検出（出力）している。一方、従来のＯＡ−２法では、テスト２でエラー（ＥＲ）を検出しているが、テスト３ではエラー（ＥＲ）の検出ができていない。また、従来のＣＳ−２では、テスト２及び３のいずれでもエラー（ＥＲ）検出に失敗している。したがって、従来の２つの方法に対して本発明の有効性を確認することができた。
【００４７】
【表１】
2015087880.tif 000003
【００４８】
図１３は、本発明の方法を実行するコンピュータの構成例を示すブロック図である。コンピュータ20は、バス230を介して相互に接続された演算処理装置（CPU）200、記憶手段210、各種I/F220を含む。各種I/F220は、入力I/F、出力I/F、外部記憶I/F、外部通信I/F等を含む総称として用いられ、各I/Fが、それぞれ対応するキーボード、マウス等の入力手段240、CRT、LCD等の表示手段250、USB接続の半導体メモリやHDD等の外部記憶手段260等に接続する。記憶手段210は、RAM、ROM等の半導体メモリ、HDD等を含むことができる。本発明の方法の各ステップの結果は、必要に応じて適時表示手段250に表示される。
【００４９】
本発明の実施形態について、図を参照しながら説明をした。しかし、本発明はこれらの実施形態に限られるものではない。本発明はその趣旨を逸脱しない範囲で当業者の知識に基づき種々なる改良、修正、変形を加えた態様で実施できるものである。
【符号の説明】
【００５０】
１０  イベント発生の流れ／シーケンス
２０  コンピュータ
【図１】
2015087880.tif 000004
【図２】
2015087880.tif 000005
【図３】
2015087880.tif 000006
【図４】
2015087880.tif 000007
【図５】
2015087880.tif 000008
【図６】
2015087880.tif 000009
【図７】
2015087880.tif 000010
【図８】
2015087880.tif 000011
【図９】
2015087880.tif 000012
【図１０】
2015087880.tif 000013
【図１１】
2015087880.tif 000014
【図１２】
2015087880.tif 000015
【図１３】
2015087880.tif 000016