Font Size: a A A

Research On Formal Modeling And Security Verification Method Of Cyber-Physical Systems

Posted on:2020-08-11Degree:MasterType:Thesis
Country:ChinaCandidate:Q SuFull Text:PDF
GTID:2428330599476470Subject:Software engineering
Abstract/Summary:PDF Full Text Request
In today's highly interconnected world,cyber-physical systems(CPS)connects computer systems to physical devices.The computer system interacts with the physical environment to provide the services that people need every day,including transportation,construction equipment automation,electricity,irrigation works,industrial production and medical treatment,etc.With the research and development of CPS,some questions about the safety and reliability of CPS are gradually presented.Formal methods use mathematical language to abstract the software and hardware systems.They also can accurately standardize and verify the systems and their properties,in order to greatly improve the reliability and security of the systems,and ensure safe and correct working of the system.Because CPS have high requirements on time,and the timed automata contains clock constraints,this thesis uses timed automata as the modeling language to model CPS.This thesis first studies and analyzes the relevant knowledge of CPS,and then models each component of the system,and performs security properties verification on the models.Taking the water level control system as an example of CPS,the construction of each component model mainly contains system modeling,attacker modeling and automatic recovery mechanism modeling.The verifications of CPS security properties include deadlock,timing,and security detection based on the deadlock algorithm,reachability algorithm and the algorithm based on linear temporal logic.In addition,the thesis puts forward the language inclusion verification method of timed automata based on property patterns to verify the system models.The method is an improvement of the original method,and only the verification-related events are focused during the modeling.The achievements of the thesis are as follows:(1)The thesis gives the method of modeling CPS with timed automata.Taking the water level control system as an example,each component of the system is firstly constructed as one or more models based on timed automata.Then the models of the attacker and the automatic recovery mechanism are completed.Finally,the models are integrated into a complete system;(2)A language inclusion verification method of timed automata based on property patterns is proposed.The models with timed automata of several commonly used property patterns are summarized.Based on this,the existing language inclusion verification method is improved.The improved algorithm could ignore the irrelevant events among the modeling of properties,so that greatly simplifies the modeling of properties to be verified;(3)On the basis of the above model and verification method,the verification and analysis of whether the system satisfies security properties is completed.Firstly,the security properties are formally described.Then the corresponding assertion statements are written.Finally,the thesis gives the results of verification and analysis of the system based on the deadlock algorithm,reachability algorithm and the algorithm based on linear temporal logic and language inclusion verification method of timed automata based on property patterns.
Keywords/Search Tags:Cyber-Physical Systems, timed automata, formal modeling, PAT, language inclusion checking
PDF Full Text Request
Related items