公开(公告)号：US20050278153A1

公开(公告)日：2005-12-15

申请号：US10853526

申请日：2004-05-25

申请人： Roy Armoni ,  Limor Fix ,  Alon Flaisher ,  Nir Piterman ,  Andreas Tiemeyers ,  Moshe Vardi

发明人： Roy Armoni ,  Limor Fix ,  Alon Flaisher ,  Nir Piterman ,  Andreas Tiemeyers ,  Moshe Vardi

IPC分类号： G06F9/45 ,  G06F17/50

CPC分类号： G06F17/504

摘要： Modifying a specification of a design by replacing a sub formula of the specification with a free variable; model checking the modified specification in a model to determine whether the modified specification is satisfied in the model; and determining whether the sub formula affects satisfaction of the specification in the model based on determining whether the modified specification is satisfied in the model.

摘要翻译： 通过用自由变量替换规范的子公式来修改设计规范; 模型检查模型中的修改规范，以确定模型中是否满足修改后的规范; 并且基于确定模型中是否满足修改的规范，确定子公式是否影响模型中的规范的满足。