LEADER 00000nam  2200349   4500 
001    AAI3364975 
005    20101121142138.5 
008    101121s2009    ||||||||||||||||| ||eng d 
020    9781109249729 
035    (UMI)AAI3364975 
040    UMI|cUMI 
100 1  Madl, Gabor 
245 10 Model-based analysis of event-driven distributed real-time
       embedded systems 
300    222 p 
500    Source: Dissertation Abstracts International, Volume: 70-
       07, Section: B, page: 4296 
500    Adviser: Nikil D. Dutt 
502    Thesis (Ph.D.)--University of California, Irvine, 2009 
520    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 
520    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 
520    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 
520    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 
520    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 
590    School code: 0030 
650  4 Computer Science 
690    0984 
710 2  University of California, Irvine 
773 0  |tDissertation Abstracts International|g70-07B 
856 40 |uhttp://pqdd.sinica.edu.tw/twdaoapp/servlet/
       advanced?query=3364975