关键词：
实时嵌入式系统
中断
形式化方法
语义理论
程序统一理论
摘要：
随着计算机的发展,实时嵌入式系统被广泛应用于各个行业。相较于通用计算系统,嵌入式系统对安全性、可靠性、实时性以及稳定性都提出了更高的要求。它不仅要求系统实现逻辑正确,而且要求任务运行时可满足相应的时间限制。在实时嵌入式系统中,为了让系统可以及时地与外界环境进行交互,人们引入了“中断机制”。中断机制作为系统与外部设备连接的桥梁,使得系统可以随环境的变化而动态地、实时地做出相应的响应。然而,中断产生的随机性与不确定性却为系统埋下了内存安全和时间安全等方面的隐患。近年来,众多学者从不同的角度、采用不同的方法对中断进行了研究,其目的就是为了在保证中断机制正常运行的同时,提高此类系统的安全性指标。
本文以实时嵌入式系统中的中断机制为研究对象,在程序统一理论的指导下,提出可描述实时嵌入式系统的中断行为的抽象建模语言。该语言引入了时间、概率等信息,通过刻画程序的行为研究中断给程序行为、系统表现带来的时间安全问题。该语言中引进的概率程序算子结合了多种概率模型,不仅能更细致、准确地刻画中断环境的不确定性,也可以帮助系统设计者、开发者加深对中断的了解,减少中断对此类系统带来的安全隐患,显著提高此类系统的安全性。本文将提出的研究方法应用于汽车电子领域,结合基于AUTOSAR OS规范的操作系统与汽车发动机管理系统应用案例,验证了该研究方法的可行性与有效性。本文的研究方法有效地提高了系统设计、实现以及测试过程的工作效率,对实时嵌入式系统的开发起了重要的辅助作用。
本文的主要内容与贡献包括：
一、本文提出了三种用以描述实时嵌入式系统的中断机制的形式化语言：中断建模语言IML、带卫兵的中断建模语言gIML以及带概率的中断建模语言pIML；三种语言的依次提出展示了本文对中断的研究过程。gIML是IML的扩展,pIML是gIML的扩展；三种语言可用于研究不同抽象层次的中断机制。它们不仅包括了常见的程序,如带时间的赋值程序、串行组合程序,而且包括关于中断特征的程序,如解除屏蔽程序、屏蔽中断程序、概率打断程序。pIML中引入的概率信息,使得我们不仅能对中断行为进行定性分析,还能对中断行为进行更为准确、精致的定量分析。
二、本文给出了三种中断建模语言的两种语义模型：操作语义和指称语义。操作语义的迁移规则直观地模拟了程序是如何运行的。而指称语义从更为抽象的层次利用数学论域中的对象来描述程序的行为。两种语义都包涵了时间、概率信息,分析与讨论了系统在中断环境下的时间安全问题。本文在操作语义框架下通过互仿真定义了程序的等价性,并推导出一些关于中断的代数规则。同时,这些代数规则也在指称语义的框架下得到了证明。本文还研究了操作语义与指称语义的一致性问题。
三、本文提出了带概率的中断建模语言pIML的应用。pIML包含了时间、概率信息,从定量的角度清晰地展示了中断发生对程序运行造成的影响。本文利用工具Maude仿真了pIML的概率操作语义,仿真结果可以协助程序员观察与分析程序运行的状况。pIML的概率指称语义也可以直接用于计算程序在中断影响下的运行时间与对应概率。本文提出可以引入概率分布函数来模拟实际应用场景的中断环境,从而对程序行为进行定量分析,帮助程序员预测系统的表现。本文还以基于AUTOSAR OS规范实现的操作系统与汽车发动机管理系统为例,通过pIM(?)L描述的程序来展示中断的准时发生对实时系统的重要性。
欢迎来到三峡大学图书馆！
