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