(57)【要約】【課題】状態遷移を動作規則から自動的に合成するとともに、合成された状態遷移が動作シナリオと矛盾しないかどうかのモデル検査器による検証結果を同時に出力し、モデル検査のための検証モデルと検証式はいずれも自動的に生成する。【解決手段】ユーザから入力された動作規則を、オートマトンの形式に変換するオートマトン生成部と、前記オートマトンの積を求め、それを合成オートマトンとして出力するオートマトン合成部と、ユーザから入力された各動作シナリオと前記合成オートマトンとに基づいて検証モデルを生成するとともに、前記動作シナリオが最後まで実行され、かつ前記合成オートマトンで禁止された動作が無いことを確認する検証式を生成する検証モデル・検証式生成部と、前記検証モデルと検証式とを用いて、モデル検査を実行する出る検査部とを有する状態遷移設計支援装置。【選択図】図１
2010244140.tif 000002
【特許請求の範囲】
【請求項１】
ユーザから入力された動作規則を、オートマトンの形式に変換するオートマトン生成手段と、
前記オートマトンの積を求め、それを合成オートマトンとして出力するオートマトン合成手段と、
ユーザから入力された各動作シナリオと前記合成オートマトンとに基づいて検証モデルを生成するとともに、前記動作シナリオが最後まで実行され、かつ前記合成オートマトンで禁止された動作が無いことを確認する検証式を生成する検証モデル・検証式生成手段と、
前記検証モデルと検証式とを用いて、モデル検査を実行する検査手段と
を有することを特徴とする状態遷移設計支援装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、状態遷移設計支援装置に関し、より詳しくは状態遷移モデルを作成してさらに検証をする装置である状態遷移設計支援装置に関するものである。
【背景技術】
【０００２】
ソフトウェア開発、特に組込みシステムでは、誤りや漏れのない仕様を記述するために状態遷移図や状態遷移表を用いて設計をする。この時に誤りや漏れの無い状態遷移を効率的に記述する方法が望まれている。
【０００３】
この課題に応える技術として、モデル検査支援装置が提案されている（例えば、特許文献１）。この技術は、モデル記述言語の習得を必要とせずに、動作仕様からモデル検査プログラムを生成でき、より好ましくは、検証済みの動作仕様に応じたソフトウェアを自動的に生成することも可能である。
【０００４】
また、上記課題に応える別の従来技術として、タイミングチャート処理システムも提案されている（例えば、特許文献２）。このシステムは、複数のタスクが共通のリソースを排他的に確保するためのリソーススケジューリングの設計におけるタイミングチャートの処理を行うものである。
【先行技術文献】
【特許文献】
【０００５】
【特許文献１】特開２００７−１１６０５号公開公報（図１）
【特許文献２】特開２００８―１５７３５号公開公報
【発明の概要】
【発明が解決しようとする課題】
【０００６】
状態遷移図や状態遷移表を作成する場合、状態遷移設計を人手で行うのは時間が掛かってしまう。また、状態遷移設計に誤りや漏れが無いことをレビューだけで保証することも一般に困難である。状態遷移設計の正しさをモデル検査によって自動的に確認する手法はあるが、このモデル検査を実施するためには、検証モデルや検証式の作成が必要である。検証モデルや検証式もやはり人手で作られるため、その作成には時間がかかり、また誤りが入ってしまうこともある。
【０００７】
上述の従来の技術であるモデル検査支援装置は、検証モデルは自動生成されるが、検査項目は作業者が時相論理式によって記述する必要があるので、自動的にモデル検査が実施されるわけではない。
【０００８】
また、上述のタイミングチャート処理システムは検証モデル・検証式とも自動生成して検証するシステムであるが、設計そのものを合成する機能は無い。また入力として時間の長さを具体的に記述したタイミングチャートに限定することでリソーススケジューリングの問題を扱うことに特化している。
【０００９】
本発明の目的は、状態遷移を動作規則から自動的に合成するとともに、合成された状態遷移が動作シナリオと矛盾しないかどうかのモデル検査器による検証結果を同時に出力する装置であって、モデル検査のための検証モデルと検証式はいずれも自動的に生成する装置を提供することにある。
【課題を解決するための手段】
【００１０】
上記課題を解決するための手段として、本発明は以下の特徴を有する。
本発明にかかる状態遷移設計支援装置は、ユーザから入力された動作規則を、オートマトンの形式に変換するオートマトン生成手段と、前記オートマトンの積を求め、それを合成オートマトンとして出力するオートマトン合成手段と、ユーザから入力された各動作シナリオと前記合成オートマトンとに基づいて検証モデルを生成するとともに、前記動作シナリオが最後まで実行され、かつ前記合成オートマトンで禁止された動作が無いことを確認する検証式を生成する検証モデル・検証式生成手段と、前記検証モデルと検証式とを用いて、モデル検査を実行する検査手段とを有することを特徴としている。
【発明の効果】
【００１１】
本発明によれば、モデル検査のための検証モデルと検証式はいずれも自動的に生成したうえで、状態遷移を動作規則から自動的に合成するとともに、合成された状態遷移が動作シナリオと矛盾しないかどうかのモデル検査による検証結果を同時に出力することが可能となる。
【発明を実施するための最良の形態】
【００１２】
以下、図面を参照しながら本発明の実施の形態について説明する。  
［１．状態遷移設計支援装置の概要］
本発明の実施の形態は、状態遷移設計支援装置（以下、「支援装置」と略す）として提案される。この支援装置は、状態遷移を動作規則から自動的に合成するとともに、合成された状態遷移が動作シナリオと矛盾しないかどうかを検証するモデル検査の検証結果を同時に出力する装置であって、モデル検査のための検証モデルと検証式を自動的に生成する装置である。
【００１３】
本実施の形態にかかる支援装置の使用法と動作は以下の通りである。
【００１４】
（１）  設計対象についての動作シナリオをユーザが入力する。
（２）  設計対象がもつべき動作規則をユーザが入力する。
（３）  各動作シナリオごとに動作規則を満たしているかどうかの検証を支援装置が実施して、検証の結果を出力する。
（４）  検証の結果が偽になるものがあれば、ユーザは入力を修正して再度検証を繰り返すことができる。
（５）  動作シナリオの検証が全て真になれば、支援装置は矛盾の無い状態遷移設計を出力する。
（６）  動作規則を追加すると、より詳細な状態遷移設計が得られる。
【００１５】
［２．支援装置の構成］
次に、支援装置の構成の例を説明する。  
支援装置は、例えばコンピュータ、ワークステーションなどの情報処理装置によって実現される装置である。この情報処理装置は、演算処理装置（ＣＰＵ）、主メモリ（ＲＡＭ）、読出し専用メモリ（ＲＯＭ）、入出力装置（Ｉ／Ｏ）、及び必要な場合にはハードディスク装置等の外部記憶装置を具備している装置である。
【００１６】
図１に、支援装置の構成例を示した機能ブロック図を掲げる。支援装置１は、動作規則入力部１０と、動作規則入力部１０に接続されたオートマトン変換部２０と、オートマトン変換部２０に接続されたオートマトン合成部３０と、オートマトン合成部３０に接続された状態遷移出力部４０と、動作シナリオ入力部５０と、動作シナリオ入力部５０に接続された検証モデル・検証式生成部６０と、検証モデル・検証式生成部６０に接続されたモデル検査部７０と、モデル検査部７０に接続された検査結果出力部８０とを有している。また、オートマトン合成部３０は、検証モデル・検証式生成部６０に接続されている。
【００１７】
なお、ここで「接続」とは、物理的に結合されている状態に限られず、データの受け渡しが可能である状態を含む意味である。また、上記の各構成要素はＣＰＵ及びＣＰＵによって実行されるプログラムによって実現される機能に対応するものであり、実際に各構成要素に対応するハードウエアを支援装置１が備えている必要はない。
【００１８】
以下、上記構成要素のそれぞれについて説明する。
［２．１．動作規則入力部］
動作規則入力部１０は、ユーザによって入力される動作規則１００を受け取り、これをオートマトン変換部２０に渡す機能を有する。動作規則１００において、ユーザは順序、選択、禁止、繰返しの4種類が指定可能である。動作規則１００の詳細については、後述する。
【００１９】
［２．２．オートマトン変換部］
本発明のオートマトン変換手段に相当するオートマトン変換部２０は、動作規則入力部１０から受け取った動作規則１００を、オートマトンの形式に変換する機能を有する。「オートマトン」とは、入力に対して内部の状態に応じた処理を行い、真か偽のいずれかの結果を出力するシステムをいう。
【００２０】
［２．３．オートマトン合成部］
本発明のオートマトン合成手段に相当するオートマトン合成部３０は、オートマトン変換部２０から出力されたオートマトン（複数）から、そのオートマトンの積を求め、それを合成オートマトンとして出力する機能を有する。
【００２１】
［２．４．状態遷移出力部］
状態遷移出力部４０は、オートマトン合成部３０で生成された合成オートマトンを出力する。状態遷移出力部４０は、例えば、液晶ディスプレイ装置、プリンタ、外部記憶装置のファイルなどである。
【００２２】
［２．５．動作シナリオ入力部］
ユーザは、設計するシステムの動作例を複数のシナリオ（以下、「動作シナリオ」と呼ぶ）として記述する。動作シナリオ入力部５０は、この記述された動作シナリオ２００を受け付け、後述する検証モデル・検査式生成部６０に渡す機能を有する。動作シナリオ２００は時系列的な動作の順序を指定した記述である。本実施の形態では、動作シナリオ２００内に分岐は設けない。
【００２３】
［２．６．検証モデル・検証式生成部］
本発明の検証モデル・検証式生成手段に相当する検証モデル・検証式生成部６０は、入力された各動作シナリオ２００について、オートマトンがシナリオを最後まで実行可能であることを検証するモデル（検証モデル）、及び検証式を生成する。
【００２４】
［２．７．モデル検査部］
本発明の検査手段に相当するモデル検査部７０は、検証モデル・検証式生成部６０によって生成された検証モデルと検証式の組について、モデル検査を実行する。モデル検証部７０は、SPIN（http://www.spinroot.com参照）、NuSMV（http://nusmv.irst.itc.it/参照）等のモデル検査器を使用して実現してよい。どのようなモデル検査器によるものであっても、本実施の形態におけるモデル検査部７０として使用可能である。
【００２５】
［２．８．検査結果出力部］
モデル検査部７０による検査の実行結果を出力し、各動作シナリオ２００について、最後まで実行可能であるか否かを出力する機能を有する。
【００２６】
［３．入力］
次に、支援装置１にユーザにより入力される情報について説明する。
ユーザは、支援装置１に入力する情報として、動作規則１００および動作シナリオ２００を支援装置１に入力可能なデータとして準備する必要がある。以下に、動作規則１００及び動作シナリオ２００について説明する。
【００２７】
［３．１．動作規則］
まず、支援装置１に入力される情報である動作規則１００について説明する。  
「動作規則」は、設計したいシステムが持つ動作規則であって、当該システムが動作の順序について守るべき一般的な規則を記述したものである。ユーザによって記述される動作規則においては、個々の動作について唯一の名称が付けられている。以下に、支援装置１に入力される動作規則の例を挙げる。以下の説明では、Ａ、Ｂ、Ｃをそれぞれシステムの動作に付けられた名称であるものとする。
【００２８】
動作規則は、順序、選択、禁止、繰返しの組合せとして記述される。
「順序」とは動作の時系列的な前後関係のことである。本実施の形態では、「Aの後にBが動作する」という規則を「A->B」と記述する。
「選択」とは複数の動作から1つだけが実行されることである。本実施の形態では、「AとBのいずれかが動作する」という規則を「A|B」と記述する。
「禁止」とはその動作を行わないことである。本実施の形態では、「Ａが動作しない」という規則を「^A」と記述する。
「繰返し」とは順序、選択、禁止ないしそれらの組み合わせが０回以上繰り返されることである。本実施の形態では、順序「A->B」の繰返しを「(A->B)*」と記述する。
【００２９】
なお、上記の記述方式は一例に過ぎず、どのような記述方式で順序、選択、禁止、繰返しを記述する場合であっても、本発明は成立することはいうまでもない。
【００３０】
［３．１．１．動作規則のオートマトンへの変換方法］
オートマトン変換部２０は、入力された動作規則１００を順序、選択、禁止、繰返しの組み合わせとして解釈し、対応するオートマトンに変換する。以下に順序、選択、禁止、繰返しに対応するオートマトンを説明する。
【００３１】
図２に、順序に対応するオートマトンの例として、「Aの後にBが動作する」という動作規則「Ａ−＞Ｂ」に対応するオートマトンを示す。
【００３２】
図３に、選択に対応するオートマトンの例として、「AとBのいずれかが動作する」という規則「A|B」に対応するオートマトンの例を示す。
【００３３】
図４に、禁止に対応するオートマトンの例として、「Ａが動作しない」という規則「^A」に対応するオートマトンの例を示す。
【００３４】
図５は、繰返しに対応するオートマトンの例として、順序「A->B」の繰返し「(A->B)*」に対応するオートマトンの例を示す。
【００３５】
オートマトン変換部２０は上記の各動作規則の要素に対応するオートマトンの基本パターンを有しており、入力された動作規則１００を順序、選択、禁止、繰返しの要素に分解し、分解した要素に上記基本パターンを適用することで、動作規則１００に対応するオートマトンを生成する。
【００３６】
［３．２．動作シナリオ］
次に、支援装置１に入力されるもう一つの情報である動作シナリオ２００について説明する。
動作シナリオ２００は、設計したいシステムの動作シナリオである。「動作シナリオ」とは、そのシステムが実行可能な可能な動作の具体例を時系列的な順番に記述したものをいう。
【００３７】
例えば「最初にA、次にC、B、A、Bの順に動作を行う」という動作シナリオ２００は、以下のように記述される。
「A->C->B->A->B」
動作シナリオ２００には、条件分岐は無い。従って、Aの次にBを行う場合とCを行う場合があるなら「A->B」と「A->C」の2つのシナリオをそれぞれ記述する。
【００３８】
［４．出力］
支援装置１は、状態遷移設計のための情報として、動作規則１００からオートマトンを生成して、生成した各オートマトンの積を求め、得られた積を合成オートマトンとして出力する。この合成オートマトンは、全ての動作規則１００を組合わせて作成された1つの状態遷移である。
【００３９】
また、支援装置１は、上記合成オートマトンを検証モデルとして、このモデルの検証結果を出力する。すなわち、支援装置１は各動作シナリオ２００が動作規則１００に違反しないことを検証する。支援装置１は各動作シナリオ２００が合成された状態遷移仕様である、上記合成オートマトンを満たすことを検証する。
【００４０】
［５．動作（作用）］
次に、上記支援装置１の動作（作用）について説明する。
まず、ユーザが用意した動作規則１００が動作規則入力部１０に入力され、オートマトン変換部２０に渡されると、オートマトン変換部２０は、動作規則１００をオートマトンに以下に述べる方法により、変換する。
【００４１】
（１）動作規則１００において順序が指定されたら、オートマトン内で処理を逐次的に行う。
（２）動作規則１００において選択が指定されたら、オートマトン内で処理を排他的に１つだけ選んで行う。
（３）動作規則１００において禁止が指定されたら、オートマトン内で禁止されたもの以外の処理を繰返し、また禁止された処理が起きたらエラー状態へ遷移する。
（４）動作規則１００において繰返しが指定されたら、オートマトン内で指定の処理を繰返し行う。
（５）指定されなかった任意の動作については、オートマトンの全状態で動作可能とする。
（６）オートマトンが受理されないと見なすのはエラー状態のみである。
【００４２】
次に、上記の方法により動作規則１００から変換されたオートマトンは、オートマトン合成部３０に渡される。各動作規則１００から一つのオートマトンが生成され、動作規則１００が複数入力された場合は、複数のオートマトンがオートマトン合成部３０に渡される。
【００４３】
複数のオートマトンを受け取ったオートマトン合成部３０は、複数のオートマトンを合成し、新たな一つのオートマトン（「合成後オートマトン」と呼ぶ）を生成する。
【００４４】
例えば３つの異なる動作規則１００から3つのオートマトンX、Y、Zが生成されたものとする。オートマトン合成部３０は、各オートマトンで受理できる動作の集合を求め、これらの積集合を定義する。オートマトン合成部３０は、この積集合を表す1つのオートマトンを求め、それを合成オートマトンとして出力する。この合成オートマトンの生成は、全ての動作規則１００を同時に満たす動作を求めることを意味する。
【００４５】
なお、オートマトン合成部３０は、ＬＴＳＡ（Labelled Transition System Analyzer; http://www.edutool.com/ltsa/等参照）等の既存のツールにより実現することが可能である。
【００４６】
生成された合成オートマトンは、状態遷移出力部４０及び検証モデル・検証式生成部６０に渡される。
【００４７】
上記の動作規則１００とは別に、支援装置１にはユーザが用意した動作シナリオ２００が入力される。入力された動作シナリオ２００は、動作シナリオ入力部５０を介して、検証モデル・検証式生成部６０に渡される。
【００４８】
検証モデル・検証式生成部６０は、前述の合成オートマトンに基づく検証モデルと、入力された動作シナリオ２００に基づく検証モデルとを生成する。検証モデル・検証式生成部６０は、動作シナリオ２００の数と同じだけ、動作シナリオ２００に基づく検証モデルを生成する。
【００４９】
また、検証モデル・検証式生成部６０は、検証式の生成を行う。この検証式は、動作シナリオが最後まで到達することを確認する検証式である。
【００５０】
上記の検証モデル及び検証式は、モデル検査部７０が使用可能なものを検証モデル・検証式生成部６０は出力する。例えば、モデル検査部７０がＳＰＩＮモデル検査器である場合は、検証モデル・検証式生成部６０はこれに適合する検証モデル及び検証式を出力する。
【００５１】
［６．動作例］
次に、上述の支援装置１の動作例を挙げる。
［６．１．入力］
ここで説明する例において、支援装置１の入力は以下の内容であるものとする。
（１）動作規則
動作規則１００として以下の２つの動作規則が入力されるものとする。
(^(Read|Write)->Open->(Read|Write)*->Close)*  …（動作規則１）
(Read->Process->Write)*                       …（動作規則２）
【００５２】
（２）動作シナリオ
また、動作シナリオは以下の一つの動作シナリオ２００が入力されるものとする。
Open->Read->Process->Save->Write->Close    …（動作シナリオ）
【００５３】
［６．２．オートマトンの生成］
上記動作規則１及び動作規則２は、支援装置１のオートマトン変換部２０によってオートマトンに変換される。図６に上記動作規則１をオートマトン変換部２０がオートマトンに変換した結果を示す。また、図７に上記動作規則２をオートマトン変換部２０がオートマトンに変換した結果を示す。
【００５４】
［６．３．オートマトンの合成］
オートマトン合成部３０は、オートマトン変換部２０が生成したオートマトンを合成する。上記図６，図７に示す２つのオートマトンがオートマトン合成部３０に渡された場合、オートマトン合成部３０が合成する合成オートマトンを図８に示す。なお、図８中の符号Ｓ０からＳ５は、説明の都合上付けた状態の名称である。
【００５５】
［６．４．検証モデル、検証式の生成］
上記合成オートマトンは状態遷移出力部４０に渡されて出力されるとともに、検証モデル・検証式生成部６０に渡される。検証モデル・検証式生成部６０は合成オートマトン及び動作シナリオ２００に基づいて検証モデルを生成し、また検証式を生成する。
【００５６】
［Ａ．検証モデル］
検証モデル・検証式生成部６０は、各検証モデルを以下の手順で作成する。
（１）  合成オートマトンと動作シナリオから、動作の一覧を作成して、検証モデルのイベントとする。図９は、図８に示した合成オートマトン並びに動作シナリオから生成された検証モデルの記述例を示す。図９の検証モデルにおいて、「mtype」の定義が動作一覧から作成された検証モデルのイベントに該当する。
【００５７】
より具体的に、合成オートマトンからモデルを作る処理方法を説明する。図９において、合成オートマトンから作られた部分は記述９０１に相当する（「active proctype StateTransitionModel()」の行から次の「 ｝」までの部分）。
まず、合成オートマトンの状態一覧(図８では、図中Ｓ０〜Ｓ５に相当する)を探して、モデルの状態を定義する(図９に示す検証モデルの「state」変数の値が該当する)。
【００５８】
次に、各状態でイベントが発生した場合の遷移をモデルに記述する。
もし禁止されたイベントが起きたら、検証時に検出できるようにする(図９の検証モデルの変数forbiddenをtrueにする場合がこれに該当する)。
動作モデルに無いイベントが起きた場合には、そのイベントを無視する。
【００５９】
（２）上記の検証モデルに加えて、検証モデル・検証式生成部６０は動作シナリオ２００からも検証モデルを作る。動作シナリオ２００から生成された検証モデルは、図９の記述９０２に相当する（「active proctype Scenario()」の行から次の「 ｝」までの部分）。この検証モデルは、前述の動作シナリオ
「Open->Read->Process->Save->Write->Close」
から生成された検証モデルの例である。
【００６０】
より具体的には、検証モデル・検証式生成部６０は、動作シナリオ２００に記述された動作の順に、イベントを送る検証モデルを生成する。動作シナリオ２００の最後まで実行されたら、検証時に検出できるようにする(図９の検証モデルの変数finの値をtrueにする場合がこれに該当する)。
【００６１】
［Ｂ．検証式］
また、検証モデル・検証式生成部６０は、動作シナリオ２００が最後まで実行され、かつ合成オートマトンで禁止された動作が無いことを確認する検証式を生成する。図１０に、モデル検査部７０がＳＰＩＮにより構成されている場合の検証式の例を示す。
この例の場合、動作規則１００、動作シナリオ２００に関わらず、常に同じ検証式を使用するようにしてよい。
【００６２】
なお、図１０に示す検証式において、変数finがtrueならばシナリオが最後まで到達したことを意味する。また、変数forbiddenがfalseならばオートマトンで禁止されている動作が無かったことを意味する。
【００６３】
［６．５．検証の実施］
モデル検査部７０は、検証モデル・検証式生成部６０から検証モデルと検証式の組を複数受け取り、これらに基づいてモデル検査を実施して、検証結果(真か偽のいずれか)を生成する。すなわち、モデル検査部７０は検証モデル（例えば、図９に示す検証モデル）が検証式（例えば、図１０に示す検証式）の性質を満たすことを検証する。
【００６４】
検証結果が真の場合は、動作シナリオと動作規則の間に矛盾がないことを意味する。一方、検証結果が偽の場合は、動作シナリオと動作規則の間に矛盾があることを意味する。
【００６５】
［７．利点］
本発明の利点を以下に掲げる。
（１）状態遷移は自動的に合成されるので時間が掛からない
（２）ユーザが入力を行うと、即座に検証結果が出るので効率よく設計作業を行うことができる。
（３）設計を行うユーザは、モデル検査器に特有な検証モデルや検証式の書き方を覚える必要が無い。
（４）仕様の追加や変更があっても、状態遷移の修正や検証が即座にできる。
【図面の簡単な説明】
【００６６】
【図１】状態遷移設計支援装置の構成例を示した機能ブロック図
【図２】順序に対応するオートマトンの例を示す図
【図３】選択に対応するオートマトンの例を示す図
【図４】禁止に対応するオートマトンの例を示す図
【図５】繰返しに対応するオートマトンの例を示す図
【図６】動作規則１をオートマトン変換部がオートマトンに変換した結果を示す図
【図７】動作規則２をオートマトン変換部２０がオートマトンに変換した結果を示す図
【図８】図６，図７に示す２つのオートマトンがオートマトン合成部により合成された結果の合成オートマトンを示す図
【図９】図８に示した合成オートマトン、動作シナリオ「Open->Read->Process->Save->Write->Close」から生成された検証モデルの例を示す図
【図１０】モデル検査・検証式生成部によって生成される検証式の例を示す図
【符号の説明】
【００６７】
１…状態遷移設計支援装置
１０…動作規則入力部
２０…オートマトン変換部
３０…オートマトン合成部
４０…状態遷移出力部
５０…動作シナリオ入力部
６０…検証モデル・検証式生成部
７０…モデル検査部
８０…検査結果出力部
１００…動作規則
２００…動作シナリオ
【図１】
2010244140.tif 000003
【図２】
2010244140.tif 000004
【図３】
2010244140.tif 000005
【図４】
2010244140.tif 000006
【図５】
2010244140.tif 000007
【図６】
2010244140.tif 000008
【図７】
2010244140.tif 000009
【図８】
2010244140.tif 000010
【図９】
2010244140.tif 000011
【図１０】
2010244140.tif 000012