• About
    • Login
    View Item 
    •   Institutional Repository Home
    • Electronic Theses and Dissertations
    • Electronic Theses and Dissertations
    • View Item
    •   Institutional Repository Home
    • Electronic Theses and Dissertations
    • Electronic Theses and Dissertations
    • View Item
    JavaScript is disabled for your browser. Some features of this site may not work without it.

    Browse

    All of Institutional RepositoryCommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects

    My Account

    LoginRegister

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

    Zhang, Zhenkai
    : https://etd.library.vanderbilt.edu/etd-10192015-105546
    http://hdl.handle.net/1803/14342
    : 2015-10-20

    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.
    Show full item record

    Files in this item

    Icon
    Name:
    Zhang.pdf
    Size:
    1.935Mb
    Format:
    PDF
    View/Open

    This item appears in the following collection(s):

    • Electronic Theses and Dissertations

    Related items

    Showing items related by title, author, creator and subject.

    • Seed-based correlation analysis and instantaneous global correlation analysis for resting state fMRI 
      Bell, Charreau Sieanna (2018-04-12)
      Brain 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 ...
    • 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)
      Observational 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 ...
    • Finite-Element Analysis of Low-Power Laser Heating in Gold::Vanadium Dioxide Nanocomposites 
      MacQuarrie, Evan (Vanderbilt University. Dept. of Physics and Astronomy, 2011-04)
      Finite element modeling was performed using COMSOL Multiphysics to study the thermal dynamics of gold::vanadium dioxide (VO$_{2}$) nanocomposites.  These simulations were done to understand the data from transient ...

    Connect with Vanderbilt Libraries

    Your Vanderbilt

    • Alumni
    • Current Students
    • Faculty & Staff
    • International Students
    • Media
    • Parents & Family
    • Prospective Students
    • Researchers
    • Sports Fans
    • Visitors & Neighbors

    Support the Jean and Alexander Heard Libraries

    Support the Library...Give Now

    Gifts to the Libraries support the learning and research needs of the entire Vanderbilt community. Learn more about giving to the Libraries.

    Become a Friend of the Libraries

    Quick Links

    • Hours
    • About
    • Employment
    • Staff Directory
    • Accessibility Services
    • Contact
    • Vanderbilt Home
    • Privacy Policy