Z语言的实时扩展及应用

摘要

实时软件系统在现代工业和社会生活中扮演着越来越重要的角色,随着需求的逐步增加,实时系统的软件开发方法学渐渐成为研究的热点问题.形式化方法在实时系统的开发过程中的使用也越来越多,Z语言是一种广泛应用的形式化规格说明语言,然而,它并不是为处理系统的动态行为而设计的,因此对Z进行扩充以适应实时应用的需要是非常重要的.在该文,我们归纳了Z实时扩展,提出了分类标准,一类是被称为集成的扩展方法,它基于形式化说明语言Z和其它形式化方法的集成,在这里由其它形式化方法提供表示动态行为的结构;另一类称之为非集成的扩展方法则只使用Z的语义,而由其它形式化方法对时间约束性和并发进行的描述则被转换成Z规格说明,完成了上述分析之后实际就给出了一个对Z进行实时扩展的通用方法.一种被称为RT-Z的基于规格描述语言Z和timed CSP的实时扩展是集成扩展方法的典型代表,RT-Z将Z和timed CSP的功能用一个紧密的框架结合起来,实际上无论是Z还是timed CSP都缺乏对结构化的支持机制,为了能适应系统复杂性的需要,RT-Z另外引入了对结构化的支持机制.RT-Z的语义基于Z和timed CSP,这是它具有正确性和数学严格性的基础.RT-Z可以用于需求描述,也可以用于设计阶段,非常适合于实时系统的开发.另一方面,使用过程描述语言可以方便的描述时序关系,在该文中,我们也讨论了这种非集成的扩展方式,它能够利用时序状态转换系统将过程描述语言转换为Z规格.通常,实时系统开发依赖于时间约束性和复杂的外部因素,因此无论是采用Z和timed CSP集成还是使用规格描述语言转换的非集成方法都不能很好地解决系统设计的所有问题,因此在实时系统设计中选择合适的方法是非常重要的.经过进一步研究,我们在微机仿真系统的设计过程中提取了通用的设计模式,这个模式基于多视点的软件工程方法,采用集成方法从功能视点得到的规格说明和采用非集成方法从控制视点得到的规格说明在一个统一的语义下结合起来,这样就可以利用两种规格说明方法直接得到在语法和机制上一致的规格说明,因此可以避免单独使用两种方案所产生的缺陷.

目录

文摘

英文文摘

第一章绪论

第二章实时系统

2.1实时系统的基本概况

2.1.1实时系统的概念

2.1.2强实时系统和弱实时系统

2.1.3实时系统的外在约束

2.1.4实时操作系统

2.2实时系统的基本特征

2.2.1时间约束性

2.2.2并发性

2.2.3可预测性

2.2.4正确性

2.2.5健壮性

2.3实时系统的分类

2.3.1周期性事件类型

2.3.2不规则时间类型

2.3.3有边界事件类型

2.3.4突发事件类型

2.3.5无边界事件类型

2.4实时系统的开发技术

2.4.1实时系统的分析技术

2.4.2实时系统的设计和实现技术

2.5实时软件工程概述

2.5.1需求获取阶段

2.5.2分析阶段

2.5.3设计阶段

2.5.4测试阶段

2.6实时系统的并发设计问题

2.6.1实时系统的并发

2.6.2面向对象的并发模型

第三章形式化方法

3.1形式化方法概述

3.1.1形式化方法的基本概念

3.1.2形式化方法的优点

3.1.3形式化方法的分类

3.1.4形式化方法的使用：

3.1.5形式化方法的发展

3.1.6对形式化方法的进一步认识

3.2形式化方法研究的主要内容

3.2.1形式规约

3.2.2形式验证

3.3结构化方法、面向对象方法和形式化方法的比较

3.3.1建立模型的可读性

3.3.2应用范围的比较

3.3.3正确性比较

3.3.4软件运行效率

第四章形式化方法与实时系统

4.1形式方法在实时系统开发中的作用

4.1.1形式化规约的作用

4.1.2定量证明的作用

4.1.3形式验证的作用

4.2形式化方法在实时系统开发中的优点和不足：

4.2.1形式化方法的优点：

4.2.2形式化方法在实时系统开发中的不足之处

4.3形式化方法在实时系统开发中的发展方向

第五章Z语言及其实时扩展

5.1 Z语言

5.1.1 Z模式

5.1.2 Z语言中的基本符号说明

5.1.3 Z规格说明的构造方法

5.1.4 Z语言的求精

5.2 Z语言实时扩展

5.2.1 Z语言实时扩展的分类

5.2.2非集成的Z语言实时扩展

5.2.3集成的实时扩展语言RT-Z

5.2.4实时扩展的比较

第六章形式化方法在微机仿真系统中的应用

6.1微机仿真系统的设计思路

6.1.1基本设计方案

6.1.2在仿真系统的设计中需要解决的主要问题

6.1.3微机仿真系统设计中的形式化方法

6.2实时Z在微机仿真系统设计中应用模式的研究

6.2.1应用特点的分析

6.2.2应用模式的提取

6.3面向功能视点的规格说明应用

6.3.1抽象说明

6.3.2具体说明

6.4面向控制视点的规格说明

6.4.1根据控制信号和指令提取状态集

6.4.2数据类型定义

6.4.3 8259A的状态模式：

6.4.4确定操作的时序关系关系

结论

攻读学位期间发表的论文

参考文献：

独创性声明

致谢