特許

J-GLOBAL ID：201003035345476169

状態遷移設計支援装置

発明者： 青木 翼 ,  藤原 聡子 ,  村田 由香里 ,  藤原 靖 ,  池田 信之
出願人/特許権者： 株式会社東芝
代理人 (3件)： 伊丹 勝 ,  田村 和彦 ,  中村 俊郎
公報種別：公開公報
出願番号（国際出願番号）：特願2009-089500
公開番号（公開出願番号）：特開2010-244140
出願日： 2009年04月01日
公開日（公表日）： 2010年10月28日
要約：

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

請求項（抜粋）：

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

IPC (1件)：

G06F 11/36

FI (1件)：

G06F9/06 620M

Fターム (4件)：

5B376BB05 ,  5B376BC32 ,  5B376BC70 ,  5B376BC71