{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/98134"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/98134","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Remedies for building reliable cyber-physical systems","abstract":"Cyber-physical systems (CPS) are systems that are tight integration of computer programs as controllers or cyber parts, and physical environments. The interaction is carried out by obtaining information about the physical environment through reading sensors and responding to the current knowledge through actuators. Examples of such systems are autonomous automobile systems, avionic systems, robotic systems, and medical devices. Perhaps the most common feature of all these systems is that they are all safety critical systems and failure most likely causes catastrophic consequences. This means that while testing continues to increase confidence in cyber-physical systems, formal or mathematical proofs are needed at the very least for the safety requirements of these systems. Hybrid automata is the main modeling language for cyber-physical systems. However, verifying safety properties is undecidable for all but very restricted known classes of these automata. Our first result introduces a new subclass of hybrid automata for which bounded time safety model checking problem is decidable. We also prove that unbounded time model checking for this subclass is undecidable which suggests this is the best one can hope for the new class. Our second result in this thesis is a counter-example guided abstraction refinement algorithm for unbounded time model checking of non- linear hybrid automata. Clearly, this is an undecidable problem and that is the main reason for using abstraction refinement techniques. Our CEGAR framework for this class is sound but not complete, meaning the algorithm never incorrectly says a system is safe, but may output unsafe incorrectly. We have also implemented our algorithm and compared it with seven other tools. There are multiple inherent problems with traditional model checking approaches. First, it is well-known that most models do not depict physical environments precisely. Second, the model checking problem is undecidable for most classes of hybrid automata. And third, even when model checking is decidable, controller part in most models cannot be implemented. These problems suggest that current methods of modeling cyber-physical systems and problems might not be the right ones. Our last result focuses on robust model checking of cyber-physical systems. In this part of the thesis, we focus on the implementability issue and show how to solve four different robust model checking problem for timed automata. We also introduce an optimal algorithm for robust time bounded safety model checking of monotonic rectangular automata.","abstract_html":"Cyber-physical systems (CPS) are systems that are tight integration of computer programs as controllers or cyber parts, and physical environments. The interaction is carried out by obtaining information about the physical environment through reading sensors and responding to the current knowledge through actuators. Examples of such systems are autonomous automobile systems, avionic systems, robotic systems, and medical devices. Perhaps the most common feature of all these systems is that they are all safety critical systems and failure most likely causes catastrophic consequences. This means that while testing continues to increase confidence in cyber-physical systems, formal or mathematical proofs are needed at the very least for the safety requirements of these systems. Hybrid automata is the main modeling language for cyber-physical systems. However, verifying safety properties is undecidable for all but very restricted known classes of these automata. Our first result introduces a new subclass of hybrid automata for which bounded time safety model checking problem is decidable. We also prove that unbounded time model checking for this subclass is undecidable which suggests this is the best one can hope for the new class. Our second result in this thesis is a counter-example guided abstraction refinement algorithm for unbounded time model checking of non- linear hybrid automata. Clearly, this is an undecidable problem and that is the main reason for using abstraction refinement techniques. Our CEGAR framework for this class is sound but not complete, meaning the algorithm never incorrectly says a system is safe, but may output unsafe incorrectly. We have also implemented our algorithm and compared it with seven other tools. There are multiple inherent problems with traditional model checking approaches. First, it is well-known that most models do not depict physical environments precisely. Second, the model checking problem is undecidable for most classes of hybrid automata. And third, even when model checking is decidable, controller part in most models cannot be implemented. These problems suggest that current methods of modeling cyber-physical systems and problems might not be the right ones. Our last result focuses on robust model checking of cyber-physical systems. In this part of the thesis, we focus on the implementability issue and show how to solve four different robust model checking problem for timed automata. We also introduce an optimal algorithm for robust time bounded safety model checking of monotonic rectangular automata.","abstract_has_math":false,"creators":["Roohi, Nima"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Viswanathan, Mahesh","Dullerud, Geir","Mitra, Sayan","Misailovic, Sasa","Tivari, Ashish"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2017,"date_issued":"2017-09-29T16:38:03Z","date_published":"2017-09-29T16:38:03Z","updated_at":"2026-07-22T22:24:35Z","subjects":["Hybrid automata","Cyber-physical systems","Formal model checking","Safety","Robust model checking","Counter example guided abstraction refinement (CEGAR)"],"languages":["en"],"rights":["Copyright 2017 Nima Roohi"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/98134","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Viswanathan, Mahesh","Dullerud, Geir","Mitra, Sayan","Misailovic, Sasa","Tivari, Ashish"]},{"key":"dc:creator","label":"Author","values":["Roohi, Nima"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2017-09-29T16:38:03Z","2017-06-30","2017-08"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Hybrid automata","Cyber-physical systems","Formal model checking","Safety","Robust model checking","Counter example guided abstraction refinement (CEGAR)"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2017 Nima Roohi"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/98134"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Cyber-physical systems (CPS) are systems that are tight integration of computer programs as controllers or cyber parts, and physical environments. The interaction is carried out by obtaining information about the physical environment through reading sensors and responding to the current knowledge through actuators. Examples of such systems are autonomous automobile systems, avionic systems, robotic systems, and medical devices. Perhaps the most common feature of all these systems is that they are all safety critical systems and failure most likely causes catastrophic consequences. This means that while testing continues to increase confidence in cyber-physical systems, formal or mathematical proofs are needed at the very least for the safety requirements of these systems. Hybrid automata is the main modeling language for cyber-physical systems. However, verifying safety properties is undecidable for all but very restricted known classes of these automata. Our first result introduces a new subclass of hybrid automata for which bounded time safety model checking problem is decidable. We also prove that unbounded time model checking for this subclass is undecidable which suggests this is the best one can hope for the new class. Our second result in this thesis is a counter-example guided abstraction refinement algorithm for unbounded time model checking of non- linear hybrid automata. Clearly, this is an undecidable problem and that is the main reason for using abstraction refinement techniques. Our CEGAR framework for this class is sound but not complete, meaning the algorithm never incorrectly says a system is safe, but may output unsafe incorrectly. We have also implemented our algorithm and compared it with seven other tools. There are multiple inherent problems with traditional model checking approaches. First, it is well-known that most models do not depict physical environments precisely. Second, the model checking problem is undecidable for most classes of hybrid automata. And third, even when model checking is decidable, controller part in most models cannot be implemented. These problems suggest that current methods of modeling cyber-physical systems and problems might not be the right ones. Our last result focuses on robust model checking of cyber-physical systems. In this part of the thesis, we focus on the implementability issue and show how to solve four different robust model checking problem for timed automata. We also introduce an optimal algorithm for robust time bounded safety model checking of monotonic rectangular automata.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2017-09-29 without embargo terms","The student, Nima Roohi, accepted the attached license on 2017-06-27 at 12:03.","The student, Nima Roohi, submitted this Dissertation for approval on 2017-06-27 at 12:04.","This Dissertation was approved for publication on 2017-06-30 at 09:37.","DSpace SAF Submission Ingestion Package generated from Vireo submission #11271 on 2017-09-29 at 11:27:14","Made available in DSpace on 2017-09-29T16:38:03Z (GMT). No. of bitstreams: 2 ROOHI-DISSERTATION-2017.pdf: 4713672 bytes, checksum: e845267404a78b6a2ee24aec3cd01c3a (MD5) LICENSE.txt: 4207 bytes, checksum: 3a5829f21c169fc67cad3abd29229e8a (MD5) Previous issue date: 2017-06-30"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Remedies for building reliable cyber-physical systems"]}]}],"canonical_facts":{"dc:contributor":["Viswanathan, Mahesh","Dullerud, Geir","Mitra, Sayan","Misailovic, Sasa","Tivari, Ashish"],"dc:creator":["Roohi, Nima"],"dc:date":["2017-09-29T16:38:03Z","2017-06-30","2017-08"],"dc:description":["Cyber-physical systems (CPS) are systems that are tight integration of computer programs as controllers or cyber parts, and physical environments. The interaction is carried out by obtaining information about the physical environment through reading sensors and responding to the current knowledge through actuators. Examples of such systems are autonomous automobile systems, avionic systems, robotic systems, and medical devices. Perhaps the most common feature of all these systems is that they are all safety critical systems and failure most likely causes catastrophic consequences. This means that while testing continues to increase confidence in cyber-physical systems, formal or mathematical proofs are needed at the very least for the safety requirements of these systems. Hybrid automata is the main modeling language for cyber-physical systems. However, verifying safety properties is undecidable for all but very restricted known classes of these automata. Our first result introduces a new subclass of hybrid automata for which bounded time safety model checking problem is decidable. We also prove that unbounded time model checking for this subclass is undecidable which suggests this is the best one can hope for the new class. Our second result in this thesis is a counter-example guided abstraction refinement algorithm for unbounded time model checking of non- linear hybrid automata. Clearly, this is an undecidable problem and that is the main reason for using abstraction refinement techniques. Our CEGAR framework for this class is sound but not complete, meaning the algorithm never incorrectly says a system is safe, but may output unsafe incorrectly. We have also implemented our algorithm and compared it with seven other tools. There are multiple inherent problems with traditional model checking approaches. First, it is well-known that most models do not depict physical environments precisely. Second, the model checking problem is undecidable for most classes of hybrid automata. And third, even when model checking is decidable, controller part in most models cannot be implemented. These problems suggest that current methods of modeling cyber-physical systems and problems might not be the right ones. Our last result focuses on robust model checking of cyber-physical systems. In this part of the thesis, we focus on the implementability issue and show how to solve four different robust model checking problem for timed automata. We also introduce an optimal algorithm for robust time bounded safety model checking of monotonic rectangular automata.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2017-09-29 without embargo terms","The student, Nima Roohi, accepted the attached license on 2017-06-27 at 12:03.","The student, Nima Roohi, submitted this Dissertation for approval on 2017-06-27 at 12:04.","This Dissertation was approved for publication on 2017-06-30 at 09:37.","DSpace SAF Submission Ingestion Package generated from Vireo submission #11271 on 2017-09-29 at 11:27:14","Made available in DSpace on 2017-09-29T16:38:03Z (GMT). No. of bitstreams: 2 ROOHI-DISSERTATION-2017.pdf: 4713672 bytes, checksum: e845267404a78b6a2ee24aec3cd01c3a (MD5) LICENSE.txt: 4207 bytes, checksum: 3a5829f21c169fc67cad3abd29229e8a (MD5) Previous issue date: 2017-06-30"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/98134"],"dc:language":["en"],"dc:rights":["Copyright 2017 Nima Roohi"],"dc:subject":["Hybrid automata","Cyber-physical systems","Formal model checking","Safety","Robust model checking","Counter example guided abstraction refinement (CEGAR)"],"dc:title":["Remedies for building reliable cyber-physical systems"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:35Z"}