Formal Analysis And Verification Of Uncertain Task Model Based On Parameter Logic Time Constraints

With the wide use of Internet of things,real-time and embedded systems and other related technologies in automobile,rail transit,aerospace,intelligent factory and other scenarios,the complexity and safety of these technologies are widely concerned by people.They need to be strictly modeled,analyzed and verified to ensure the safety and normal performance of the system.At the same time,for most of the Internet of things devices and real-time and embedded systems,their working environment is always very different.There are not only cars that can work at-50?C in winter and 50?C in summer,but also spacecraft that suffer extreme radiation or extreme high and low temperature in space.They need to face all kinds of extreme environment tests all the time,but they still need to meet the normal work needs,so they need to be strictly verified to ensure the stability of the work.However,in different working environments,these systems usually run at different speeds,which we call the uncertainty of execution time.For example,the CPU runs fastest when the temperature is moderate.At the same time,for some periodic time series behaviors,their periods may be uncertain before the completion of the design,which we call cycle uncertainty.In real-time and embedded systems,we always use the rising and falling edge of voltage to determine the clock period.However,when the voltage is not stable,there may be errors in multiple clock periods.In this paper,we classify them as period drift and period jitter.As for the uncertain temporal behaviors such as the uncertainty of execution time,period uncertainty,period drift and period jitter mentioned above,they are widely existed in a variety of real-time and embedded systems,so we need to carry out strict analysis and verification on them to ensure that they can meet the normal work requirements.In order to model the above-mentioned uncertain timing behavior and make full use of the scalability of logical time,this paper will adopt the method of introducing parameters in the clock constraint language CCSL based on logical time to expand it.At the same time,in order to solve the obscure grammatical semantics of parameterized CCSL constraints and reduce the difficulty of engineers using this method,we will use an uncertain task model to analyze the timing behavior and timing behavior between real-time and embedded systems The relationship between the two is modeled,and then the methods and algorithms for transforming the uncertain task model into parameterized CCSL constraints are summarized.Therefore,engineers only need to focus on modeling real-time and embedded systems using uncertain task models,and the corresponding methods of transforming into parameterized CCSL constraints can be automated.Next,we propose a method to convert parameterized CCSL constraints into SMT formulas and use quantifier elimination methods to reduce the complexity of the original SMT formula.After experimental verification,the quantifier elimination method can be used to improve the efficiency of solving CCSL constraints.Finally,we apply our method to a simple producer-consumer model and an industrial case of the FMTV(formal method of time verification)challenge proposed in 2015.The final results show that parametric CCSL constraints can be effectively used to model,analyze,and verify the task model with uncertain time-series behavior.