随着计算机软件的飞速发展,提高软件开发的效率已成为一个非常重要的问题。采用软件形式化技术,不仅可以极大地减少软件设计早期阶段的错误,缩短开发的总体时间,而且有利于开发人员之间的沟通,提高软件的可靠性。形式化方法是建立在严格数学基础上,通过严格的分析、验证发现软件设计及开发过程中的模糊性和不完备性,以达到对软件质量、开发成本及开发进度的有效控制。形式化方法分为形式化规格说明和形式化验证。Petri网是满足上述两个要求的很好的描述工具。Petri网是一种对系统软件形式化、图形化的描述和分析工具,具有直观、易懂和易用的优点。对于具有并发、异步、分布、并行、不确定性和随机性的系统,都可以利用这种工具构建模型。然后对模型进行分析,即可得到有关系统静态结构和动态行为方面的信息。根据这些信息可以对要开发的系统进行评价和改进。同时,Petri网为程序员与其他人员之间的沟通和交流提供了一个强有力的一个平台环境,使得软件开发的过程形式化。本文讨论的是基于Petri网的形式化软件开发方法。主要从模拟与验证两方面展开。利用不变技术、结构分析技术、分块建模技术等,对Petri网的模拟能力以及主要行为特征进行较深入细致的研究,得到了一些新的结果。本文的主要贡献有:(1)数据库系统的并发控制一直都受到业内人士的广泛关注,它是衡量一个DBMS性能的重要指标之一。而S-不变作为Petri网的一个重要的验证方法同样也越来越受到人们的关注。经典的S-不变方法往往只用来对系统性质的一种解释和判定,或是对一些具体的范例的性质的一种定性、定量分析。本文使用增广Petri网构建一个比较通用的带封锁机制的DBMS模型,给出了形式化软件开发的一个范例。从整体上模拟了一个DBMS,并用S不变对模型进行验证。(2)目前,大多数的软件系统都是并发系统。Petri作为一个很好的形式化描述和分析工具,必须要能很好的描述和分析这类系统。路灯故障检测系统就是一个典型的并发系统,系统信号在路灯故障检测系统与路灯设备以及传输线路之间是并行传输的。本文使用带禁止/容许弧的自控网构建了一类路灯故障检测系统,采用Petri网形式化方法对系统进行描述、分析和证明,确保了系统的正确性。(3)交通信号控制是一个世界性的话题,它是一类典型的并发、同步系统。本文构建了一类具有中断处理功能且便于实现区域控制的交通信号控制系统。建模过程中采用分块建模的方法也正好符合了软件设计的模块化准则和面向对象的设计思维。并且从网所定义的变迁发生序列的结构入手,对模型进行了正确性分析。