Timed Automata Models for Principled Composition of ACE Mechanisms
Introduction
Middleware for Distributed Real-time Embedded (DRE) systems has grown
more and more complex in recent years due to the varying functional
and temporal requirements of complex real-time applications. To enable
DRE middleware to be configured and customized to meet the demands of
different applications, a body of ongoing research has focused on
applying model-driven development techniques to developing QoS-enabled
middleware.
While current approaches for modeling middleware focus on easing the
task of assembling, deploying and configuring middleware and
middleware-based applications, a more formal basis for correct
middleware composition and configuration in the context of individual
applications is needed. While the modeling community has used
application-level formal models that are more abstract to uncover
certain flaws in system design, a more fundamental and lower-level set
of models is needed to be able to uncover more subtle safety and
timing errors introduced by interference between application
computations, particularly in the face of alternative concurrency
strategies in the middleware layer.
Modeling Approach
In this research, we examine how detailed formal models of lower-level
middleware building blocks as that found in ACE provide an appropriate
level of abstraction both for modeling and synthesis of a variety of
kinds of middleware from these building blocks. When combined with
model checking techniques, these formal models can help developers in
composing correct combinations of middleware mechanisms, and
configuring those mechanisms for each particular application.
Our models are executable models and can be model checked for
constraint violations, at which time a trace is produced by the model
checker as to what sequence of events led to the constraint
violation. This research has produced a modeling architecture for
modeling middleware infrastructure elements. We have realized this
architecture using the UPPAAL and IF
toolkit. We have also identified a number of state optimization
techniques that make model checking more tractable.
This research thus impacts two different research communities. First,
by modeling well-known low-level middleware abstractions such as
reactors, acceptors, connectors, and service handlers, this work
establishes concrete, canonical reference models for use by the formal
systems modeling community. Second, by using those low-level models
to evaluate particular concurrency and communication strategies in
current use, this work increases the rigor of current analysis and
checking approaches used by higher-level model-based middleware
development techniques.
Software
Our IF based models can be obtained from here. Our UPPAAL based models can be
obtained from here.
Papers
Venkita Subramonian, Christopher Gill, Cesar Sanchez and Henny Sipma,
Composable Models for Timing and Liveness Analysis in Distributed
Real-Time Embedded Systems,Washington University Technical Report
WUCSE-2005-54.
Venkita Subramonian, Christopher Gill, Cesar Sanchez and Henny Sipma,
Composable Time Automata Models for Real-Time Embedded Systems Middleware
,Washington University Technical Report
WUCSE-2005-29.
Cesar Sanchez, Henny Sipma, Zohar Manna, Venkita Subramonian, and
Christopher Gill,
On
Efficient
Distributed Deadlock Avoidance for Real-Time and Embedded Systems,
IPDPS '06, April 25 - 29, 2006, Rhodes Island, Greece
Cesar Sanchez, Henny Sipma, Venkita Subramonian and Christopher Gill,
Thread
Allocation Protocols for Distributed Real-Time and Embedded
Systems, 25th IFIP WG 6.1 International Conference on Formal
Techniques for Networked and Distributed Systems, Taipei, Taiwan,
October 2-5, 2005
Venkita Subramonian and Christopher Gill, A
Generative Programming Framework for Adaptive Middleware, Hawai'i International Conference on
System Sciences, January 2005