Comparison And Checking Between Requrement Models And Programs For Behavioral Consistency

In software development process, requirements and programs are two different forms of software, and people aim to transform the requirements to programs. Under the current technology circumstance, capability of worker is still the primary factor of the software quality in this transformation process. Although automated tools have been wildly used, such as requirement modeling and model checking, model transformation, automated testing, and automated program synthesis in minor areas, hand coding is still the primary method the software development stage of most areas. Who makes sure the consistency between the requirements and the software becomes a key problem in development.Furthermore, in many projects, people have spent many resources in building correct requirement models, which were only used as subjective references in software testing, or even useless, leading the costs of requirement models being wasted. Nowadays, the primary method of checking the accordance between requirement and software is to test the programs carefully and adequately, while several factors may compromise the effects of testing, e.g. the potential differences in human comprehension on requirements, the coverage problem of testing, and the evolution of the test cases after the mutation of the requirements and programs.For these problems, this article proposes a new method, which automatically checks the programs and existing requirement models comparatively, and finds the differences to guide people to find potential problems. This method includes following three aspects of works.1. The model of Parallel State Machine is extended from Labeled Transition System, and is defined mathematically. This model can be conveniently converted from requirements and program sources. With extensions of abstract parallel descriptions on Labeled Transition System, the Parallel State Machine has strong expressivity for model description and simple structure for the convenience of algorithm description.2. The complete method of extracting Parallel State Machine is proposed, which includes three techniques. The first is the alias analysis based on field propagation, which solves the function pointers in indirect calls to construct complete flow graphs. The second is the data flow analysis with data relations between requirement models and program models, with which users can obtain complete data relations by setting few data relations manually. The last technique is the parallel recognition, which converts the program from imperative flow charts to Parallel State Machine models.3. The theories of model comparison checking are carefully studied, and the checking method is proposed. The theories provide foundations of correctness of the algorithm. With this method, an automated tool called Model-Program Comparison Analyzer is built, which compares the requirement models and program sources, positions the differences and assists users for problem analysis.Furthermore, the migration of model comparison checking method to other models is also studied theoretically, which provides guides for building automated checking tools on other models.