中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
XYZ系统在多媒体领域的应用研究
作者: 赵琛
答辩日期: 2000
专业: 计算机软件与理论
授予单位: 中国科学院软件研究所
授予地点: 中国科学院软件研究所
学位: 博士
关键词: 多媒体系统 ; XYZ系统 ; 时序描述 ; 逐步求精 ; 自动转换 ; 基于描述的测试 ; 形式化方法
摘要: 本文主要研究XYZ系统在多媒体领域的应用问题。XYZ系统是一个以增强软件可靠性和提高软件生产率为目的的程序开发支撑系统,它由时序逻辑语言(TLL:Temporal Logic Language)XYZ/E和以该语言为基础的一组软件工程工具组成。为了在多媒体领域中应用逐步求精、程序自动生成和面向形式规范的并发系统测试等形式化技术,本文首先研究一个表达能力足够的Allen区间代数(Interval Algebra)的子集合,以它作为多媒体对象时序关系的描述语言。其次,本文研究基于该描述语言的基本求精规则。对这些规则作严格的正确性证明之后,在利用这些规则进行逐步求精过程中,无需再进行语义一致性检查,从而简化了求精过程,便于多媒体领域的工程师接受逐步求精方法。接着,本文研究了从时序描述到XYZ/RE表示的可执行同步器的自动转换,XYZ/RE 是时序逻辑语言族XYZ/E中表示实时系统的子语言。最后,本文对一类特殊的时序描述分别给出自动生成事件序列前后约束(CSPE:Constraints on Succeeding and Preceding Events)和时间自动机(Timed Autoamta)的方法,依据生成的结果,一方面可以应用CSPE的测试理论和工具进行同步器的同步测试;另一方面根据时间自动机,进行非确定性测试,可以较容易地判断运行结果正确与否,在进行确定性测试时,可以辅助自动生成测试用例。
英文摘要: In this thesis we mainly study how to apply XYZ System to the multimedia field. XYZ System is a programming support system with the goal to enhance reliability and productivity of software development. It consists of a Temporal Logic Language (TLL) XYZ/E to serve as its kernel and a suite of software engineering tools. In order to introduce the formal techniques such as stepwise refinement, automatic transformation and testing based on formal specification to the multimedia field, we first present a powerful subset of Allen's interval algebra as the temporal specification language to multimedia program. The we find some basic refinement rules oriented to the temporal specification language. After the correctness of these rules has been proved, in the stepwise refinement procedure the semantic consistency need not be considered so that the engineers in multimedia field easily accept this formal method. Thirdly we study the automatic transformation from the temporal specification to synchronizer in XYZ/RE which is a sub-language representing real time system in XYZ/E. Finally, two methods generating CSPE(Constraints on Succeeding and Preceding Events) constraints and timed automata from temporal specification are presented respectively. Based on these results, on one hand, we can test synchronizer by using CSPE-based methodology and tools directly. On the other hand, we can select timed test sequences from timed automata when considering the deterministic testing of synchronizer, and decide whether the running results are correct when considering the nondeterministic testing of synchronizer.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/7030
Appears in Collections:中科院软件所

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

Recommended Citation:
赵琛. XYZ系统在多媒体领域的应用研究[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