空间通信片上网络数字系统形式化验证与可靠性分析

项目名称： 空间通信片上网络数字系统形式化验证与可靠性分析

项目编号： No.61373034

项目类型： 面上项目

立项/批准年度： 2013

项目学科： 自动化技术、计算机技术

项目作者： 李晓娟

作者单位： 首都师范大学

项目金额： 76万元

中文摘要： 空间通信片上网络系统(SpW)是空间设备数据通信的关键技术。对这类安全攸关应用的片上网络系统，仅采用传统的模拟、测试方法无法满足其正确性和可靠性验证需求。本项目拟以SpW为用例,研究片上网络链路接口设计及通信协议的层次化形式建模、验证及可靠性分析方法；探索片上网络软硬件协同验证, 实现严格的功能正确性验证与量化性能分析的结合。面向数据流，直接基于硬件设计的结构进行形式建模，在保留其时序和功能细节信息的前提下，提高了抽象层次，有效避免以控制流为中心建模导致的状态空间爆炸问题。抽象端口队列的非确定属性，建立Markov 模型进行性能分析。建立协议并发、随机行为的高阶逻辑模型, 提取关键属性的逻辑表达函数，量化分析协议的可靠性。据此总结出从较低抽象层RTL 实现到较高抽象层传输协议的NOC 形式化建模、验证方法。

中文关键词： 形式化验证；空间总线；xMAS；网络总线系统；

英文摘要： Network-On-Chip for SPACEWIRE is the key technology for communication between devices in space engineering. The traditional test or simulation verification can not satisfy the critical safety NOC requirements for correctness and reliability verification.

英文关键词： formal verification；Spacewire；excutable Microarchitectural Specification；network bus system；