Formal frameworks for protocol behavior in mobile and embedded systems

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.