Analysis and Verification of Cyber-Physical System Software Using Static Analysis

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.