论文部分内容阅读
随着计算机科学和信息产业的不断发展,实时系统在社会生产和人民生活中有着广泛而深入的应用,如视频点播、信息采集与检索系统,信息物理融合系统(CPS),航空航天、军事、核工业等。相对于一般的软件系统,实时系统有着更严格的需求规范,对外部事件的响应有着非常严格的时间约束,实时系统所面临的外部环境可能非常恶劣,外部环境的变化可能非常剧烈,安全性的要求更高,并且可能要求系统本身具备一定的可生存性,实时系统本身可能是分布式的,规模和复杂度更高,测试难度极大。因此实时系统的理论研究有助于实时系统规范的描述,高质量实时系统的分析、设计、发展、实现和验证。程序理论的目的是通过研究程序及其规范来支持程序设计实践。程序理论的主要内容是解释程序语言各语法成分的语义。指称语义,操作语义和代数语义是三种常见的程序语义的表现形式。指称方法用数学论域中的对象来指称程序语言的记号和公式;操作方法通过描述抽象数学机上的一系列执行步来表示程序是如何被执行的;代数方法相比前两者更加抽象,它不直接告诉程序的含义,而是通过代数等式(不等式)来刻画程序的性质。程序语义的不同表现形式具有各自不同的优势,能从不同的角度研究程序语言的语义以及理解各表现形式的关系,是体现程序理论价值和成熟度的重要指标。本文首先提出了一种基于事件的同步信号语言,可用于嵌入式实时系统的描述和编程实现。进而在程序统一理论的指导下,将信号演算分解成包含不同特征的信号演算子集族,然后以代数方法为基石,研究各信号演算子集的代数语义模型和规范型,同时从代数方法出发,发展与之等价的指称语义模型,揭示了代数语义和指称语义的等价关系,展示代数方法在程序统一理论中的重要性,也为实时系统程序语言理论和信号演算的语义理论做出一些贡献。本文的主要内容包括:·提出了一种基于事件的同步信号语言,它遵循著名的同步性假设和有限可变性假设。该语言涵盖实时系统规范语言的诸多特征,譬如:反应的瞬时和延时、反应的有限和无限、反应的中止和发散、组合的顺序和并发等。为了降低信号演算语义理论的复杂度和难度,信号演算语言被分解成包括不同特征的信号演算子集族。·分别研究了各信号演算子集的代数语义模型和指称语义模型,在代数模型中,我们首先以公理化的方法定义了基本原子反应和组合算子的语义,然后讨论了相应的代数规范型,任意一个反应都可以通过给出的代数定律转化为规范型形式。在指称语义模型中,我们分别构建了不同反应类型的指称论域,如:瞬时反应的指称物是健康的事件输入-输出函数,延时反应可以用正则的执行树类来描述。·讨论了代数语义和指称语义的语义联接问题。我们证明了这两种语义在本质上是等价的,即两个反应代数语义相等当且仅当它们的指称语义相等,一方面,我们证明了所有的代数定律都可以在指称语义的框架下得以证明,这体现了代数语义的合理性。另一方面,由于指称语义相同的规范型反应具有相同的规范型,而每一个反应都可以根据代数规则转化为规范型形式,因此指称语义相等的反应具有相同的规范型,从而是代数等价的,这体现了代数语义相对于指称语义的完备性。