论文部分内容阅读
实时软件系统在现代工业和社会生活中扮演着越来越重要的角色，随着需求的逐步增加，实时系统的软件开发方法学渐渐成为研究的热点问题。形式化方法在实时系统的开发过程中的使用也越来越多，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集成还是使用规格描述语言转换的非集成方法都不能很好地解决系统设计的所有问题，因此在实时系统设计中选择合适的方法是非常重要的。经过进一步研究，我们在微机仿真系统的设计过程中提取了通用的设计模式，这个模式基于多视点的软件工程方法，采用集成方法从功能视点得到的规格说明和采用非集成方法从控制视点得到的规格说明在一个统一的语义下结合起来，这样就可以利用两种规格说明方法直接得到在语法和机制上一致的规格说明，因此可以避免单独使用两种方案所产生的缺陷。