Title page for ETD etd-11102012-171915

Type of Document Dissertation
Author Lu, Zheng
Author's Email Address zlu5@tigers.lsu.edu
URN etd-11102012-171915
Title Deductive Formal Verification of Embedded Systems
Degree Doctor of Philosophy (Ph.D.)
Department Computer Science
Advisory Committee
Advisor Name Title
Mukhopadhyay, Supratik Committee Chair
Busch, Konstantin Committee Member
Chen, Jianhua Committee Member
Nguyen, Phuc Committee Member
  • Coq
  • Static Code Analysis
  • Theorem Proving
  • Android
  • Formal Verification
  • SMT
Date of Defense 2012-11-08
Availability unrestricted
We combine static analysis techniques with model-based deductive verification using SMT solvers to provide a framework that, given an analysis aspect of the source code, automatically generates an analyzer capable of inferring information about that aspect.

The analyzer is generated by translating the collecting semantics of a program to a formula in first order logic over multiple underlying theories. We import the semantics of the API invocations as first order logic assertions. These assertions constitute the models used by the analyzer. Logical specification of the desired program behavior is incorporated as a first order logic formula. An SMT-LIB solver treats the combined formula as a constraint and solves it. The solved form can be used to identify logical and security errors in embedded programs. We have used this framework to analyze Android applications and MATLAB code.

We also report the formal verification of the conformance of the open source Netgear WNR3500L wireless router firmware implementation to the RFC 2131. Formal verification of a software system is essential for its deployment in mission-critical environments. The specifications for the development of routers are provided by RFCs that are only described informally in English. It is prudential to ensure that a router firmware conforms to its corresponding RFC before it can be deployed for managing mission-critical networks. The formal verification process demonstrates the usefulness of inductive types and higher-order logic in software certification.

  Filename       Size       Approximate Download Time (Hours:Minutes:Seconds) 
 28.8 Modem   56K Modem   ISDN (64 Kb)   ISDN (128 Kb)   Higher-speed Access 
  Lu_Diss.pdf 767.59 Kb 00:03:33 00:01:49 00:01:35 00:00:47 00:00:04

Browse All Available ETDs by ( Author | Department )

If you have questions or technical problems, please Contact LSU-ETD Support.