Design And Achievement Of A Tool Of Modeling, Simulation And Verification Of Context Aware System Based On UPPAAL

Extensive use of context-aware systems reflects the growing market demand and its huge economic potential.Context-aware systems are usually large, complex, heterogeneous systems.Development of such a system involves the design and development of software, hardware and network implementation. To design and implement a complete, safe and strong context-aware system, the workload would be enormous and complex.This makes the use of software engineering principles of design and development be particularly important. As the diversity of device types, context interpretation and adaptation requirements, context-aware systems are always heterogeneous and dynamic systems.This makes the complexity of design and development of context-aware systems. Therefore, to build a well-designed, strong safety and security context-aware system, the usage of formal methods for system modeling, simulation and verification is extremely necessary. However, there is still no formal and convenient tool specifically for modeling, simulation context-aware systems, and verification of important properties of context-aware systems.UPPAAL is a formal real-time system modeling, simulation and verification tools. The application of UPPAAL in aspect of real-time systems, such as analysis of communication protocols, operation of train systems, has shown particular advantages. If make some extends of UPPAAL to apply this toolkit in context-aware systems scale, then use UPPAAL to model, dymaticly simulate context-aware systems, and formally verify some important properties of context-aware systems, such as reacheablity, safety and liveness.This approach would preciously add real-time constraints to context-aware systems and considerably improve the efficiency of the design of context-aware system.All researchment of this paper is expended below background of design and verification of context-aware systems. The research goal is to be on the expansion direction of context-aware, so that UPPAAL can serve context-aware systems. It is necessary to provide a clear and convenient method and a tool of formal modeling, simulation and verification of context-aware systems.To achieve this research purpose, firstly it is necessary to analysis and abstract the existing context-aware application system applications, research and design architecture approach of modeling context-aware systems. Secondly, make more in-depth study of UPPAAL, use the features of UPPAAL, expanding the application of UPPAAL syntax, and progressively realize the process of modeling of context-aware systems in UPPAAL.This includes construction of context structures and context sensitive situations, performance of the context information, context reasoning algorithms, context-aware system adaptation methods, context-aware system function modules and communication modules, data storage system design and implementation of context-aware systems. Meanwhile, this paper will be based on UPPAAL in a special direction for the context-aware design, make detailed analysis of content of source file of UPPAAL, design and develop an expansion tool of UPPAAL to achieve a clear and quick method to construct context-aware system source files of UPPAAL. Finally, according to this method of modeling, simulation and verification of context-aware systems proposed in this paper, we make a detailed modeling, simulation of a context-aware system example in the expending tool and UPPAAL.We also verify some important properties such as, reachablity, safety and liveness of this example in UPPAAL.This illustrates the clarity and convenience of this method and toolkit.