基本信息:
- 专利标题： Counter example analysis support apparatus
- 专利标题（中）：Vorrichtung zurUnterstützungder Analyze von Gegenbeispielen
- 申请号：EP08162819.0 申请日：2008-08-22
- 公开(公告)号：EP2063368A2 公开(公告)日：2009-05-27
- 发明人： Takada, Satoko , Murata, Yukari , Ikeda, Nobuyuki
- 申请人： Kabushiki Kaisha Toshiba
- 申请人地址： 1-1, Shibaura 1-chome Minato-ku, Tokyo 105-8001 JP
- 专利权人： Kabushiki Kaisha Toshiba
- 当前专利权人： Kabushiki Kaisha Toshiba
- 当前专利权人地址： 1-1, Shibaura 1-chome Minato-ku, Tokyo 105-8001 JP
- 代理机构： HOFFMANN EITLE
- 优先权： JP2007296713 20071115
- 主分类号： G06F17/50
- IPC分类号： G06F17/50
摘要：
A counter example analysis support apparatus includes a counter example storage storing the counter example being a transition sequence of state and event that has not satisfied a verification condition as a result of the model checking; comprising: a related item list storage storing a related item list being a list associating a detection event, which is an event for detecting and generating the other-state, and a detected state, which is a state for determining the existence of the generation of the detection event; and a searching unit outputting a possible problem part from the counter example, wherein the searching unit determines whether a state included in the counter example is the detected state, and if the state included in the counter example is the detected state, determines whether a detection event corresponding to the related item list is generated before the detected state transits to a next state.
摘要（中）：
计数器示例分析支持装置包括存储作为模型检查结果不满足验证条件的状态和事件的转换序列的计数器示例的计数器示例存储器; 包括：相关项目列表存储，存储作为用于检测和生成另一状态的事件的检测事件关联的列表的相关项列表以及用于确定是否存在生成的状态的检测状态 检测事件; 以及搜索单元，从计数器示例输出可能的问题部分，其中搜索单元确定计数器示例中包括的状态是否是检测状态，并且如果计数器示例中包括的状态是检测状态，则确定检测 在检测到的状态转换到下一状态之前生成与相关项列表相对应的事件。
公开/授权文献:
- EP2063368A3 Counter example analysis support apparatus 公开/授权日：2010-03-10