Please use this identifier to cite or link to this item: http://hdl.handle.net/10603/4387
Title: Formal frameworks for protocol behavior in mobile and embedded systems
Researcher: Poroor, Jayaraj
Guide(s): Bharat, Jayaraman
Ramachandra, Kaimal
Keywords: Computer Science
mobile and embedded systems
Upload Date: 22-Aug-2012
University: Amrita Vishwa Vidyapeetham (University)
Completed Date: May 2012
Abstract: We investigate formal frameworks for de_ning and analyzing the behavior of network protocols in mobile and embedded systems. Such systems are typically networked for the purposes of remote monitoring and control. Hence understanding and analyzing their protocol behavior becomes important. Moreover, formal approaches are necessitated since such devices often perform safety-critical functions such as medical drug-delivery or automotive control. The protocol behavior in mobile and embedded systems are de_ned by the three distinct phases of their implementation, namely, speci_cation, construction, and embedded execution. Developing formal approaches covering these three phases are, therefore, important for establishing robust protocol behavior. Hence, the main contributions of the thesis are three-fold: (1) A new language _Z is introduced that o_ers a principled combination of mobile channels of the _-calculus and stateful abstract types of the Z language. We de_ne formal semantics of the _Z language and establish important properties of the semantics. The _Z language can be used for specifying a number of problems in mobile embedded systems and we illustrate its use with the speci_cation of the hidden node problem in wireless networks. (2) A novel veri_cation technique called split veri_cation is introduced for verifying security properties of protocol stacks constructed in a subset of C++. The split veri_cation is a strategy for verifying security properties wherein tactical operation-level properties are expressed as data re_nement conditions and veri_ed using theorem-proving and global control ow properties are expressed using temporal logic and veri_ed using model-checking. (3) A novel analysis method for the performance of protocol stacks, based on the notion of operation traces, is introduced for analyzing the performance of real-time protocol stacks under contention-based attacks. We also introduce metrics to evaluate the performance based on the operation trace concept.
Pagination: 115p.
URI: http://hdl.handle.net/10603/4387
Appears in Departments:Department of Computer Science and Engineering (Amrita School of Engineering)

Files in This Item:
File Description SizeFormat 
01_title.pdfAttached File258.69 kBAdobe PDFView/Open
02_certificate.pdf255.28 kBAdobe PDFView/Open
03_declaration.pdf21.86 kBAdobe PDFView/Open
04_dedication.pdf14.3 kBAdobe PDFView/Open
05_contents.pdf32.1 kBAdobe PDFView/Open
06_acknowledgements.pdf32.24 kBAdobe PDFView/Open
07_list of figures.pdf48.94 kBAdobe PDFView/Open
08_abstract.pdf30.58 kBAdobe PDFView/Open
09_chapter 1.pdf828.21 kBAdobe PDFView/Open
10_chapter 2.pdf146.83 kBAdobe PDFView/Open
11_chapter 3.pdf329.92 kBAdobe PDFView/Open
12_chapter 4.pdf199.15 kBAdobe PDFView/Open
13_chapter 5.pdf1.25 MBAdobe PDFView/Open
14_chapter 6.pdf41.16 kBAdobe PDFView/Open
15_bibliography.pdf74.8 kBAdobe PDFView/Open


Items in Shodhganga are protected by copyright, with all rights reserved, unless otherwise indicated.