Type of Document Dissertation Author Lu, Zheng Author's Email Address email@example.com 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 Keywords
- Static Code Analysis
- Theorem Proving
- Formal Verification
Date of Defense 2012-11-08 Availability unrestricted AbstractWe 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
If you have questions or technical problems, please Contact LSU-ETD Support.