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

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. The proposal focuses on hierarchical formal modelling, verification and reliability analysis of NOC，which is taken SPACEWIRE(SpW) as application case, and explores the co-verification of hardware and software on NOC. Moreover, the rigorous correctness verification and reliability analysis for NOC are integrated. Data-flow based modelling with the high level structural information of the system can also capture the timing and functionality about the hardware design, which effectively avoid the space explosion problem for control-centric states modelling. The Markov models for the uncertainty properties of the data link queues are established in order to performance analysis. Concurrency and random behaviors of transport protocol for NOC are formalized within the High Order Logic, and the statistic properties are extracted in the form of mathematical logic functions, which can be used for reliability analysis of transport process. The NOC verification will be achieved from RTL to high transport protocol level.

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

对安全攸关应用的总线网络系统，仅采用传统的模拟、测试方法无法满足其正确性和可靠性验证需求。本项目首先以SpW为用例,研究总线网络链路接口设计及通信协议的层次化形式建模、验证及可靠性分析方法；并以此为基础，提出较为通用的嵌入式系统网络接口的正确性和可靠性的层次化验证和分析方法, 实现严格的功能正确性验证与量化性能分析的结合。研究面向数据流的网络接口微体系结构的形式表达建模方法，建立了图形化元件的形式表达库，在保留其时序和功能细节信息的前提下，提高了抽象层次，有效避免以控制流为中心建模导致的状态空间爆炸问题。基于图形模型符号化库，创建了面向片上网络验证需求的xMAS模型库，并且在已有元件基础上，创建了一个可以描述数据流优先级的新xMAS元件，并在定理证明工具ACL2中进行形式表达和属性的验证，可实现运用ACL2对SPW及CAN总线等通信系统关键属性正确性的自动验证。基于马尔科夫决策过程建立模型通信过程的模型，建立时间自动机模型对链路设计进行验证和分析，获得在不同信道质量情况下总线协议的工作性能；提取关键属性的逻辑表达函数，量化分析协议的可靠性。据此总结出从较低抽象层RTL 实现到较高抽象层传输协议的嵌入式系统网络接口形式化建模、验证方法，并将该方法用于机器人分布式控制的总线传输系统的设计和验证。本项目研究层次化、模块化的SOC网络通信系统形式建模和自动验证方法，为通信总线系统的设计人员进行验证下的设计、避免设计阶段的bug和系统可靠性保证及性能分析等方面提供了有效参考。