首页> 中文会议>2018年第十五届全国工业控制计算机学术年会 >SpaceOS2汇编代码的形式化建模与验证方法

SpaceOS2汇编代码的形式化建模与验证方法

页面导航

摘要
著录项
相似文献
相关主题

摘要

航天嵌入式操作系统SpaceOS2的代码有一部分是用汇编语言实现的,要对其进行验证,首先要对汇编代码进行建模.本文基于Coq平台,在SPARC V8指令集形式化模型框架的基础上,根据SpaceOS2中断管理建模和验证的需要,对原框架进行了补充,在此基础上对中断管理模块的汇编代码进行形式化建模,验证了TrapEnable函数的正确性,给出了汇编代码正确性验证方法和理论依据.

著录项

来源
《2018年第十五届全国工业控制计算机学术年会》||266-273|共8页
会议地点广东佛山
作者
周育逵; 乔磊; 杨桦;
展开▼
作者单位

中国计算机学会;

展开▼
会议组织
正文语种
原文格式 PDF
中图分类
关键词
航天器; 嵌入式操作系统; 汇编代码; 形式化建模; 正确性; 验证方法;

相似文献

中文文献
外文文献
专利

1. 基于Event-B的SpaceOS2操作系统任务管理需求形式化建模与验证 [J] . 谭彦亮 ,杨桦 ,乔磊 . 空间控制技术与应用 . 2014,第004期
2. 操作系统汇编级形式化设计和验证方法 [J] . 钱振江 ,黄皓 ,宋方敏 . 软件学报 . 2016,第012期
3. 一种面向UEFI模块的形式化建模与验证方法 [J] . 王冠 ,郝晓星 . 计算机技术与发展 . 2021,第012期
4. 一种代币智能合约的形式化建模与验证方法 [J] . 欧阳恒一 ,熊焰 ,黄文超 . 计算机工程 . 2020,第010期
5. 面向新兴系统的形式化建模与验证方法专题前言 [J] . 陈振邦 ,冯新宇 ,刘志明 . 软件学报 . 2020,第8期
6. 一种动静结合的代码反汇编框架 [C] . XI Qi ,奚琪 ,ZENG Yong-jun . 2013中国计算机大会 . 2013
7. 工业控制系统网络安全形式化建模验证方法研究 [A] . 项露露 . 2020

SpaceOS2汇编代码的形式化建模与验证方法

摘要

著录项

相似文献

相关主题

期刊订阅