Research And Application Of Conversion Method From Simulink/Stateflow Model To HCSP

With the growth of the complexity of embedded systems,designers are facing more and more quality problems.In order to improve the reliability of the system,researchers proposed and widely adopted model-based development methods.At present,Simulink/Stateflow tools are widely used in the industry to model and simulate embedded systems.However,due to the imperfection of simulation itself,the reliability of the system cannot be guaranteed only by simulation.Simulation with formal verification technology to improve system reliability has become a consensus in industry and academia.However,the lack of formal semantics in Simulink/Stateflow makes formal verification impossible.In view of the above problems,this paper analyzes the semantics of advanced functions of Stateflow and the shortcomings of existing conversion methods.First,a new conversion method based on modular design is proposed and Stateflow features are converted based on this method.Then,in order to ensure the simplicity of the result model,the optimization process for HCSP obtained after transformation is proposed for the first time.Finally,a set of benchmark examples is designed to ensure the correctness of the conversion results.In summary,the contributions of this paper are as follows:(1)This paper proposes a transformation method based on modular design,which modularizes the components of Stateflow model and treats each feature of Stateflow model independently.This method can not only reuse the converted results to improve conversion efficiency,but also make the obtained result model easier to understand and maintain.Based on this method,this paper reimplements the basic functions of the existing research work and also implements many advanced features of Stateflow that are not supported in the existing research,including Matlab functions,graphics functions,temporal logic event,directional event broadcast,history junctions,triggered subsystem and so on.(2)Optimization of this process was first proposed for HCSP after conversion.By performing four code optimizations: inlining of procedures,peephole optimization,constant propagation,and dead code elimination,some redundant content was deleted to make the resulting model more concise and easy to understand,and the execution speed was faster.(3)Numerous test examples were built to verify the correctness of the transformation process and the effectiveness of code optimization.This article records the running behavior of the current model by inserting output commands into the example.The correctness of the transformation process is ensured by comparing the output information of the model before and after the transformation.The effectiveness of the code optimization process was verified by comparing the size of HCSP programs before and after optimization.Each example is hand-designed to illustrate the semantics of some aspect of Stateflow.This article builds a baseline sample set of 112 examples covering a wide range of semantic issues.At the same time,to make the results of the transformation more persuasive,two large synthesis cases already existing in the existing study were tested.