Institutional Repository
| XYZ系统在多媒体领域的应用研究 | |
| 赵琛 | |
| Major | 计算机软件与理论 |
| 2000 | |
| Degree Grantor | 中国科学院软件研究所 |
| Degree Level | 博士 |
| Place of Degree Grantor | 中国科学院软件研究所 |
| Keyword | 多媒体系统 Xyz系统 时序描述 逐步求精 自动转换 基于描述的测试 形式化方法 |
| English Abstract | 本文主要研究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的测试理论和工具进行同步器的同步测试；另一方面根据时间自动机，进行非确定性测试，可以较容易地判断运行结果正确与否，在进行确定性测试时，可以辅助自动生成测试用例。 |
| Abstract | 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. |
| Pages | 92 |
| Language | 中文 |
| Content Type | 学位论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/7030 |
| Collection | 中科院软件所_中科院软件所 |
| Recommended Citation GB/T 7714 | 赵琛. XYZ系统在多媒体领域的应用研究[D]. 中国科学院软件研究所. 中国科学院软件研究所,2000. |
| Files in This Item: | ||||||
| File Name/Size | DocType | Version | Access | License | ||
| LW002976.pdf（2149KB） | 限制开放 | -- | Application Full Text | |||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment