Research On Verification Of Trustworthiness For CPS Software Based On Statistical Model Checking

With the significant development of embedded technology, computer technology andnetwork technology, as well as hardware performance and data processing capabilities onthe rise, the technology of Internet of Things has rapid development. Under that situation,Cyber-Physical systems (CPS) come into being as a new type of embedded network systemwhich has attracted high attention of governments, academia and industry. CPS is acomplex embedded network system that combines computing and the physical process.Embedded computers and networks are used to monitor and control the physical processeswith feedback loops where physical processes affect computations and vice versa. CPS isusually widely used to monitor and control in many safety-critical areas, such as defenseweapons systems, health care, intelligent transportation and other important infrastructure.The physical environment is often uncertain, and the physical device itself may be faulty,so it is an important challenge to ensure the entire CPS robustness and safety. However, thereliability of CPS is closely related with the reliability of CPS software, so it’s veryimportant to ensure that CPS software is reliable.Formal verification is an important method to improve software reliability, and modelchecking, one technique of formal verification methods, is often used to verify softwareproperties. The application of traditional model checking is limited by the size of statespace, but the size of CPS state space is very huge. Statistical model checking is a kind ofmodel checking technology to verify huge complex system based on simulation andstatistical evaluation technology, which can be applied to verify infinite system. It is verydifficult to verify CPS software using traditional model checking. Thanks to that problem,statistical model checking is used in this paper, where three core steps about CPS softwareproperty verification are studied: CPS software modeling, CPS software properties staticverification and CPS software properties run-time verification. First, as the extension tohybrid automata, communication port is introduced on the basis of hybrid automata, andthen CPS software model, formal model can effectively express CPS important information, is created. Secondly, a new method to act on the CPS properties staticverification is proposed based on statistical model checking technology. Finally, someimprovements on CPS model are made to present the uncertainty of CPS, where theenvironmental factors impact on CPS is taken into account, such as modeling theuncertainty in CPS and study the approach to verify CPS software properties at run-time. Itcan effectively avoid the state space explosion problem, which the traditional modelchecking techniques must face, to using statistical model checking techniques to verifyCPS properties, enhancing the robustness and safety of CPS.