Pat

J-GLOBAL ID：201003035345476169

状態遷移設計支援装置

Inventor： 青木 翼 ,  藤原 聡子 ,  村田 由香里 ,  藤原 靖 ,  池田 信之
Applicant, Patent owner： 株式会社東芝
Agent (3)： 伊丹 勝 ,  田村 和彦 ,  中村 俊郎
Gazette classification：公開公報
Application number (International application number)：2009089500
Publication number (International publication number)：2010244140
Application date： Apr. 01, 2009
Publication date： Oct. 28, 2010
Summary：

【課題】状態遷移を動作規則から自動的に合成するとともに、合成された状態遷移が動作シナリオと矛盾しないかどうかのモデル検査器による検証結果を同時に出力し、モデル検査のための検証モデルと検証式はいずれも自動的に生成する。【解決手段】ユーザから入力された動作規則を、オートマトンの形式に変換するオートマトン生成部と、前記オートマトンの積を求め、それを合成オートマトンとして出力するオートマトン合成部と、ユーザから入力された各動作シナリオと前記合成オートマトンとに基づいて検証モデルを生成するとともに、前記動作シナリオが最後まで実行され、かつ前記合成オートマトンで禁止された動作が無いことを確認する検証式を生成する検証モデル・検証式生成部と、前記検証モデルと検証式とを用いて、モデル検査を実行する出る検査部とを有する状態遷移設計支援装置。【選択図】図1

Claim (excerpt)：

ユーザから入力された動作規則を、オートマトンの形式に変換するオートマトン生成手段と、 前記オートマトンの積を求め、それを合成オートマトンとして出力するオートマトン合成手段と、 ユーザから入力された各動作シナリオと前記合成オートマトンとに基づいて検証モデルを生成するとともに、前記動作シナリオが最後まで実行され、かつ前記合成オートマトンで禁止された動作が無いことを確認する検証式を生成する検証モデル・検証式生成手段と、 前記検証モデルと検証式とを用いて、モデル検査を実行する検査手段と を有することを特徴とする状態遷移設計支援装置。

IPC (1)：

G06F 11/36

FI (1)：

G06F9/06 620M

F-Term (4)：

5B376BB05 ,  5B376BC32 ,  5B376BC70 ,  5B376BC71