Show simple item record

dc.contributor.authorWaez, MD Tawhid Binen
dc.date2015-09-24 23:23:22.625
dc.date.accessioned2015-09-26T16:43:00Z
dc.date.available2015-09-26T16:43:00Z
dc.date.issued2015-09-26
dc.identifier.urihttp://hdl.handle.net/1974/13686
dc.descriptionThesis (Ph.D, Computing) -- Queen's University, 2015-09-24 23:23:22.625en
dc.description.abstractIntroducing automated formal methods for large industrial real-time systems is an important research challenge. We propose timed process automata for modeling and analysis of time-critical systems which can be open, hierarchical, and dynamic. The model offers two essential features for large industrial systems: (i) compositional modeling with reusable designs for different contexts, and (ii) automated state-space reduction technique. Timed process automata model dynamic networks of continuous-time communicating control processes which can activate other processes. We show how to automatically establish safety and reachability properties of timed process automata by reduction to solving timed games. To mitigate the state-space explosion problem, an automated state-space reduction technique using compositional reasoning and aggressive abstractions is also proposed. Before working on timed process automata, we did a survey on semantics, decision problems, variants, and tools of timed automata. The insights gained from this survey motivated us to use timed game theory and Uppaal Tiga in a couple of industrial case studies and the development of timed process automata. Both the case studies show that state-space explosion is a severe problem for timed games. Suitable abstractions, however, dramatically improve the scalability of timed games in one case study. These case studies motivate the development of timed process automata and an automatable state-space reduction technique for them based on aggressive abstraction.en
dc.language.isoengen
dc.relation.ispartofseriesCanadian thesesen
dc.rightsQueen's University's Thesis/Dissertation Non-Exclusive License for Deposit to QSpace and Library and Archives Canadaen
dc.rightsProQuest PhD and Master's Theses International Dissemination Agreementen
dc.rightsIntellectual Property Guidelines at Queen's Universityen
dc.rightsCopying and Preserving Your Thesisen
dc.rightsCreative Commons - Attribution - CC BYen
dc.rightsThis publication is made available by the authority of the copyright owner solely for the purpose of private study and research and may not be copied or reproduced except as permitted by the copyright laws without written authority from the copyright owner.en
dc.subjectHierarchical Systemsen
dc.subjectModel-Based Developmenten
dc.subjectOpen Systemsen
dc.subjectAutomotive Systemsen
dc.subjectState-Space Reductionen
dc.subjectSurveyen
dc.subjectCompositional Analysisen
dc.subjectTimed Automataen
dc.subjectCompositional Modelingen
dc.subjectCase Studyen
dc.subjectGame Theoryen
dc.subjectTimed Gamesen
dc.subjectTimed Process Automataen
dc.subjectReal-Time Systemsen
dc.titleA Model for Hierarchical Open Real-Time Systemsen
dc.typethesisen
dc.description.degreePhDen
dc.contributor.supervisorDingel, Juergenen
dc.contributor.supervisorRudie, Karenen
dc.contributor.departmentComputingen
dc.degree.grantorQueen's University at Kingstonen


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record