Verifying distributed real-time properties of embedded systems via graph transformations and model checking |
| |
Authors: | Gabor Madl Sherif Abdelwahed Douglas C Schmidt |
| |
Affiliation: | (1) Institute for Software Integrated Systems, Vanderbilt University, Nashville, TN, 37205;(2) Center for Embedded Computer Systems, University of California, Irvine, CA, 92697 |
| |
Abstract: | Component middleware provides dependable and efficient platforms that support key functional, and quality of service (QoS)
needs of distributed real-time embedded (DRE) systems. Component middleware, however, also introduces challenges for DRE system
developers, such as evaluating the predictability of DRE system behavior, and choosing the right design alternatives before
committing to a specific platform or platform configuration. Model-based technologies help address these issues by enabling
design-time analysis, and providing the means to automate the development, deployment, configuration, and integration of component-based
DRE systems. To this end, this paper applies model checking techniques to DRE design models using model transformations to
verify key QoS properties of component-based DRE systems developed using Real-time CORBA. We introduce a formal semantic domain
for a general class of DRE systems that enables the verification of distributed non-preemptive real-time scheduling. Our results
show that model-based techniques enable design-time analysis of timed properties and can be applied to effectively predict,
simulate, and verify the event-driven behavior of component-based DRE systems.
This research was supported by the NSF Grants CCR-0225610 and ACI-0204028
Gabor Madl is a Ph.D. student and a graduate student researcher at the Center for Embedded Computer Systems at the University of California,
Irvine. His advisor is Nikil Dutt. His research interests include the formal verification, optimization, component-based composition,
and QoS management of distributed real-time embedded systems. He received his M.S. in computer science from Vanderbilt University
and in computer engineering from the Budapest University of Technology and Economics.
Dr. Sherif Abdelwahed received his Ph.D. degree in Electrical and Computer Engineering from the University of Toronto, Canada, in 2001. During
2000–2001, he was a research scientist with the system diagnosis group at the Rockwell Scientific Company. Since 2001 he has
been with the Department of Electrical Engineering and Computer Science at Vanderbilt University as a Research Assistant Professor.
His research interests include verification and control of distributed real-time systems, and model-based diagnosis of discrete-event
and hybrid systems.
Dr. Douglas C. Schmidt is a Professor of Computer Science, Associate Chair of the Computer Science and Engineering program, and a Senior Researcher
in the Institute for Software Integrated Systems (ISIS) all at Vanderbilt University. He has published over 300 technical
papers and 6 books that cover a range of research topics, including patterns, optimization techniques, and empirical analyses
of software frameworks and domain-specific modeling environments that facilitate the development of distributed real-time
and embedded (DRE) middleware and applications. Dr. Schmidt has served as a Deputy Office Director and a Program Manager at
DARPA, where he lead the national R&D effort on middleware for DRE systems. In addition to his academic research and government
service, Dr. Schmidt has over fifteen years of experience leading the development of ACE, TAO, CIAO, and CoSMIC, which are
widely used, open-source DRE middleware frameworks and model-driven tools that contain a rich set of components and domain-specific
languages that implement patterns and product-line architectures for high-performance DRE systems. |
| |
Keywords: | Schedulability analysis Model checking Component middleware Distributed real-time Embedded systems |
本文献已被 SpringerLink 等数据库收录! |
|