【摘要】对嵌入式操作系统类安全关键软件,测试、模拟、分析等传统软件验证方法不能保证其正确性,需要使用形式化方法。综述了主流商用嵌入式操作系统所采用的形式化验证方法,分析了操作系统内核不同特性的形式化验证思路。通常对空间隔离、信息流控制、系统调用、进程间通信等的证明采用定理证明方式,而对时间隔离的证明则采用模型检测方式。seL4的通用抽象和逐层精化方法、模型检测和定理证明的混合方法在工程使用中都有前 […]

【摘要】线性时态逻辑(LTL)现今已被广泛运用于计算机科学领域(CS)。它常作为描述系统行为的性质语言,用在程序验证、程序综合与人工智能(AI)等研究方向。比方说,为了验证给定的系统是否满足其对应的性质规范(通常是用LTL来书写的),模型检测技术会将该性质的否定转成与其等价的Buchi自动机,把它与系统模型求交得到新的自动机,并在这新的自动机上检查其接收的语言是否为空,从而可以判定系统是否满足该性 […]

【摘要】随着物联网、云计算、智能终端等新兴技术的快速发展,多样化的应用软件为用户提供了丰富的功能和服务。为了分散和简化应用逻辑,屏蔽不同软件间的差异性,提高软件的可重用性,组件化、专业化逐渐成为应用软件设计实现的发展趋势,不同软件间的相互协同与组合也成为了下一代网络服务提供及复杂软件系统功能开发的新模式。在该工作模式下,信息将在不同软件间交互和传输,而由于不同组件间的独立性和差异性,即使单一组件满 […]