Research Into Localized Software Engineering And Practice With Z Notation

A series of software security events have caused the panic among the citizen in recent years. The citizen look forward to the theoretical breakthrough confronted with the state that software development is. So it is time to research and practice a new development method. If there is no formal description, then there is no standardized software industry.Z notation describes the system(software/hardware) "what to do" and not the "how to do" accurately. It describes associated computing operations through pre-conditions and post-conditions of state transition and their relations between input and output variables. As for Z specifications, it can be reasoned and verified within formal software.Formal reasoning infers the necessity of conditions for successfully execution of associated operations and verifies whether or not the objective conditions meet those pre-requisite conditions. Formal verification is an operation that checks the validity of variables in terms of set theory after the execution of operations. The operating mode can be converted into the principal disjunctive normal form via analyzing its preconditions and post-conditions. Assigning actual meanings to the mini-terms insides principal disjunctive normal forms does obtain the resulting test case suite.This paper applies the Z notation to each stage of the software life cycle in the localized literature firstly. It is an effective attempt to solve the problem of software using of formal z notation.