首页>
外国专利>
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.
展开▼