Date of Award
8-2010
Document Type
Thesis
Degree Name
Master of Science (MS)
Legacy Department
Computer Science
Committee Chair/Advisor
Hallstrom, Jason O
Committee Member
Sitaraman , Murali
Committee Member
Malloy , Brian
Abstract
Embedded networked devices are required to produce dependable outputs and communicate with peer devices given limited computing resources. These devices monitor and control processes within the physical world. They are used in applications related to environmental monitoring, telecommunications, social networking, and also life-critical applications in domains such as health care, aeronautics, and automotive manufacturing. For such applications, software errors can be costly - both in terms of nancial and human costs. Therefore, software programs installed on these devices must meet the appropriate requirements. To guarantee this, one must verify that the implemented code meets the corresponding specications. Manual trial-and-error validation of such applications, especially life-critical software programs, is not a feasible option.
This work presents a verifying compiler developed for embedded network programs by extending the RESOLVE verifying compiler with a software module that translates RESOLVE code to equivalent C code. Specications and implementations for embedded networked applications are written in the RESOLVE language. The compiler supports automated verication, automatically generating mathematical assertions, which, if satised, ensure that the code is correct. These assertions are proved using the mathematical theorems and lemmas provided by the RESOLVE
mathematical library. The veried code is then translated to C and installed on the embedded target.
The contributions described in this thesis are: (i) We explore the use of RESOLVE in specifying pin-level drivers for components of an embedded device. (ii) We describe the translation strategies implemented to generate correct-by-construction C source code from verified RESOLVE code, with examples of basic and reusable operations such as sense data, broadcast data, and receive
data. (iii) We provide techniques used to optimize the generated code in terms of memory usage and runtime eciency.
Recommended Citation
Regula, Kalyan chakradhar, "A Verifying Compiler for Embedded Networked Systems" (2010). All Theses. 899.
https://tigerprints.clemson.edu/all_theses/899