A joint project of the Graduate School, Peabody College, and the Jean & Alexander Heard Library

Title page for ETD etd-10192015-105546


Type of Document Dissertation
Author Zhang, Zhenkai
Author's Email Address zhenkai.zhang@vanderbilt.edu
URN etd-10192015-105546
Title Analysis and Verification of Cyber-Physical System Software Using Static Analysis
Degree PhD
Department Computer Science
Advisory Committee
Advisor Name Title
Xenofon D. Koutsoukos Committee Chair
Akos Ledeczi Committee Member
Gabor Karsai Committee Member
Janos Sztipanovits Committee Member
William H. Robinson Committee Member
Keywords
  • value analysis
  • WCET analysis
  • CPS software
  • static analysis
Date of Defense 2015-08-27
Availability unrestricted
Abstract
Cyber-Physical Systems (CPS) are complex systems which involve tight interactions between physical dynamics, computational platforms, communication networks, and embedded software. The complex interactions prevent us from formally analyzing and verifying the whole system. However, since most of the CPS are safety-critical systems, sufficient analysis of important system properties is necessary. Since the most error-prone part is software, this thesis focuses on how to analyze and verify CPS software using static analysis. Both functional and non-functional properties are considered.

In the case of functional properties, the thesis focuses on how to use value-set analysis (VSA) for binaries in different instruction set architectures (ISA). To this end, a set of intermediate instructions with a straightforward concrete semantics to encode the instructions of different ISA is defined. The work extends the strided-interval abstract domain used in VSA and defines a set of operations on the extended domain. The work also defines an abstract semantics for the intermediate instructions in the value-set abstract domain to facilitate any VSA program writing. Examples show the feasibility of the generic VSA approach, which is to precisely resolve indirect branch target addresses.

In the case of non-functional properties, the thesis focuses on how to derive the execution time information of a task running on a single-core processor. Since caches have the most impact on the variation of execution time, the work mainly concentrates on how to safely and precisely estimate the worst-case execution time (WCET) in the presence of single-level and multi-level caches. In order to tighten the WCET estimation when there are many loops, the work first studies the sources of pessimism of single-level cache persistence analysis and then proposes two methods to improve the analysis precision. Since many modern processor are also equipped with multi-level caches, the work also proposes two approaches to improve the precision of the WCET estimation in the presence of inclusive cache hierarchies. The proposed methods are proven safe, and evaluations show all the methods can tighten the WCET estimation. Moreover, the thesis also investigates how to bound the cache-related preemption delay for a task under a preemptive scheduling strategy.

Files
  Filename       Size       Approximate Download Time (Hours:Minutes:Seconds) 
 
 28.8 Modem   56K Modem   ISDN (64 Kb)   ISDN (128 Kb)   Higher-speed Access 
  Zhang.pdf 2.03 Mb 00:09:23 00:04:49 00:04:13 00:02:06 00:00:10

Browse All Available ETDs by ( Author | Department )

If you have more questions or technical problems, please Contact LITS.