【摘 要】
：
Exception management,as the lowest level function module of the operating system,is responsible for making abrupt changes in the control flow to react to exception events in the system.The correctness of the exception management is crucial to guaranteeing
【机 构】
：
Beijing Institute of Control Engineering,Beijing 100190,China;China Academy of Space Technology,Beij
论文部分内容阅读
Exception management,as the lowest level function module of the operating system,is responsible for making abrupt changes in the control flow to react to exception events in the system.The correctness of the exception management is crucial to guaranteeing the safety of the whole system.However,existing formal verification projects have not fully considered the issues of exceptions at the assembly level.Especially for real-time operating systems,in addition to basic exception handling,there are nested exceptions and task switching by exceptions service routine.In our previous work,we used high-level abstraction to describe the basic elements of the exception management and verified correctness only at the requirement layer.Building on earlier work,this paper proposes EMS(Exception Management SPARCv8),a practical Hoare-style program framework to verify the exception management based on SPARCv8(Scalable Processor Architecture Version 8) at the design layer.The framework describes the low-level details of the machine,such as registers and memory stack.It divides the execution logic of the exception management into six phases for comprehensive formal modeling.Taking the executing scenario of the real-time operating system SpaceOS on the Beidou-3 satellite as an example,we use the EMS framework to verify the exception management.All the formalization and proofs are implemented in the interactive theorem prover Coq.
其他文献
Many applications need to meet diverse requirements of a large-scale distributed user group.That challenges the current requirements engineering techniques.Crowd-based requirements engineering was proposed as an umbrella term for dealing with the requirem
Programmable logic controllers(PLCs)play a critical role in many industrial control systems,yet face in-creasingly serious cyber threats.In this paper,we propose a novel PLC-compatible software-based defense mechanism,called Heterogeneous Redundant Proact
Allocation,dereferencing,and freeing of memory data in kernels are coherently linked.There widely exist real cases where the correctness of memory is compromised.This incorrectness in kernel memory brings about significant security issues,e.g.,information
A quantum circuit is a computational unit that transforms an input quantum state to an output state.A natural way to reason about its behavior is to compute explicitly the unitary matrix implemented by it.However,when the number of qubits increases,the ma
Contextual refinement is a compositional approach to compositional verification of concurrent objects.There has been much work designing program logics to prove the contextual refinement between the object implementation and its abstract specification.How
The Linux kernel adopts a large number of security checks to prevent security-sensitive operations from being executed under unsafe conditions.If a security-sensitive operation is unchecked,a missing-check issue arises.Missing check is a class of severe b
Graph neural networks(GNNs) have shown great power in learning on graphs.However,it is still a challenge for GNNs to model information faraway from the source node.The ability to preserve global information can enhance graph representation and hence impro
Dialogue state tracking(DST)leverages dialogue information to predict dialogues states which are generally represented as slot-value pairs.However,previous work usually has limitations to efficiently predict values due to the lack of a powerful strategy f
中文命名实体识别(NER)任务是信息抽取领域内的一个子任务,其任务目标是给定一段非结构文本后,从句子中寻找、识别和分类相关实体,例如人名、地名和机构名称.中文命名实体识别是一个自然语言处理(NLP)领域的基本任务,在许多下游NLP任务中,包括信息检索、关系抽取和问答系统中扮演着重要角色.全面回顾了现有的基于神经网络的单词-字符晶格结构的中文NER模型.首先介绍了中文NER相比英语NER难度更大,存在着中文文本相关实体边界难以确定和中文语法结构复杂等难点及挑战.然后调研了在不同神经网络架构下(RNN、CNN
组合最优化问题(COP)的求解方法已经渗透到人工智能、运筹学等众多领域.随着数据规模的不断增大、问题更新速度的变快,运用传统方法求解COP问题在速度、精度、泛化能力等方面受到很大冲击.近年来,强化学习(RL)在无人驾驶、工业自动化等领域的广泛应用,显示出强大的决策力和学习能力,故而诸多研究者尝试使用RL求解COP问题,为求解此类问题提供了一种全新的方法.首先简要梳理常见的COP问题及其RL的基本原理;其次阐述RL求解COP问题的难点,分析RL应用于组合最优化(CO)领域的优势,对RL与COP问题结合的原理