Trusted Modeling And Verification Method Of Time Property Software For Cyber Physical System

Formal method has been widely applied in industrial field,and it has important meaning on revealing the essence of software designing.However,the systematic structure of software in CPS is dynamic depending on the demand and environment.Except the functional requirements,dynamic software system also requires non-functional requirements,such as timing.Currently,there has been no mature modeling methods for that how to precisely describe and verify software system yet.To improve the liability of CPS,the key research on CPS trusted property is how to precisely describe software system,how to extract systemic specification from the software requirements conditions,and how to efficiently check system model in order to detect potential mistakes in the early stage of software designing and correct the inconsistency and incompleteness in software requirements and system designs.Formal method should be used to improve the trust of CPS software.We try to build the integration framework based on model driven,and propose a method for modeling and verifying time trusted property of CPS software.Using the formalization of Object-Z to describe the static semantics of model and the timing constraints and transition probability of PTA to describe the dynamic semantics of model,we propose a time trusted software model.We utilize the scenario-based language to analyze requirements,and further extract the requirement specification.For the time trusted property of CPS software,we also design a model checking algorithm to verify time property.From software model,requirements specification and model checking,we has carried on the thorough exploration research,the main innovative research results are as follows:(1)For precisely describe the functional properties and non-functional properties such as time,we studied the graphic model and formal modelling method.Constructing graphic model of software system is very convenient for software developers.Graphic model could efficiently reduce the complexity during software development,however,it is not conductive for software verification.We took advantage of MARTE,which is advanced on constructing non-functional properties,and formal integrated model that fused both static structure and dynamic behavior.Under the MDA framework,we defined the mapping rules from MARTE static structure to Object-Z class and also from MARTE dynamic behavior to PTA expression,and propose the integrated formal modeling method PTA-OZ.The method could be used to verify the static structure and dynamic behavior of software model built by MARTE.Thus,we could take advantage of formalized methods to verify the models constructed by using graphic modeling language.In addition,this study verified the consistency of semantic on model transformation by using methods that combined invariance and triple metamodel,and achieved this transform framework based on XMI in Papyrus condition.Experimental analysis indicated that the formal integration model can be effectively used to verify the function properties and non-functional properties such as real-time.(2)We introduced the formalized definition of clock and time constraints,and defined the time property model of LSC graph,then proposed the translation rules from TLSC to time logic formal,further introduced the optimizing formula method.This study focused on property problem of time sensitive LSC,since the unnegligible affect of time on the behavior of CPS software system.Through introducing the formalized definition of clock and time constraints,we proposed a new chart called TLSC,and utilized it to solove the time property problem using scenario-based language during the stage of describing software requirement.We defined the grammar and syntax of TLSC by using formalized methods to facilitate converted into temporal logic formula.This study defined the basic rule and combination rule,thus achieved the transfom from TLSC to temporal logic formula.In order to simplify formula scale,we used the transitivity to redefine time sequence relation,and in further studied the method for improving formula.This study designed and completed the transform system from TLSC to temporal logic formula,and achieved that automatically extracting logic formula from requirement analysis.(3)For precisely calculating the completeness threshold of bounded model checking,this study first introduced semi-tensor product theory to bounded model checking,and present a solving method for completeness threshold which studied the topology structure of status evolution of Kripke model by using the discrete time evolution system.Firstly we designed a algorithem for analyzing Kripke model to establish the algebraic form of Boolean function,and tranfomed it into logic form.Secondly we designed algorithms for solving fixed point and solving k-loop to calculate the attractor in Boolean network.Lastly we calculated the position of fixed point,the length and the state set of loop according to the attractor.The prior radius that solves Kripke model using matrix analysis in classic mathematical theory was used as the completeness threshold.Compared with previous threshold calculation method,this method is simple in calculation,and less time-consuming.(4)For improving the efficiency of bounded model checking,this study present a bounded model checking algorithm for CPS-oriented time trusted property,and fully considered the time property lacking problem in SAT-based coding.For temporal logic formula in CPS real-time system,the bounded model checking algorithm of RTECTL formula based on SMT was studied.The time property in formula was remained in propositional formula coding.This study proposed optimization selection of path quantifier E to reduce run number,and proved the feasibility of this coding method in theory.