论文部分内容阅读
随着人们对软件系统的要求不断地提高，形式化技术得到了充分的发展。过去人们依赖于优秀的软件工程师来对软件系统可靠性和安全性提供保证，而如今，人们可以使用已有的形式化技术，按照一定的步骤逐步来开发出满足市场高要求的软件系统。 然而，目前的形式化技术还比较单一，它们只能满足开发人员对软件系统设计的某些方面，因此，这种满足有一定局限性和限制。随着研究人员对这些形式化技术的研究的深入，人们逐渐发现了这些技术和方法本身存在着固有的缺陷。于是，人们开始对形式化方法的集成这一研究思路的探讨，已有的集成的例子，如CSP和B方法进行的集成，CSP和Z语言进行的集成。 本文研究的对象的基础有两个，分别是时间Petri网(TPN)和B方法。TPN是一种图形化的形式化技术，它主要应用于实时系统，分布式系统或者并发系统，它建立在普通的Petri网基础之上，并加以时间约束，和普通Petri网一样，它缺乏数据建模能力和函数定义能力。B方法是一种形式化方法，它包含了自己的形式规格说明语言和验证系统，它适合描述一些顺序系统，但是它也有缺点，它不适合描述实时系统和并发系统。鉴于以上两种方法各自的缺陷，我们考虑将TPN和B方法结合在一起，用B方法作为TPN底层的形式化模型，这一点和众多高级Petri网有非常多的相似之出。将B方法作为底层模型之后，将B方法中的某些元素替换原有TPN中的概念，从而建立TPN和B方法之间映射关系。这种关系是静态的，我们还需要定义TB网的动态映射，描述TB网的动态性质。TB网是一种高级的Petri网，需要搞清楚这种网的构造方法，它的可达图的构造，它的活性的定义，本文对于这些问题都进行了探讨。另外，由于TB网是一种集成的形式化方法，它应该能够描述实时系统，我们需要指出如何能够证明构造出来的系统能够满足时间约束。 TB网是一种集成的形式化方法，它能够使用的领域应该包括了TPN和B方法各自使用的领域，这是因为在集成的过程中，我们使用B方法来解决TPN不能够描述数据类型和定义函数，同时，使用TPN来解决B方法不能够描述实时系统，不能够描述那些Time-Critical的系统，所以，我们有理由认为TB网是一个使用更广泛的形式化方法。