高阶时段演算及其应用
文献类型：学位论文
| 作者 | 詹乃军 |
| 学位类别 | 博士 |
| 答辩日期 | 2000 |
| 授予单位 | 中国科学院软件研究所 |
| 授予地点 | 中国科学院软件研究所 |
| 关键词 | 时段演算 高阶逻辑 实时系统 超稠密计算 完备性 |
| 学位专业 | 计算机软件与理论 |
| 中文摘要 | 时段演算是区间时序逻辑的一个扩充，是由周巢尘，C.A.R. Hoare 和 A.P. Ravn 提出的。时段演算可以用来描述计算系统的实时需求, 并可以用来验证计算系统的实时性质。在这方面人们已经做了大量工作，证明它是非常成功的。期限驱动调度算法是 Liu 和 Layland 提出的一种动态调度策略。它假设若干任务周期性地向同一处理器请求执行时间，算法根据每个任务当前请求的的期限动态地分配优先级，当前请求较急的任务将获得较高优先极，否则将获得低优先级。在任意时刻，只有优先级最高且请求尚未完成的任务才能占有处理器。作为时段演算的一个应用，我们将用时段演算来形式描述这个算法，并证明 Liu 和 Layland 给出的关于该算法能行的充要条件。本文的主要工作是研究如何用时段演算来刻画程序的实时行为。为了处理局部变量的声明，我们必须引进关于变量和量词。而在实时程序设计里，所有程序变量均看成时间域上的函数，因此，建立高阶时段演算是必要的。本文建立了高阶时段演算理论，包括它的语法，语义和证明系统。在假设所有程序变量均有穷可变的条件下，我们证明它在抽象时间域上是完备的。我们也将用高阶时段演算去验证一些程序的实时性质。例如，我们将说明在高阶时段演算里可以定义超稠密切害算子；我们将给出局部变量声明的形式描述；我们将证明程序复合操作“;”具有单位元且满足结合律，以及可以将程序的实时语义分解成两部分：实时部分和非实时部分，从而可以将程序的实时语义看成是它的与时间无关语义的保守扩充。 |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 97 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/6118]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 詹乃军. 高阶时段演算及其应用[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2000. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。