{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/50553"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/50553","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Rewriting-based model checking methods","abstract":"Model checking is an automatic technique for verifying concurrent systems. The properties of the system to be verified are typically expressed as temporal logic formulas, while the system itself is formally specified as a certain system specification language, such as computational logics and conventional programming languages. Rewriting logic is a highly expressive computational logic for effectively defining a formal executable semantics of a wide range of system specification languages. This dissertation presents new rewriting-based model checking methods and tools to effectively verify concurrent systems by means of their rewriting-based formal semantics. Specifically, this work develops: (i) efficient model checking algorithms and a tool for a suitable property specification language, namely, linear temporal logic of rewriting (LTLR) formulas under parameterized fairness; (ii) various infinite-state model checking techniques for LTLR properties, such as equational abstraction, folding abstraction, predicate abstraction, and narrowing-based symbolic model checking; and (iii) the Multirate PALS methodology for making it possible to model check virtually synchronous cyber-physical systems by reducing their system complexity. To demonstrate rewriting-based model checking, we have developed fully integrated modeling and model checking tools for two widely-used embedded system modeling languages, AADL and Ptolemy II. This approach provides a model-engineering process that combines the advantages of an existing modeling language with automatic rewriting-based model checking.","abstract_html":"Model checking is an automatic technique for verifying concurrent systems. The properties of the system to be verified are typically expressed as temporal logic formulas, while the system itself is formally specified as a certain system specification language, such as computational logics and conventional programming languages. Rewriting logic is a highly expressive computational logic for effectively defining a formal executable semantics of a wide range of system specification languages. This dissertation presents new rewriting-based model checking methods and tools to effectively verify concurrent systems by means of their rewriting-based formal semantics. Specifically, this work develops: (i) efficient model checking algorithms and a tool for a suitable property specification language, namely, linear temporal logic of rewriting (LTLR) formulas under parameterized fairness; (ii) various infinite-state model checking techniques for LTLR properties, such as equational abstraction, folding abstraction, predicate abstraction, and narrowing-based symbolic model checking; and (iii) the Multirate PALS methodology for making it possible to model check virtually synchronous cyber-physical systems by reducing their system complexity. To demonstrate rewriting-based model checking, we have developed fully integrated modeling and model checking tools for two widely-used embedded system modeling languages, AADL and Ptolemy II. This approach provides a model-engineering process that combines the advantages of an existing modeling language with automatic rewriting-based model checking.","abstract_has_math":false,"creators":["Bae, Kyungmin"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Meseguer, José","Agha, Gul A.","Clarke, Edmund M.","Roşu, Grigore"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2014,"date_issued":"2014-09-16T17:23:47Z","date_published":"2014-09-16T17:23:47Z","updated_at":"2026-07-22T22:25:40Z","subjects":["Model checking","Rewriting logic","Formal methods","Temporal logic","Infinite-state systems","Cyber-physical systems"],"languages":["en"],"rights":["Copyright 2014 Kyungmin Bae"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/50553","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Meseguer, José","Agha, Gul A.","Clarke, Edmund M.","Roşu, Grigore"]},{"key":"dc:creator","label":"Author","values":["Bae, Kyungmin"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2014-09-16T17:23:47Z","2014-08","2014-09-16"]},{"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":["Model checking","Rewriting logic","Formal methods","Temporal logic","Infinite-state systems","Cyber-physical systems"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2014 Kyungmin Bae"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/50553"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Model checking is an automatic technique for verifying concurrent systems. The properties of the system to be verified are typically expressed as temporal logic formulas, while the system itself is formally specified as a certain system specification language, such as computational logics and conventional programming languages. Rewriting logic is a highly expressive computational logic for effectively defining a formal executable semantics of a wide range of system specification languages. This dissertation presents new rewriting-based model checking methods and tools to effectively verify concurrent systems by means of their rewriting-based formal semantics. Specifically, this work develops: (i) efficient model checking algorithms and a tool for a suitable property specification language, namely, linear temporal logic of rewriting (LTLR) formulas under parameterized fairness; (ii) various infinite-state model checking techniques for LTLR properties, such as equational abstraction, folding abstraction, predicate abstraction, and narrowing-based symbolic model checking; and (iii) the Multirate PALS methodology for making it possible to model check virtually synchronous cyber-physical systems by reducing their system complexity. To demonstrate rewriting-based model checking, we have developed fully integrated modeling and model checking tools for two widely-used embedded system modeling languages, AADL and Ptolemy II. This approach provides a model-engineering process that combines the advantages of an existing modeling language with automatic rewriting-based model checking.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2014-07-14T18:19:22Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 1 Bae_Kyungmin.pdf: 3839986 bytes, checksum: f03c26eb4bfd69b988a3a0ea933870f3 (MD5)","Made available in DSpace on 2014-09-16T17:23:47Z (GMT). No. of bitstreams: 2 Kyungmin_Bae.pdf: 3839986 bytes, checksum: f03c26eb4bfd69b988a3a0ea933870f3 (MD5) license.txt: 4059 bytes, checksum: 40b1488fd92f93fbe3b18af938328807 (MD5)"]},{"key":"dc:title","label":"Title","values":["Rewriting-based model checking methods"]}]}],"canonical_facts":{"dc:contributor":["Meseguer, José","Agha, Gul A.","Clarke, Edmund M.","Roşu, Grigore"],"dc:creator":["Bae, Kyungmin"],"dc:date":["2014-09-16T17:23:47Z","2014-08","2014-09-16"],"dc:description":["Model checking is an automatic technique for verifying concurrent systems. The properties of the system to be verified are typically expressed as temporal logic formulas, while the system itself is formally specified as a certain system specification language, such as computational logics and conventional programming languages. Rewriting logic is a highly expressive computational logic for effectively defining a formal executable semantics of a wide range of system specification languages. This dissertation presents new rewriting-based model checking methods and tools to effectively verify concurrent systems by means of their rewriting-based formal semantics. Specifically, this work develops: (i) efficient model checking algorithms and a tool for a suitable property specification language, namely, linear temporal logic of rewriting (LTLR) formulas under parameterized fairness; (ii) various infinite-state model checking techniques for LTLR properties, such as equational abstraction, folding abstraction, predicate abstraction, and narrowing-based symbolic model checking; and (iii) the Multirate PALS methodology for making it possible to model check virtually synchronous cyber-physical systems by reducing their system complexity. To demonstrate rewriting-based model checking, we have developed fully integrated modeling and model checking tools for two widely-used embedded system modeling languages, AADL and Ptolemy II. This approach provides a model-engineering process that combines the advantages of an existing modeling language with automatic rewriting-based model checking.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2014-07-14T18:19:22Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 1 Bae_Kyungmin.pdf: 3839986 bytes, checksum: f03c26eb4bfd69b988a3a0ea933870f3 (MD5)","Made available in DSpace on 2014-09-16T17:23:47Z (GMT). No. of bitstreams: 2 Kyungmin_Bae.pdf: 3839986 bytes, checksum: f03c26eb4bfd69b988a3a0ea933870f3 (MD5) license.txt: 4059 bytes, checksum: 40b1488fd92f93fbe3b18af938328807 (MD5)"],"dc:identifier":["http://hdl.handle.net/2142/50553"],"dc:language":["en"],"dc:rights":["Copyright 2014 Kyungmin Bae"],"dc:subject":["Model checking","Rewriting logic","Formal methods","Temporal logic","Infinite-state systems","Cyber-physical systems"],"dc:title":["Rewriting-based model checking methods"],"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:25:40Z"}