公开(公告)号：US20050278669A1

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

申请号：US11119443

申请日：2005-04-28

申请人： Thomas Sidle ,  Christian Stangier ,  Koichiro Takayama

发明人： Thomas Sidle ,  Christian Stangier ,  Koichiro Takayama

IPC分类号： G06F17/50

CPC分类号： G06F17/504

摘要： In one embodiment, a method for invariant checking includes executing one or more first steps of a finite state machine (FSM) corresponding to one or more binary decision diagrams (BDDs) to traverse a state space of the FSM in a first direction with respect to an initial state and an erroneous state. The method also includes, automatically and without user input, accessing a first profile corresponding to the one or more first steps of the FSM, comparing the first profile with one or more first predetermined criteria, stopping the traversal of the state space in the first direction according to the comparison between the first profile and the one or more first predetermined criteria, executing one or more second steps of the FSM to traverse the state space in a second direction with respect to the initial state and the erroneous state opposite the first direction according to a first partial result from the one or more first steps of the FSM, accessing a second profile corresponding to the one or more second steps of the FSM, comparing the second profile with one or more second predetermined criteria, stopping the traversal of the state space in the second direction according to the comparison between the second profile and the one or more second predetermined criteria, and executing one or more third steps of the FSM to traverse the state space in the first direction from the one or more first steps according to a second partial result from the one or more second steps of the FSM.

摘要翻译： 在一个实施例中，用于不变检查的方法包括执行与一个或多个二进制判定图（BDD）相对应的有限状态机（FSM）的一个或多个第一步骤，以相对于第一方向遍历FSM的状态空间 初始状态和错误状态。 该方法还包括自动地且没有用户输入，访问对应于FSM的一个或多个第一步骤的第一简档，将第一简档与一个或多个第一预定标准进行比较，停止第一方向上的状态空间的遍历 根据第一轮廓和一个或多个第一预定标准之间的比较，执行FSM的一个或多个第二步骤以相对于初始状态的第二方向和与第一方向相反的错误状态横穿状态空间， 到FSM的一个或多个第一步骤的第一部分结果，访问对应于FSM的一个或多个第二步骤的第二简档，将第二简档与一个或多个第二预定标准进行比较，停止遍历状态 根据第二轮廓和一个或多个第二预定标准之间的比较，执行第二方向的空间 根据来自FSM的一个或多个第二步骤的第二部分结果，从所述一个或多个第一步骤中删除所述FSM的一个或多个第三步骤沿所述第一方向穿过所述状态空间。