摘要：随着星载计算机系统功能的日益复杂,程序规模也在快速扩大.在存储资源极其受限的背景下,需要稳定、有效的代码压缩功能来保障星载软件的正常存储与运行.混合压缩算法是目前无损数据压缩的主流算法,具有压缩率高、代码规模和计算资源需求大的特点.然而,在航天星载计算机等嵌入式系统中,由于其运行环境特殊,需要较高的可靠性和抗干扰能力,无法实现混合压缩算法应有的效果.同时,单一压缩模型压缩率较低.针对以上问题,在LZ77算法代码体积和内存消耗优势的基础上提出了改进方法:为压缩过程设计一种新的匹配记录表以存储高价值数据索引来辅助压缩,实现了原算法局部性优势与高价值数据全局分布的互补,更大程度上减少了数据冗余;结合动态填充、变长编码等进一步优化编码结构,降低存储需求;最终,设计并实现了一种更加适合航天嵌入式环境的无损数据压缩算法(LZRC).实验结果表明:(1)新算法在比LZ77算法代码体积仅多出3.5 KB的条件下,对软件代码的平均压缩比提高了17%;(2)新算法的运行内存需求仅为混合压缩算法的12%,代码体积也减少了84%,更加适合星载计算机系统.

摘要：安全关键系统的失败会造成很严重的后果,确保其正确性非常重要.空间嵌入式操作系统是一个典型的安全关键系统,在其内存管理的设计上,必须保障其高效的分配与回收,同时对系统资源的占用降到最低.在传统的软件开发过程中,通常是在整个软件开发结束后再进行集中测试及验证,这样势必会造成开发进展的不确定性.因此,将形式化验证方法和软件工程领域内的“需求-设计-实现”的3层开发框架相结合,通过性质分层传递验证的方法,保证了各个层次间的一致性.首先,从需求层面的需求分析开始,引入形式化证明的思路,证明对需求层逻辑的正确性,从而可以更好地指导程序的设计.其次,在设计层面的验证可以极大地减少开发代码的错误率,证明设计算法和需要实现的函数之间调用逻辑的正确性.最后,在实现层,证明所实现代码与函数设计的一致性,并且证明代码实现的正确性.使用交互式定理证明辅助工具Coq,以某一国产空间嵌入式操作系统的内存管理模块为例,证明了其内存管理算法的正确性以及需求、设计、实现的一致性.

摘要：在航天器上采用FLASH设备作为存储介质,需要采用文件系统来管理存储设备.在航天嵌入式系统中,数据存储的规模越来越大,进行采集任务产生的数据量将达到TB级别.出于安全性的考虑,航天器嵌入式系统内存容量受限,并且实时性要求极高.普通嵌入式系统在内存容量和实时性的要求同航天嵌入式系统相差较多,因此不适用于航天嵌入式系统.本文针对航天器系统资源受限的特殊需求,对嵌入式系统中常用的YAFFS2文件系统中存在的内存中文件索引结构占用空间随文件数据量线性增长的问题,提出基于二元组索引的低内存开销快速文件管理(Low Overhead and Fast File Management based on Binary group,BLOF)方法,通过基于B+树引入二元组链表结构对连续FLASH页进行统一索引,并依据索引结构设计文件读、文件写操作算法,具有文件系统内存占用小,读写文件速度快的特点.实验结果表明,BLOF相比于YAFFS2索引方法,对任意数据量的文件:1)当文件数据所在闪存页达到平均6个页以上连续时,BLOF方法内存占用低于YAFFS2方法,最高节省55.55%;2)在文件规模大于512KB时,BLOF方法的文件读写时间始终小于YAFFS2的文件读写时间,并且YAFFS2文件写时间和BLOF写时间之差随文件大小呈线性增长趋势.BLOF方法更适合于文件数据量大且存储在大量连续页的情境下.

摘要：形式化验证方法被认为是一种构建高可信软件系统的有效手段.在定理证明工具通过手动写证明脚本来验证系统软件的功能正确性,这种验证方式表达力强,可以证明复杂系统,但是自动化程度低、验证代价比较高;而使用程序验证器接受经过规范标注的源代码生成验证条件,并将验证条件交给约束求解器自动求解,这种方式自动化程度高,缺点在于它很难验证复杂系统软件的全部功能的正确性.结合上述两种方式的优点,在定理证明工具Coq中实现了一个自动证明策略smt4coq,它通过在Coq中调用约束求解器Z3自动证明32位机器整数相关的数学命题,提高了自动化验证的程度,减少了用户手动验证程序的开销.

摘要：基于可信硬件构建安全关键应用的可信执行环境(TEE),是嵌入式安全领域的一个研究热点。虽然底层硬件可信,但TEE软件仍可能因错误使用硬件指令或存在其他安全漏洞而导致机密信息泄露。该文基于ARM TrustZone技术提出了多层次的TEE架构,并建立了安全通信通道,用户层可信应用不能直接访问非可信环境的软硬件资源,只能通过内核层的安全通信通道API与外界通信,因此整个TEE的信息流不再受用户层影响。该文进一步提出了TEE形式化模型(TEEFM),借助Coq辅助证明器验证了TEE信息流无干扰性并证明了TEE安全监控模块不存在整型溢出、程序返回地址异常等资源边界类软件漏洞,以此保证了TEE的自身安全性。

摘要：形式化方法是基于严格数学基础,对计算机硬件和软件系统进行描述、开发和验证的技术.其数学基础建立在形式语言、语义和推理证明三位一体的形式逻辑系统之上.形式化方法已经以不同程度和不同方式愈来愈多地应用在计算系统生命周期的各个阶段.介绍了形式化方法的发展历程和基本方法体系;以形式规约和形式验证为主线,综述了形式化方法的理论、方法、工具和应用的现状,展示了形式化方法与软件学科其他领域的交叉和融合;分析了形式化方法的启示,并展望了其面临的发展机遇和未来趋势.形式化方法的发展和研究现状表明:其应用已经取得了长足的进步,在提高计算系统的可靠性和安全性方面发挥了重要作用.在当今软件日益成为社会基础设施的时代,形式化方法将与人工智能、网络空间安全、量子计算、生物计算等领域和方向交叉融合,得到更加广阔的应用.研究和建立这种交叉融合的理论和方法不仅重要,而且具有挑战性.

摘要：随着软件复杂度的迅速增长,传统的基于测试的方法逐渐难以满足航天器操作系统的可靠性和安全性需求,形式化方法逐渐成为航天器操作系统安全可靠性的有效保障.基于Rodin平台,采用Event-B形式化语言,通过需求和设计重写、制定精化策略并逐步精化的方法,对航天嵌入式操作系统SpaceOS2的中断管理模块建立了需求层和设计层形式化模型,将模型检验和定理证明相结合,验证模型的正确性并且满足安全性质.

摘要：开展基于模型设计研究,旨在解决当前航天器控制软件研制所面临的需求描述准确性、设计验证充分性以及软件产品可靠性等问题.针对基于模型设计过程中的代码胶合接口复杂且操作繁琐问题,提出一种基于模型架构的航天器控制软件研制方式,搭建软件模型驱动框架,通过模型封装方式将既有代码资产或新编写代码嵌入到软件模型驱动框架,简化代码胶合过程.同时,建设航天器控制领域通用模型库来提高成熟算法模型的复用效率及自动生成代码可靠性.本方法研究为推进航天器控制软件向模型驱动开发方式转变夯实基础.

摘要：SpaceOS是北京控制工程研究所自主研发的嵌入式实时操作系统,已被应用于探月工程、空间站等重大航天项目.SpaceOS作为底层系统软件,是影响航天任务成败的关键因素. SpaceOS在设计中提出了一些多个内核模块(如任务管理、调度、通信和时间管理等)相互协同过程中所需要满足的全局性质.本文扩展已有的操作系统验证框架支持全局性质的推理,为SpaceOS内核建立抽象模型,给出主要系统调用的抽象规范,并基于设计需求给出形式化定义描述若干全局性质,通过严格的数学证明保证SpaceOS在抽象设计层面上满足这些全局性质.所有工作都在证明助手Coq中完成.

摘要：为了保证一种非常经典的适用大规模存储地NAND闪存上的DFTL算法的正确性,对DFTL算法采用了形式化建模的方法来建立一个高可信的形式化模型.根据DFTL算法提出者的设计,我们以此为依据,对DFTL算法的基本数据结构,读写操作和垃圾回收操作以及基本性质进行了形式化的建模和验证,并对文中提出的垃圾回收算法进行了适当的修改和优化,以证明垃圾回收算法的正确性.最后我们针对DFTL算法,设计了一个验证框架,在这个验证框架和形式化的NAND闪存模型的基础上,对DFTL算法的的一些基本性质进行了验证.