基于xMAS模型的SpaceWire信誉逻辑的形式化验证

来源 :计算机科学 | 被引量 : 0次 | 上传用户：szmms

【摘要】

：

空间总线(SpaceWire)协议是应用于航空航天领域的高速通信总线协议,保证其可靠性至关重要。但是由于通信系统具有队列量、分布控制和并发性等特点,传统仿真模拟的验证方法存在不完备性的问题,采用模型检测方法对高层次属性进行验证时,通常会出现状态爆炸的问题。基于xMAS模型对SpaceWire通信系统中的信誉逻辑进行形式化建模、验证,xMAS模型既保留了底层的结构信息,又可以验证高层次的属性。对通信

【作者】

：

李艳春李晓娟关永王瑞张杰魏洪兴

【机构】

：

首都师范大学信息工程学院电子系统可靠性重点实验室,北京化工大学信息科学与技术学院,北京航空航天大学机械工程及自动化学院

【出处】

：

计算机科学

【发表日期】

：

2016年02期

【关键词】

：

xMAS模型信誉逻辑 SPACEWIRE 形式化验证 ACL2 xMAS model Credit logic SpaceWire Formal ver

下载到本地 , 更方便阅读

下载此文赞助VIP

声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架

论文部分内容阅读

其他文献

民用无人机飞行控制器软件设计

介绍了民用摄像无人机飞行控制器软件的功能需求。基于数据流图设计了软件的逻辑模型, 利用结构化方法设计了软件的模块构成。在程序权限分配和接口设计时采用了智能递阶控制思想。程序的多运行模式流程实现采用了多个互斥主循环加中断的结构。最终设计的飞行控制软件具有4个功能层次, 能够在飞控、测试和调参3种模式下运行。介绍了软件设计中的几项专门技术。所设计的软件具有功能集成度高、稳定性好、可扩展性强等特点。

期刊

飞行控制器软件设计无人机民用飞行控制软件结构化方法功能需求逻辑模型模块构成控制思想权限分配运行模式可扩展性图设计数据流功能层集成

VXI总线寄存器基器件中断请求器的设计与实现

在基于VXI总线的自动测试系统中,中断技术的使用加快了数据传输与处理的速度。文章首先详细地阐述了VXI总线的中断机制,进而提出了一种基于寄存器基器件的中断请求器的设计方案,并给出了硬件电路及软件代码。实际运行表明该设计具有硬件开销小,可移植性强等特点,完全符合VXI总线规范的要求。

期刊

VXI总线寄存器基器件中断请求器状态机AHDLVXIbus register - based element interrupt - requ

基于PCI总线的空调电控自动测试系统设计

文章针对空调电控板的测试原理,阐述了ADLINK工控机控制系统的特点,设计了一种新的基于PCI总线的空调电控自动测试系统.该系统包括硬件部分和软件部分,它提供了一个自动测试

期刊

PCI总线上控机数字脉冲模拟信号PCI bus industrial control computer digital impulse analo

某型舰空导弹武器系统调试信号源的设计

在某型舰空导弹武器系统调试信号源的设计中,基于便携性要求,利用PC104总线完成了系统硬件的构建,利用面向测控领域的软件开发平台Lab Windows/CVI进行了软件的开发,将RS422

期刊

系统调试导弹武器信号源WINDOWS/CVI设计PC104总线软件开发平台RS232C舰模拟产生数字信号RS422系统硬件测控领域问

发动机测试台循环水温度智能混合控制

介绍了发动机测试台循环水温度控制对象的建模,针对大滞后强耦合的特点,构造了一种新型的智能混合控制器,在近似解耦的基础上,利用专家控制思想,将Fuzzy和PID两种控制算法相

期刊

发动机智能混合控制FUZZYPIDengine intelligent combined control Fuzzy PID

ATLAS语言的ANSIC设计与实现

文章对ATLAS语言面向信号的测试理念及其方法描述进行了研究,针对ANSI C在测控领域之优点,通过追加一些新概念,提出了以ANSI C为核心,实现面向信号的测试程序设计思想.重点阐

期刊

ATLAS设计与实现语言程序设计思想测控领域操纵特性信号面向新概念测试ATLASANSI Coignal-orientedTPSsr

基于xMAS模型的SpaceWire信誉逻辑的形式化验证

其他学术论文