Procedures Modeling For Testing And Model Checking Needs

Software testing and model checking are two reliable software quality assurance techniques, the former is statute of the whole state space software testing, which is part of the output detection software operating results consistency. However, due to model checking prone state space explosion problem, the lack of completeness and software testing, so the combination of the two technologies is an inevitable trend. Therefore, we propose a model to support software testing and inspection requirements of procedural modeling technology, which includes physical storage model, visualization model and algebraic models, three models constructed a model system. Using the ideas of program flow diagram of the establishment of the physical storage model and verify the correctness of the visual model by establishing rigorous mathematical model based on algebra.Program algebraic model is based on the application and extension of the service-oriented architecture SOA (Service Oriented Architecture) formal and credible property on the basis of the modeling study. Generate physical storage model is based on the idea program flow diagram describing the program structure, with Web Services Description Language WSDL (Web Services Description Language) describes the relevant information of program flow graph nodes; flow control information of flow diagram is described by BPEL (Business Process Execution Language) language business process program. Because BPEL translation into LOTOS have related research and better application, so this application uses WSDL/BPEL specification to describe the system under test, and introduced the theory of physical storage model and algorithm in the text, subsequent model has laid a good foundation for checking LOTOS modeling convection diagram. Visualization model that is the program flow diagram, physical storage model to facilitate subsequent processing model, but not intuitive, so the physical storage model using open source graph visualization software Graphviz equivalently transformed into symbols of graphical representation.Program model system provides basic information available paths model for subsequent testing work, inhibiting the model checking state space explosion problem to some extent. While for subsequent abstract TTCN-3test suites generated automatically provides the basic path, data type and other information. The paper was developed based on the algorithm proposed program modeling tools, combined with examples demonstrate the feasibility of the tool. The program model for the eventual integration of modeling and automatic detection and efficiency of the foundation.