A Caltech Library Service

Analysis-Aware Design of Embedded Systems Software


Florian, Mihai (2014) Analysis-Aware Design of Embedded Systems Software. Dissertation (Ph.D.), California Institute of Technology. doi:10.7907/VB1N-Y042.


In the past many different methodologies have been devised to support software development and different sets of methodologies have been developed to support the analysis of software artefacts. We have identified this mismatch as one of the causes of the poor reliability of embedded systems software. The issue with software development styles is that they are ``analysis-agnostic.'' They do not try to structure the code in a way that lends itself to analysis. The analysis is usually applied post-mortem after the software was developed and it requires a large amount of effort. The issue with software analysis methodologies is that they do not exploit available information about the system being analyzed.

In this thesis we address the above issues by developing a new methodology, called "analysis-aware" design, that links software development styles with the capabilities of analysis tools. This methodology forms the basis of a framework for interactive software development. The framework consists of an executable specification language and a set of analysis tools based on static analysis, testing, and model checking. The language enforces an analysis-friendly code structure and offers primitives that allow users to implement their own testers and model checkers directly in the language. We introduce a new approach to static analysis that takes advantage of the capabilities of a rule-based engine. We have applied the analysis-aware methodology to the development of a smart home application.

Item Type:Thesis (Dissertation (Ph.D.))
Subject Keywords:analysis-aware design, programming languages design, specifications, static analysis, testing, model checking
Degree Grantor:California Institute of Technology
Division:Engineering and Applied Science
Major Option:Computer Science
Thesis Availability:Public (worldwide access)
Research Advisor(s):
  • Holzmann, Gerard J.
Thesis Committee:
  • Chandy, K. Mani (chair)
  • Holzmann, Gerard J.
  • Murray, Richard M.
  • Havelund, Klaus
  • Joshi, Rajeev
Defense Date:18 October 2013
Funding AgencyGrant Number
Record Number:CaltechTHESIS:10142013-111401153
Persistent URL:
Default Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:7990
Deposited By: Mihai Florian
Deposited On:27 Feb 2014 18:21
Last Modified:04 Oct 2019 00:02

Thesis Files

PDF - Final Version
See Usage Policy.


Repository Staff Only: item control page