Adaptive software UML (unified modeling language) modeling and formal verification method

Abstract

The invention discloses an adaptive software UML (unified modeling language) modeling and formal verification method. The adaptive software UML modeling and formal verification method is mainly used for modeling and verifying adaptive software, and includes particular steps of (1), building concept models of the adaptive software; (2), extending UML to introduce novel stereotypes, tag values and constraint conditions into the UML, and building visual models of the adaptive software; (3), designing model transforming algorithms to transform behavior models of the adaptive software into timed automation networks and building formal models of the adaptive software; (4), giving TCTL (timed computation tree logic) temporal logic standards for describing properties of the adaptive software, verifying the reliability of the models of the adaptive software by the aid of model checking tools UPPAAL and further optimizing the UML models of the adaptive software according to feedback results. The visual models of the adaptive software comprise structural model adaptive class diagrams and behavior model adaptive sequence diagrams of the adaptive software. The adaptive software UML modeling and formal verification method has the advantages that the software adaptive modeling and verification complexity can be effectively lowered, and the software adaptive modeling efficiency and the reliability of the models can be improved.

Description

technical field [0001] The invention belongs to the technical field of new software methods and software modeling and verification, in particular to adaptive software UML modeling and a formal verification method thereof. Background technique [0002] Adaptive software / software adaptive technology is a new software design paradigm. This type of software can effectively reduce software maintenance pressure, enhance its own fault tolerance and ability to respond to changes, and endow software with an ability to respond to changes in the environment and user needs. Adaptability enables the software to collect software context information in real time during operation, and adjust its parameters, structure or behavior when necessary according to pre-set strategies, so as to eliminate or mitigate changes brought about by changes in a timely manner. adverse effects to ensure the continuous and uninterrupted service of the software. Due to the dynamic and changeable application sce...

AI Technical Summary

Problems solved by technology

Existing software requirements analysis and modeling methods (such as UML) lack facilities in the field of adaptive software, and cannot be directly used for modeling adaptive software, and it lacks a formal analysis and verification mechanism for the model, which can be formally verified directly Very difficult; existing formal methods (such as timed automata models) are too abstract, difficult to understand and master, and difficult to directly apply to industrial practice

Therefore, in most of the current research work, there is a "gap" between the visual modeling of adaptive software and formal modeling, which leads to visual methods that are intuitive but lack a strict analysis mechanism, which is unconvincing; The method definition is strict, but the readability is poor, and it is difficult for software engineers to understand and master

Although a few scholars (such as Andres J.Ramirez and Betty H.C.Cheng of Michigan State University) have tried to combine visual modeling methods and formal modeling methods for modeling and formal verification of adaptive software, but this aspect The research is immature and lacks consideration of factors such as model conversion algorithms and adaptive characteristics

Images