| Descript |
222 p |
| Note |
Source: Dissertation Abstracts International, Volume: 70-07, Section: B, page: 4296 |
|
Adviser: Nikil D. Dutt |
|
Thesis (Ph.D.)--University of California, Irvine, 2009 |
|
As embedded systems become increasingly networked, and interact with the physical world, Distributed Real-time Embedded (DRE) systems emerge. DRE systems range from small-scale Multi-processor Systems-on-Chip (MPSoCs) operating in resource constrained environments such as cell phone platforms, medical devices and sensor networks all the way to large-scale software-intensive systems of systems used in avionics, ship computing environments, and in supervisory control and data acquisition systems managing regional power grids |
|
This dissertation focuses on the model-based analysis of event-driven DRE systems. Event-driven DRE systems are based on a reactive communication paradigm, where the execution of tasks is triggered asynchronously, invoked by external events, interrupts, or by other tasks. Events can also express time, providing a common semantic domain for the compositional analysis of time- and event-driven DRE systems |
|
Key technical contributions of this dissertation are (1) the specification of a formal semantic domain for DRE systems, (2) a model checking method for the real-time verification of non-preemptive DRE systems by timed automata, (3) a performance estimation method for DRE systems by discrete event simulations, (4) a conservative approximation method for the verification of preemptive event-driven asynchronous DRE systems by timed automata, (5) a method for the functional verification and performance estimation of 1VIPSoCs built on an industry standard MPSoC interconnect protocol, and (6) a cross-abstraction real-time analysis method for MPSoC designs utilizing bus matrix interconnects |
|
The novelty of our approach lies in combining formal methods and symbolic simulations for the system-level evaluation of DRE designs early in the design flow, and utilizing multiple abstractions to trade off analysis accuracy in scalability |
|
We implemented the proposed analysis methods in the open-source Distributed Real-time Embedded Analysis Method (DREAM) framework for the model-based real-time verification and performance estimation of DRE systems. DREAM focuses on the practical application of formal analysis methods to automate the verification, development, configuration, and integration of event-driven DRE systems. DREAM is available for download at http://dre.sourceforge.net. We applied the proposed design flow to the domain of software-intensive mission-critical avionics DRE applications, and the domain of multimedia MPSoCs |
|
School code: 0030 |
| Host Item |
Dissertation Abstracts International 70-07B
|
| Subject |
Computer Science
|
|
0984
|
| Alt Author |
University of California, Irvine
|
|
