【摘要】 形式化的软件开发方法是建立在严格数学基础上的,其目标是通过严格的分析、验证发现软件设计及开发过程中的模糊性和不完备性,以达到对软件质量的有效控制。Petri网是形式化软件开发的一种很好的描述工具,它在描述异步并发的环境、模型验证等方面有着独到之处;图灵机是迄今为止计算能力最强的计算模型,在理论层面上有着其他模型不可替代的重要作用,它深刻地刻画了物理世界的可识别与可判定2个重要的概念。文章给出了这2种计算模型的一些基本概念、结论以及解决问题的主要方法。最后,用交通管理系统为例说明形式化方法的运用。更多还原

【Abstract】 Formal software development method is a kind of mathematically-based technique.It can achieve effective control for the software quality through rigorous analysis,verification to find the ambiguity and incompleteness of software design and development process.Petri net is one of good description tools to meet formal software development,which has obvious advantages in the description of asynchronous concurrent environment and model verification.Turing machine is a calculation model with the best computing abilities so far,which enjoys an irreplaceable role at theoretical level.It depicts deeply the two important concepts of identifiableness and decidability in the physical world.In this paper,some basic concepts,the main methodology to solve the problem for the two kinds of computational models and conclusions are presented.Furthermore,an example of traffic management system is listed to explain how to use the formal methods.更多还原