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.