Login | Register

Formal analysis of fault tolerant real time multiprocessor allocation and scheduling protocols


Formal analysis of fault tolerant real time multiprocessor allocation and scheduling protocols

Varma, Nikhil Kumar (2004) Formal analysis of fault tolerant real time multiprocessor allocation and scheduling protocols. Masters thesis, Concordia University.

Text (application/pdf)
MQ94714.pdf - Accepted Version


Dependable real-time distributed systems rely on allocation and scheduling protocols to satisfy stringent resource and timing constraints. As these protocols have both dependability and real-time attributes, verification of such composite services warrants a rigorous and formal levels of assurance for their correctness. The wide acceptance of formal techniques in the design and development of dependable real-time systems is limited because, most of these formal theories for real-time scheduling have been developed without much regard for their further reuse. This makes the formal specifications and their proof constructs in general difficult to reuse, and to verify or analyze similar or related protocols. To expand the utility of formal techniques, this thesis explores the possibility of effectively defining and then reusing formal theories in order to simplify verification and analysis for a wide spectrum of dependable real-time protocols. We present a modular formal analysis of a fault-tolerant version of a real-time task allocation and scheduling policies. The main aim is to develop a library of formal theories for the identified modules for real-time and dependable services which could be systematically, and if required, repeatedly used to develop different and new composite dependable multiprocessor real-time allocation and scheduling protocols. We demonstrate a rigorous and tool-assisted formal analysis of three multiprocessor real time fault tolerant allocation and scheduling protocols for both periodic and aperiodic task models using the concept of reuasability of previously defined theories. We show the reduced effort in the analysis and verification process by reusing the previously formalized theories. Formal analyses of these protocols have been performed using a mechanized theorem proving environment, called PVS from SRI labs.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (Masters)
Authors:Varma, Nikhil Kumar
Pagination:x, 98 leaves : ill. ; 29 cm.
Institution:Concordia University
Degree Name:M.A. Sc.
Program:Electrical and Computer Engineering
Thesis Supervisor(s):Sinha, Purnendu
ID Code:8084
Deposited By: Concordia University Library
Deposited On:18 Aug 2011 18:14
Last Modified:18 Jan 2018 17:32
Related URLs:
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Back to top Back to top