Pat
J-GLOBAL ID：201303063948432722
モデル検査装置、モデル検査方法およびコンピュータプログラム
Inventor：
Applicant, Patent owner：
Agent (2)：
机 昌彦
, 下坂 直樹
Gazette classification：公開公報
Application number (International application number)：2011182262
Publication number (International publication number)：2013045269
Application date： Aug. 24, 2011
Publication date： Mar. 04, 2013
Summary：
【課題】 モデル情報に含まれている一部の制約条件(事前条件、事後条件、不変条件)を検証するモデル検査を可能にする。【解決手段】 モデル検査装置20は、検証対象指定部21と、検証対象判断部22と、検証コード変換部23と、モデル検査実行部24とを有している。検証対象指定部21は、モデル検査で用いるモデル情報に含まれる制約条件(事前条件、事後条件、不変条件)の中から、検証対象として指定された制約条件を示す指定情報を受け付ける。検証対象判断部22は、前記モデル情報に含まれる制約条件(事前条件、事後条件、不変条件)について、前記指定情報に基づいて、検証対象とするか否かを判断する。検証コード変換部23は、検証対象であると判断された前記制約条件と、前記モデル情報に基づき、検証コードを生成する。モデル検査実行部24は、前記検証コードに基づいてモデル検査を実行する。【選択図】 図11
Claim (excerpt)：
システムが行う処理、あるいは、ソフトウェアに基づいてコンピュータが実行する処理を検証するモデル検査で用いるモデル情報に含まれる制約条件であって前記処理を開始する際に満たされるべき事前条件、前記処理を終了した際に満たされるべき事後条件、および、前記処理の実行中に満たされるべき不変条件の中から、検証対象として指定された前記制約条件を示す指定情報を受け付ける検証対象指定部と、
前記モデル情報に含まれる前記制約条件である前記事前条件と前記事後条件と前記不変条件とのそれぞれについて、前記指定情報に基づいて、検証対象とするか否かを判断する検証対象判断部と、
前記検証対象判断部によって検証対象であると判断された前記制約条件について前記モデル検査を実行する手順を示す検証コードを、前記モデル情報に基づき生成する検証コード変換部と、
前記検証コードに基づいてモデル検査を実行するモデル検査実行部と
を有するモデル検査装置。
IPC (1)：
FI (1)：
F-Term (2)：
Return to Previous Page
