Modelling and verification of predictable data flow in real-time systems
Loading...
Authors
Madzar, Boris
Date
2015-10-28
Type
thesis
Language
eng
Keyword
model checking , predictability , real-time operating systems , schedulability
Alternative Title
Abstract
As vehicle electronic control systems become responsible for an increasing number of functions, developers of such systems find themselves pulled in two directions: the need to perform more and more computation while at the same time reducing cost, weight and power consumption. Traditionally, safety isolation and fault containment of software tasks has been achieved through either physical or temporal segregation. This approach is reliable but inefficient in terms of processor utilization. Recently, there has been a move towards systems which achieve better processor utilization by executing all tasks together and guaranteeing safety isolation and fault containment by means of formal verification.
First, a definition for one such system was developed, based on PharOS and Giotto. The system modelled attempts to ensure observably deterministic data flow (i.e., inputs from and outputs to other systems), but allows for non-observable nondeterminism. It also allows for sporadic deadline overruns and accounts for criticality during fault handling.
Second, a method for verifying a given input system definition (system, set of tasks and fault model) for predictable data flow was developed. A stand-alone tool was made that performs this verification and displays the results graphically. The core exhaustive verification is performed by the Spin model checker.
Description
Thesis (Master, Computing) -- Queen's University, 2015-10-28 01:28:37.567
Citation
Publisher
License
Queen's University's Thesis/Dissertation Non-Exclusive License for Deposit to QSpace and Library and Archives Canada
ProQuest PhD and Master's Theses International Dissemination Agreement
Intellectual Property Guidelines at Queen's University
Copying and Preserving Your Thesis
This 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.
ProQuest PhD and Master's Theses International Dissemination Agreement
Intellectual Property Guidelines at Queen's University
Copying and Preserving Your Thesis
This 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.