首页> 美国政府科技报告 >Compositional Verification of a Network of CSP Processes: Using FDR2 to Verify Refinement in the Event of Interface Difference.
【24h】

Compositional Verification of a Network of CSP Processes: Using FDR2 to Verify Refinement in the Event of Interface Difference.

机译:Csp过程网络的组合验证:使用FDR2验证接口差异事件中的细化。

获取原文

摘要

The authors previously presented an implementation relation formalizing what it means for one process to 'implement' another in the CSP (Communicating Sequential Processes) framework in the event that the two processes have different interfaces. This implementation relation allows for compositional verification of a network of CSP processes. The model checker FDR2 may be used to check CSP refinement in the event that specification and implementation processes have the same interface. In this paper, the authors show how to transform the problem of checking the conditions from the implementation relation, where the specification and implementation processes have different interfaces, into one where the specification and implementation processes have the same interface. This allows the authors to take advantage of the existing tool FDR2 and allows automatic, compositional verification using the relation developed.

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号