Analysis and Verification of Cyber-Physical System Software Using Static Analysis
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.
This item appears in the following collection(s):
Showing items related by title, author, creator and subject.
Statistical Methods for the Analysis of Error-Prone Electronic Health Records: Impact of Source Data Verification, Time Discretized Multiple Imputation, and Variance Estimation with Incompatible Imputation and Analysis Models Giganti, Mark Joseph (2018-08-29)Department: BiostatisticsObservational data from electronic health records (EHRs) are prone to errors which are often correlated across multiple variables. One strategy to assess EHR data quality is to compare the research study data to the original ...
Seed-based correlation analysis and instantaneous global correlation analysis for resting state fMRI Bell, Charreau Sieanna (2018-04-12)Department: Electrical EngineeringBrain disorders have an increasingly poignant socioeconomic impact, and persons with mental illness and mental disorders, Alzheimer's disease, dementia, Parkinson's disease, and epilepsy are intensely affected by these ...
Thomas, Randall S., 1955-; Schwab, Stewart J. (Washington & Lee Law Review, 2006)In this paper, we examine the key legal characteristics of 375 employment contracts between some of the largest 1500 public corporations and their Chief Executive Officers. We look at the actual language of these contracts, ...