| 题名 | 交互系统及其基于XYZ／E的规范与逐步求精 |
| 作者 | 郑小立 |
| 学位类别 | 博士 |
| 答辩日期 | 1998 |
| 授予单位 | 中国科学院软件研究所 |
| 授予地点 | 中国科学院软件研究所 |
| 关键词 | 交互 算法 输入 输出 状态转换 交互对象 交互程序设计语言Li 开放系统 封闭系统 时间 人机交互 时序逻辑 不变式 XYZ系统 规范 验证 逐步求精 |
| 学位专业 | 计算机软件 |
| 中文摘要 | 算法对外部世界是封闭的，初始状态和内部状态转换机制决定其运行过程和结果。而交互系统则对外部世界开放，它在运行过程中，从外部世界获取并向外部世界输出信息，外界的输入将影响其行为和结果。交互系统由于其与外界的交互行为而具有比算法更为丰富的行为和更强的能力。长期以来，人们研究的注意力更多地集中在系统的算法行为上，而对其交互特性则关注极少。至于对交互系统行为的形式化研究则更是少之又少。但是，我们所使用的计算机和软件系统多是交互系统。对交互系统及其形式化加以研究十分必要。本文共分三章。第一章首先介绍了交互系统相关的概念，并总结说明了交互系统的特点。随后，我们指出，算法或图灵机已不能够完全描述交互系统的行为，交互程序的表达能力超越了图灵机。接着，我们讨论了开放系统与封闭系统，并行、分布与交互的区别和关系。最后，讨论了三种最常见的交互对象：时间、人和程序。阐述了它们的特性和相互的区别。在第二章中，首先简单介绍了线性时间时序逻辑。然后开创性地提出了交互系统的一个基于时序逻辑的形式化计算模型ICS。并在此模型中，讨论了系统性质的形式化规范以及不变式性质的验证规则。在第三章中，我们详细讨论了交互系统在XYZ／E中的程序规范和逐步求精。首先介绍了XYZ系统。然后讨论了如何在XYZ／E中给出交互系统的程序规范并通过逐步求精得到可执行的程序。最后，用一个具体的例子－五子棋程序来说明基于XYZ／E的交互程序规范和逐步求精的方法。本文的主要贡献在于：△ 总结并详细说明了交互程序的特性及其与算法程序的关系。△ 提出抽象的交互程序设计语言Li，并通过Li、程序设计语言L以及带有神喻的程序设计语言La说明交互程序的表达能力超越了图灵机。△ 阐述了常见的三种交互对象（时间，人，程序）的特性和它们之间的关系和区别。△ 提出了交互系统的一个基于时序逻辑的形式化计算模型ICS。并在此模型中，讨论了系统性质的抽象描述和验证规则。△ 阐述了交互程序基于XYZ／E的形式规范，提出了对交互行为，交互过程性质和交互对系统的影响等进行抽象描述的方法，并建立了构造交互程序规范的框架。△ 对交互程序进行逐步求精设计。逐步求精是由抽象规范到可执行程序的逐步精化的过程。逐步求精方法提高了软件的可靠性和生产率。 |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 51 |
| 内容类型 | 学位论文 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/6932]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 郑小立. 交互系统及其基于XYZ／E的规范与逐步求精[D]. 中国科学院软件研究所. 中国科学院软件研究所. 1998. |
| 个性服务 |
| 查看访问统计 |
| 相关权益政策 |
| 暂无数据 |
| 收藏/分享 |
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论