Composition And Refinement Of Timing Behavior For Cyber Physic Systems

The functions and complexity of cyber physical systems(CPS)need to meet safety requirements while grow with each passing day,which makes it necessary to analyze and verify the correctness and safety of timing behavior from the specification layer to the implementation layer in the process of system development.As an extension of UML 2.0,clock constraint specification language(CCSL)has been widely concerned by many researchers.It defines time modeling elements with rich semantics to describe the timing behavior of CPS,and provides effective support for time modeling of components.At present,the timing behavior analysis and verification based on CCSL modeling language has achieved some fruitful research results.However,the design and analysis of CPS based on CCSL language still lacks more specific timing behavior composition operation methods,timing behavior composability verification rules and other implementation technologies.Similar problems are still the main challenges faced by the industry and academic.In view of the above technical requirements,this dissertation proposes an CPS development framework based on timing behavior model with CCSL language as the core.In this framework,the timing behavior model of the system is established by using logical clocks.On this basis,the specific implementation technologies such as the operation method of time behavior composition and the formal definition of component timing behavior composability are given.The specific work and contributions of this paper are as follows:(1)This dissertation presents a composition method of component time behavior based on clock transition systems.Based on the concept of logical clock in CCSL,a component timing behavior model is established,and the ticking behavior of logical clock is modeled as the transition action in the transition system to simplify the complex intermediate formal semantic transformation.Furthermore,a component timing behavior composition method based on the clock transition system is further given.At the same time,the formal definition of composability of timing behavior based on optimistic perspective is given,which lays a theoretical foundation for time behavior analysis and composability verification of components.(2)Aiming at the problem of state explosion caused by the composition of timing behavior models,a heuristic grouping compositional verification framework based on L*learning is proposed.Based on the idea of divide and conquer,the framework transforms the properties verification of the overall model into the process derivation of the behavior properties of the individual model,so as to alleviate the problem of difficult verification of the timing behavior model due to the state explosion after the composition.At the same time,considering the difference of timing behavior,the learning process of behavior is divided into two stages:no timing behavior reasoning and timing behavior reasoning,and a heuristic grouping verification strategy is given to further divide components to reduce the number of model verification and improve the verification efficiency.The experimental results show that the verification method using heuristic grouping reduces the time by 18.66%to 36.67%and the memory consumption by 32.43%to 47.99%compared with the verification method without grouping.In terms of the verification performance of timing behavior,compared with the existing UPPAAL tools,the verification time is reduced by 37.15%to 48.12%.It can be seen from the experimental process that for some scenarios that cannot be verified due to large memory consumption,the composition verification method of heuristic grouping can also obtain corresponding verification results.(3)The timing behavior refinement method from requirement model to task model is given.Considering the scene characteristics of safety critical CPS,the method refines the three time behaviors of delay constraint,association constraint and separation constraint,which is more in line with the expression requirements of CPS function requirement layer for timing constraint behavior.The task graph structure is given to establish the relationship between the higer level time behavior model and the lower level time behavior model,and finally generate the values such as the period,phase and deadline of the task.The refinement method introduces the resource utilization ratio to limit the value range of the task execution cycle,further reducing the solution space of the task set and effectively reducing the number of iterative searches in the solution space,and at the same time making the generated task set have the best execution performance on the premise that the task can be scheduled.The number of components with the interval of 0-1000 is randomly selected for the simulation test of task set generation.The results of multiple experiments show that,in terms of the scalability of the refinement method,the timing behavior refinement method reduces 0.11 iteration search times(taking natural logarithm)on average compared with the UML-RT refinement method,and reduces 3.16 iteration search times on average compared with the Shige refinement method through decomposition and synthesis.In terms of the effectiveness of the refinement method,the refinement method in this dissertation defines the generated task set through utilization.On the premise of meeting the system time constraint,the resource utilization rate of the generated task set can be increased by 15.22%compared with before optimization.(4)Take the master-slave intelligent car system as a practical case to develop and practice.First,CCSL language is used to establish the timing behavior requirement model of the component,and the properties of the specific task is obtained by refinement method.Corresponding to the intelligent car function versions car-1,2 and 3,37,41 and 49 logical clocks are respectively defined to describe the behaviors of task release,preemption and finish,so as to establish the timing behavior model of the overall task.Based on the timing behavior model of WiFi network,the different working states of WiFi components are further abstracted,and a novel method of WiFi network transmission behavior analysis and power consumption prediction is formed.The experimental data show that the relative error between the predicted value and the real value is within 7.12%.Finally,the correctness,composability and other functional/non functional properties of the system are verified.The relevant statistical data also show that the performance of the refinement method and the composition verification method presented in this dissertation is better than the scheme before optimization to a certain extent.To sum up,this dissertation studies the timing behavior modeling and analysis of components in CPS.The specific work includes:present the composition method of timing behavior model,giving the formal definition of composability of the timing behavior,putting forward the compositional verification method based on L*learning,and the refinement method of time behavior model,and on this basis,developing and analyzing the master-slave intelligent car system.Relevant experiments and statistical data show that the research in this dissertation has certain theoretical significance and engineering practice value,and plays a positive role in promoting the development and design of CPS.