{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/26197"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/26197","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Translation of Simulink-Stateflow models to hybrid automata","abstract":"Formal analysis of Simulink/Stateflow (SLSF) diagrams requires association of semantics to these diagrams. In this thesis, we present a technique and the related tool called HyLink for translating a useful subclass of SLSF diagrams to hybrid automata. In the absence of official semantics, there are two possible interpretations of these diagrams: one is based on the ideal mathematical interpretation obtained from the syntax of the building blocks and the other is based on the simulation traces generated by the simulation engine. These two interpretations lead to two different kinds of hybrid automata---the former gives an automaton with state-dependent transitions and the latter gives a time-triggered automaton. We show that under certain assumptions, the semantics of the latter converge to the former as the simulation step size decreases. We illustrate HyLink's translation scheme, the assumptions, and the convergence result through several case studies.","abstract_html":"Formal analysis of Simulink/Stateflow (SLSF) diagrams requires association of semantics to these diagrams. In this thesis, we present a technique and the related tool called HyLink for translating a useful subclass of SLSF diagrams to hybrid automata. In the absence of official semantics, there are two possible interpretations of these diagrams: one is based on the ideal mathematical interpretation obtained from the syntax of the building blocks and the other is based on the simulation traces generated by the simulation engine. These two interpretations lead to two different kinds of hybrid automata---the former gives an automaton with state-dependent transitions and the latter gives a time-triggered automaton. We show that under certain assumptions, the semantics of the latter converge to the former as the simulation step size decreases. We illustrate HyLink's translation scheme, the assumptions, and the convergence result through several case studies.","abstract_has_math":false,"creators":["Manamcheri Sukumar, Karthikeyan"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Electrical & Computer Engr","degree_department":null,"school":null,"contributors":["Mitra, Sayan"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2011,"date_issued":"2011-08-25T22:18:21Z","date_published":"2011-08-25T22:18:21Z","updated_at":"2026-07-22T22:25:26Z","subjects":["Translation of Simulink Stateflow","Hybrid Automata","Simulink Stateflow models","Verification of Simulink Stateflow","Semantics of Simulink Stateflow"],"languages":["en"],"rights":["Copyright 2011 Karthikeyan Manamcheri Sukumar"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/26197","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Mitra, Sayan"]},{"key":"dc:creator","label":"Author","values":["Manamcheri Sukumar, Karthikeyan"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2011-08-25T22:18:21Z","2011-08"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Electrical & Computer Engr"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S."]},{"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":["Translation of Simulink Stateflow","Hybrid Automata","Simulink Stateflow models","Verification of Simulink Stateflow","Semantics of Simulink Stateflow"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2011 Karthikeyan Manamcheri Sukumar"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/26197"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Formal analysis of Simulink/Stateflow (SLSF) diagrams requires association of semantics to these diagrams. In this thesis, we present a technique and the related tool called HyLink for translating a useful subclass of SLSF diagrams to hybrid automata. In the absence of official semantics, there are two possible interpretations of these diagrams: one is based on the ideal mathematical interpretation obtained from the syntax of the building blocks and the other is based on the simulation traces generated by the simulation engine. These two interpretations lead to two different kinds of hybrid automata---the former gives an automaton with state-dependent transitions and the latter gives a time-triggered automaton. We show that under certain assumptions, the semantics of the latter converge to the former as the simulation step size decreases. We illustrate HyLink's translation scheme, the assumptions, and the convergence result through several case studies.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2011-07-16T16:19:25Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 1 Manamcheri Sukumar_Karthikeyan.pdf: 1097140 bytes, checksum: 831a1e1e1aa69016150968be5b972d35 (MD5)","Made available in DSpace on 2011-08-25T22:18:21Z (GMT). No. of bitstreams: 2 ManamcheriSukumar_Karthikeyan.pdf: 1097140 bytes, checksum: 831a1e1e1aa69016150968be5b972d35 (MD5) license.txt: 4072 bytes, checksum: 21d3503a17186f085e3d4f8436b5f3c9 (MD5)"]},{"key":"dc:title","label":"Title","values":["Translation of Simulink-Stateflow models to hybrid automata"]}]}],"canonical_facts":{"dc:contributor":["Mitra, Sayan"],"dc:creator":["Manamcheri Sukumar, Karthikeyan"],"dc:date":["2011-08-25T22:18:21Z","2011-08"],"dc:description":["Formal analysis of Simulink/Stateflow (SLSF) diagrams requires association of semantics to these diagrams. In this thesis, we present a technique and the related tool called HyLink for translating a useful subclass of SLSF diagrams to hybrid automata. In the absence of official semantics, there are two possible interpretations of these diagrams: one is based on the ideal mathematical interpretation obtained from the syntax of the building blocks and the other is based on the simulation traces generated by the simulation engine. These two interpretations lead to two different kinds of hybrid automata---the former gives an automaton with state-dependent transitions and the latter gives a time-triggered automaton. We show that under certain assumptions, the semantics of the latter converge to the former as the simulation step size decreases. We illustrate HyLink's translation scheme, the assumptions, and the convergence result through several case studies.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2011-07-16T16:19:25Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 1 Manamcheri Sukumar_Karthikeyan.pdf: 1097140 bytes, checksum: 831a1e1e1aa69016150968be5b972d35 (MD5)","Made available in DSpace on 2011-08-25T22:18:21Z (GMT). No. of bitstreams: 2 ManamcheriSukumar_Karthikeyan.pdf: 1097140 bytes, checksum: 831a1e1e1aa69016150968be5b972d35 (MD5) license.txt: 4072 bytes, checksum: 21d3503a17186f085e3d4f8436b5f3c9 (MD5)"],"dc:identifier":["http://hdl.handle.net/2142/26197"],"dc:language":["en"],"dc:rights":["Copyright 2011 Karthikeyan Manamcheri Sukumar"],"dc:subject":["Translation of Simulink Stateflow","Hybrid Automata","Simulink Stateflow models","Verification of Simulink Stateflow","Semantics of Simulink Stateflow"],"dc:title":["Translation of Simulink-Stateflow models to hybrid automata"],"thesis:degree_discipline":["Electrical & Computer Engr"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:26Z"}