首页>
外国专利>
MODEL CHECKING OF LIVENESS PROPERTY IN A PHASE ABSTRACTED MODEL
MODEL CHECKING OF LIVENESS PROPERTY IN A PHASE ABSTRACTED MODEL
展开▼
机译:阶段抽象模型中的生活财产模型检查
展开▼
页面导航
摘要
著录项
相似文献
摘要
Phase abstraction may be utilized to increase efficiency of model checking techniques. A liveness property may be checked in respect to a phase abstracted model by modifying the liveness property in accordance with the phase abstracted model. A fairness property may be modified to ensure that the fairness property is held by the model checker. A counter-example produced by a model checker is modified to be in accordance to an original model. The counter-example comprises a repetitive behavior. The counter-example may be modified to shorten the repetitive behavior or to apply the repetitive behavior in an earlier cycle of the counter-example.
展开▼