中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
高阶时段演算及其应用
作者: 詹乃军
答辩日期: 2000
专业: 计算机软件与理论
授予单位: 中国科学院软件研究所
授予地点: 中国科学院软件研究所
学位: 博士
关键词: 时段演算 ; 高阶逻辑 ; 实时系统 ; 超稠密计算 ; 完备性
摘要: 时段演算是区间时序逻辑的一个扩充,是由周巢尘,C.A.R. Hoare 和 A.P. Ravn 提出的。时段演算可以用来描述计算系统的实时需求, 并可以用来验证计算系统的实时性质。在这方面人们已经做了大量工作,证明它是非常成功的。期限驱动调度算法是 Liu 和 Layland 提出的一种动态调度策略。它假设若干任务周期性地向同一处理器请求执行时间,算法根据每个任务当前请求的的期限动态地分配优先级,当前请求较急的任务将获得较高优先极,否则将获得低优先级。在任意时刻,只有优先级最高且请求尚未完成的任务才能占有处理器。作为时段演算的一个应用,我们将用时段演算来形式描述这个算法,并证明 Liu 和 Layland 给出的关于该算法能行的充要条件。本文的主要工作是研究如何用时段演算来刻画程序的实时行为。为了处理局部变量的声明,我们必须引进关于变量和量词。而在实时程序设计里,所有程序变量均看成时间域上的函数,因此,建立高阶时段演算是必要的。本文建立了高阶时段演算理论,包括它的语法,语义和证明系统。在假设所有程序变量均有穷可变的条件下,我们证明它在抽象时间域上是完备的。我们也将用高阶时段演算去验证一些程序的实时性质。例如,我们将说明在高阶时段演算里可以定义超稠密切害算子;我们将给出局部变量声明的形式描述;我们将证明程序复合操作“;”具有单位元且满足结合律,以及可以将程序的实时语义分解成两部分:实时部分和非实时部分,从而可以将程序的实时语义看成是它的与时间无关语义的保守扩充。
英文摘要: Duration Calculus (DC) is an extension of interval temproal logic which is proposed by Zhou Chaochen, C.A.R. Hoare and A.P. Ravn, and can specify the real-time requirements of computing systems and prove their real-time properties. DC has been proved to be a powerful logical frame by lots of case studies of it. DDS (stands for Deadline Driven Scheduler) is about scheduling multiple tasks on a single processor dynamically which is proposed by Liu and Layland. It assumes that all tasks raise periodic requests for processor time, and priorities are dynamically assigned to tasks according to the deadlines of their current requests. A task will be assigned the highest priority if the deadline of its current request is the nearest, and will be assigned the lowest priority if the its current request is the furthest. As any instant, the task with the highest priority and yet unfulfilled request will occupy the processor. As an application, we will formally descripe DDS and prove the sufficient and necessary condition about DDS given by Liu and Layland in terms of DC. The main results of this paper coven how to describe the real-time behaviours of programs in terms of duration calculus. In order to deal with hiding, e.g. local variable declaration and so on, quantifications over program variables are inevitable. So a higher-order duration calculus is established in this paper including its syntax, semantics and proof system. Its completeness on abstract domains will be proved under the assumption that all program variables have finite variability. We will explain how to apply the higher-order duration calculus to define semantics for real-time programs.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/6118
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
LW002983.pdf(1109KB)----限制开放-- 联系获取全文

Recommended Citation:
詹乃军. 高阶时段演算及其应用[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2000-01-01.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[詹乃军]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[詹乃军]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2017  中国科学院软件研究所 - Feedback
Powered by CSpace