XYZ系统在多媒体领域的应用研究

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.
页数	92
语种	中文
内容类型	学位论文
URI标识	http://ir.iscas.ac.cn/handle/311060/7030
专题	中科院软件所_中科院软件所
推荐引用方式 GB/T 7714	赵琛. XYZ系统在多媒体领域的应用研究[D]. 中国科学院软件研究所. 中国科学院软件研究所,2000.

条目包含的文件
文件名称/大小	文献类型	版本类型	开放类型	使用许可
LW002976.pdf（2149KB）			限制开放	--	请求全文