Study On Program Real-time Model Checking Method Based On WCET Analysis Technology

Correctness of the system not only depends on the output in real time in the logical correctness and requires real-time system within the stipulated time frame to implement its functionality. Real time systems have a very high real-time requirements, In order to ensure real time, we tend to use formal methods to model systems for accurate. Traditional model checking method is to proceed from the model describes the system verify the nature of the system, such as security, activity, the reliability, Real time constraints in the model usually comes from the requirements specification, Regardless of system implementation.But the system is ultimately a matter for program implementation, From demand constraints cannot accurately describe the system in real time the actual execution time. Traditional model checking method for real time systems can only verify the abstract model meets real-time nature cannot verify that the corresponding program meets the real-time nature of the system in real time, and on the factors taken into account the impact of deficiencies in the software implementation, Study on model test method validation in real time real time nature of the program is very necessary. This article studies the procedures and models for real-time systems, the establishment of model checking method based on program timing analysis to interrupt as a typical research on interference factors of the effect of different types of interrupts on real-time, provides support for the study of software reliability in real time.The thesis consists of these four aspects:1. Make real time constraints and program execution path mapping of a set of methods.For realtime Systems Division of the execution path of the source program, the source program is divided into basic blocks, using directed graph based on adjacency list storage structure describes the basic block between basic blocks and control process, traversed to find effective implementation path. Through real-time constraints in timed automata model for real-time systems analysis, find out the real time constraint mapping path set, depending on where the corresponding path set node Mapper information generated fragments, research in real time constraints in the program's implementation process.2. Establishment of model checking method based on WCET analysis.Program fragments in real-time constraints on mapping process after the worst case execution time (Worst-Case Execution Time, WCET) analysis, find out the maximum execution time of program fragments, WCET estimates obtained using real time constraints in the correction system model, further amended with real-time system verification tool UPPAAL authentication model satisfies the real-time nature of the system.3. Established a typical interrupt of WCET analysis methods.Based on real-time system characteristics of the WCET analysis for interrupt will break as part of the system and study on effect of disruption on real-time, further binding instance completes interruptions based model checking methods.4. Designed and realized procedures based on WCET analysis real-time model checking methods of prototyping tool WCETModel, realized the paper proposed method, Preliminary establishment of a unified set of methods and tools set, credible research provides support for real-time systems.