A Serialization Model Checking Method For Distributed Multi-Tasking Application Software System

There is an important part of the on-board software system based on OSEK/VDX standard: multi-task application software.The distributed system composed of multi-task application software is widely deployed in the automobile.However,the application software in this distributed system is executed concurrently,and multiple tasks in the software are also executed concurrently.With the continuous improvement of development complexity,how to thoroughly detect the developed distributed multi-tasking application software system has become a challenge for developers.In order to thoroughly detect the distributed multitasking application software system,relevant researchers have proposed a naive detection method based on the model detector UPPAAL to detect this distributed system.Although this method can detect this kind of distributed system,it may not be able to detect it effectively in the face of large-scale distributed system.In order to detect large-scale distributed multitasking application software systems,this paper proposes a model checking method which uses serialization method to reduce the number of concurrent processes in the detection model.Through this method and the use of model detector to achieve the purpose of detecting large-scale distributed multitasking application software systems.First of all,serialization is carried out to transform all the application software in the distributed system into an equivalent serialization model,and then a detection model is constructed based on the serialization model and communication protocol model of all application software.Finally,the constructed detection model is used to detect the attributes that need to be verified using the model detector.According to the proposed serialization model checking method,an automatic tool is developed at the same time.Taking the source file and configuration file of multitasking application software as input,the tool can obtain equivalent serialization model and equivalent PROMELA model.Based on this automation tool,the serialization model detection method and naive detection method proposed in this paper are used to compare the distributed multitasking application software systems with different behaviors.The experimental results show that the serialization model detection method proposed in this paper can detect large-scale distributed multitasking application software systems compared with the naive detection method.