Research On Automatic Extraction And Verification Of STL Properties For Simulink Models

In recent years,the embedded software has been widely used in all walks of life,especially in some safety-critical fields.At the same time,the software requirements are more complex,and the most key is the real-time specification in the requirements.Traditional temporal logic languages,such as LTL and CTL,are mainly used to describe the temporal properties of discrete systems and can not deal with the changes of real valued signals in continuous time.STL can be used to describe the characteristics and temporal behavior of real valued signals in continuous dynamical systems.Therefore,STL is widely used to describe complex temporal requirements in safety critical fields.On the other hand,Simulink has been widely used to design and implement system models in various fields,especially in some safety-critical fields.Beyond modeling and simulation,Simulink can also automatically generate C and HDL code from the model.However,the verification ability of Simulink is very limited,and it is unable to verify the complex time properties described by STL.Therefore,we study the automatic extraction and verification methods of STL properties for Simulink models,and our methods can ensure the security and credibility of the model.The main work and contributions of this paper are as follows:1.Firstly,we propose a method to extract temporal logic STL from natural language requirements based on natural language processing technology.According to the temporal operators,logical operators,comparison operators and other elements in STL,we formulate the extraction rules in detail,and design and implement the algorithm to automatically extract and generate formulas.This part of our work can ensure the consistency of requirements and time properties.2.On the basis of describing the requirements with STL formula,we propose a comprehensive and scalable framework to automatically verify whether a Simulink model meets the requirements based on UPPAAL timed automata.The core of the framework is to formally model the Simulink model and translate it into UPPAAL timed automata.At the same time,our algorithm based on symbolic execution designed can effectively avoid the state explosion problem of translated timed automata.3.We applied our verification framework on two industrial Simulink model cases.The experimental results show the viability and effectiveness of our verification framework,which provides an important reference for the formal verification of STL properties in Simulink model.