中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
交互系统及其基于XYZ/E的规范与逐步求精
作者: 郑小立
答辩日期: 1998
专业: 计算机软件
授予单位: 中国科学院软件研究所
授予地点: 中国科学院软件研究所
学位: 博士
关键词: 交互 ; 算法 ; 输入 ; 输出 ; 状态转换 ; 交互对象 ; 交互程序设计语言Li ; 开放系统 ; 封闭系统 ; 时间 ; 人机交互 ; 时序逻辑 ; 不变式 ; XYZ系统 ; 规范 ; 验证 ; 逐步求精
摘要: 算法对外部世界是封闭的,初始状态和内部状态转换机制决定其运行过程和结果。而交互系统则对外部世界开放,它在运行过程中,从外部世界获取并向外部世界输出信息,外界的输入将影响其行为和结果。交互系统由于其与外界的交互行为而具有比算法更为丰富的行为和更强的能力。长期以来,人们研究的注意力更多地集中在系统的算法行为上,而对其交互特性则关注极少。至于对交互系统行为的形式化研究则更是少之又少。但是,我们所使用的计算机和软件系统多是交互系统。对交互系统及其形式化加以研究十分必要。本文共分三章。第一章首先介绍了交互系统相关的概念,并总结说明了交互系统的特点。随后,我们指出,算法或图灵机已不能够完全描述交互系统的行为,交互程序的表达能力超越了图灵机。接着,我们讨论了开放系统与封闭系统,并行、分布与交互的区别和关系。最后,讨论了三种最常见的交互对象:时间、人和程序。阐述了它们的特性和相互的区别。在第二章中,首先简单介绍了线性时间时序逻辑。然后开创性地提出了交互系统的一个基于时序逻辑的形式化计算模型ICS。并在此模型中,讨论了系统性质的形式化规范以及不变式性质的验证规则。在第三章中,我们详细讨论了交互系统在XYZ/E中的程序规范和逐步求精。首先介绍了XYZ系统。然后讨论了如何在XYZ/E中给出交互系统的程序规范并通过逐步求精得到可执行的程序。最后,用一个具体的例子-五子棋程序来说明基于XYZ/E的交互程序规范和逐步求精的方法。本文的主要贡献在于:△ 总结并详细说明了交互程序的特性及其与算法程序的关系。△ 提出抽象的交互程序设计语言Li,并通过Li、程序设计语言L以及带有神喻的程序设计语言La说明交互程序的表达能力超越了图灵机。△ 阐述了常见的三种交互对象(时间,人,程序)的特性和它们之间的关系和区别。△ 提出了交互系统的一个基于时序逻辑的形式化计算模型ICS。并在此模型中,讨论了系统性质的抽象描述和验证规则。△ 阐述了交互程序基于XYZ/E的形式规范,提出了对交互行为,交互过程性质和交互对系统的影响等进行抽象描述的方法,并建立了构造交互程序规范的框架。△ 对交互程序进行逐步求精设计。逐步求精是由抽象规范到可执行程序的逐步精化的过程。逐步求精方法提高了软件的可靠性和生产率。
英文摘要: Algorithm is closed to external world. Its behavior and result are decided by the initial input and internal mechanism of state transition. Interactive system is open to external world. It input and output information with external world. The input will influence the behavior of the system. Because of the interaction with external world, interactive systems have richer expressiveness than algorithms. People always focus their research on the algorithmic behavior of systems and seldom pay attention to the interactive properties of systems. Nowadays little formal research is done on interactive systems. But most of the empirical computer and software systems we use are interactive systems, so it deserves further research. This paper includes three chapters. In the first chapter, we introduced some concepts and characteristics of interactive systems. Then, we point out that algorithms or Turing machines can't model the behavior of interactive programs which have richer expressiveness than Turing machine. And then we discussed the relation and difference between open systems and closed systems, among parallelism (concurrency), distribution and interaction. At last, we discussed three kinds of interaction adversary: time, human and programs. In the second chapter, the linear time temporal logic(LTTL) is introduced. We originally put forward a formal computation model ICS(Interactive Computation System) of interactive systems based on temporal logic. And discussed abstract specification and verification of system properties in this model. In chapter 3, we discussed the specification and stepwise refinement of interactive programs using XYZ/E language. First we introduced XYZ system, and then discussed the mechanism and methods of constructing specification and stepwise refinement of interactive programs with a specific example-Wu Zi Qi program. The original contributions of this paper are: △ Summarize and explain the characteristics of interactive programs and its relation with algorithm programs. △ Put forward an abstract interactive programming language Li. And use Li the programming language L and the programming language with oracle La to explain that interactive programs are powerful than algorithms. △ Explain the characteristics of three kinds of interaction adversary(time, human and programs) and the relation and difference among them. △ Put forward a formal computation model ICS of interactive systems based on temporal logic. Discuss the abstract specification and verification of system properties in this model. △ Formal specification of interactive systems based on XYZ/E. Mechanism and methods to abstractly specify the interactive behavior, interaction properties and affect of interaction on system. A framework to construct specifications for interactive programs. △ Stepwise refinement of interactive systems. Stepwise refinement denotes the procedure from abstract specification to eventual executable program. Stepwise refinement design mechanism improves the reliability and productivity of software systems.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/6932
Appears in Collections:中科院软件所

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

Recommended Citation:
郑小立. 交互系统及其基于XYZ/E的规范与逐步求精[D]. 中国科学院软件研究所. 中国科学院软件研究所. 1998-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