A Model for Hierarchical Open Real-Time Systems
Waez, MD Tawhid Bin
MetadataShow full item record
Introducing 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.
URI for this recordhttp://hdl.handle.net/1974/13686
Request an alternative formatIf you require this document in an alternate, accessible format, please contact the Queen's Adaptive Technology Centre
Showing items related by title, author, creator and subject.
Comparison of a Newly Proposed Staging System with 7th Edition AJCC/UICC System for Surgically Resected Patients with Intrahepatic Cholangiocarcinoma Aktar, SuriyaBackground: Intrahepatic cholangiocarcinoma (IHCC) is a rare but lethal primary liver cancer. Debate exists about whether tumor size should be considered in disease staging. This study aimed to examine the association ...
A Parallel-Series Two Bridge DC/DC Converter for PV Power Conditioning Systems Used in Hybrid Renewable Energy Systems Servansing, Amish Ansuman (2012-04-19)This thesis presents a parallel-series two-bridge DC/DC converter topology with the ability to operate with ZVS over a wide input and load range. The intended application is power conditioning systems (PCS) of photovoltaic ...
Estimation and Effects of Imperfect System Parameters on the Performance of Multi-Relay Cooperative Communications Systems Mehrpouyan, Hani (2012-09-17)To date the majority of research in the area of cooperative communications focuses on maximizing throughput and reliability while assuming perfect channel state information (CSI) and synchronization. This thesis, seeks to ...