一个集成形式化模型及其操作语义

摘要

形式化方法在程序验证、模型检测的研究有着重要作用,集成形式化方法是形式化方法发展的一个方向.BCCS模型是集成B方法和进程代数CCS构建的一个混成模型,模型中给出了一个轻量级的描述语言,但缺少语义的支持.为了保证这个描述语言的完备性和一致性,本文则在传值CCS操作语义的基础上,结合B方法对抽象数据结构的定义、系统的限制以及功能处理,给出了BCCS的操作语义,进一步刻画BCCS模型.