【摘要】随着互联网的普及和云计算的发展,海量数据处理成为IT从业人员越来越重视的课题。海量数据处理常采用并发的方法,即多个线程同时运行在多台处理器上,共同访问和处理共享数据。由于多个线程的交互,并发程序的行为更难以预测,出现的错误也更难以定位。因此,通过严谨的数学方法在逻辑上验证一个并发程序的正确性很有意义。无锁并发跳表是一种无需对各个节点加锁就能实现多个线程同时无阻塞操作的数据结构,其存取时间复 […]

【摘要】近年来随着嵌入式设备的日益普及,嵌入式软件的安全性越发显得重要。在一些关键领域,如航天、医疗、军事、核能等,如果嵌入式软件存在程序漏洞,有可能导致程序在非正常状态运行,从而会带来灾难性的后果。为了解决这一类的可靠性问题,传统软件开发者通常会采用软件测试的方法去发现程序错误。但是,软件测试无法保证整个系统完全不存在缺陷。程序验证探寻一条逻辑验证为基础的解决软件安全性的道路。程序验证能够克服软 […]

【摘要】随着嵌入式技术、计算机技术和网络技术的不断发展，以及硬件产品性能和数据处理能力的不断提升，物联网技术得到快速发展。在此背景之下，信息-物理融合系统（Cyber-PhysicalSystems,CPS）作为一种新型嵌入式网络系统应运而生，并且引起了各国政府、学术界和工业界的高度重视。CPS是融合了计算和物理进程的复杂嵌入式网络系统，它通过嵌入式系统和网络对物理设备进行监测和控制，并通过反馈机 […]

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