Middleware Models
The first major contribution of this research has been the development a new set of models for the timing and event semantics of reusable middleware abstractions found in the widely used ACE framework. These models are based on timed automata and can be used within timed model checking tools such as the IF toolkit and UPPAAL to verify safety and timing properties of a system, including the middleware platform on which the system is deployed.The architecture diagram below depicts the different models we have developed, and how they cover different parts of the ACE architecture. In this figure, unshaded rectangles in the diagram represent models expressed directly as timed automata, while shaded rectangles represent models expressed as data structures that are shared among the automata:
Model Refinements
The second major contribution of this research has been the identification and application of model refinements that are specific to the middleware domain from which out models are derived, but also are generally valid across a variety of applications using such middleware. These refinements both more accurately reflect the semantics of the middleware domain, and also in several cases reduce the amount of state space exploration that must be performed in checking the models.
Modeling Threads
The first such refinement was to model threads of control flowing concurrently through multiple objects as chains of object method invocations are performed, a feature that is not provided by existing model checkers for timed automata. The following figure shows a flow of control from one object to another object (Foo1 to Foo2, Bar1 to Bar2), with both of these objects modeled as timed automata. To model a distinct thread flow of control, we added a thread id that is maintained by each automaton, which serves as a unique reference to the thread whose execution it represents.
Modeling Priority Scheduling
The second refinement was to model the prioritization of threads of control that is used in many real-time systems (e.g., to enforce a rate monotonic scheduling policy efficiently). The following figure shows how a model checker's ability to enforce specified priority rules can be used to ensure the execution of automaton transitions in the models adheres to the prioritization of threads in the actual system.
Modeling Run-to-Completion Semantics
The third refinement was to model run-to-completion semantics among threads with the same thread priority (e.g., under the SCHED_FIFO policy in Linux and other operating systems), a widely used feature of real-time systems. To achieve this, we added a global thread identifier to track which thread is currently executing. This allows us to specify another model checker priority rule which will ensure the current thread continues executing unless a higher priority thread becomes eligible to run. The following figure illustrates this semantics.
However, simply maintaining a current thread identifier and continuing the execution of the automaton whose thread is current may accidentally over-constrain the model by eliminating concurrent execution that is possible in the actual system. The left side of the following figure illustrates this problem. We therefore refined the run-to-completion semantics further by adding a low priority automaton that only runs when the automata modeling threads are idle. As the right side of the following figure illustrates, this "idle catcher" automaton sets the current thread id back to nil, ensuring non-deterministic choice of the next thread to be run after an idle interval.
Verification Studies
The third major contribution of this research has been to demonstrate the use of our models in verifying properties of specific applications and protocols based on the middleware abstractions we have modeled.As a representative example of verification scenarios for ACE-based applications, we used our models to verify a version of the Gateway example that is distributed with ACE, in which notification of event delivery establishes a potential for deadlock. We used model checking in the IF toolkit to explore the effects of alternative event dispatching strategies for the ACE Reactor ("wait-on-connection" in which remote method invocations block in the calling object until the reply is received, versus "wait-on-reactor" in which the thread of execution making the call is returned to the reactor and the reply is handled asynchronously) in that example.
The following figure illustrates the results of those studies, which demonstrate the use of our models in detecting timing and concurrency hazards in non-trivial software systems. The left side of the figure shows an event sequence in which a deadlock occurs with the "wait-on-connection" strategy, which was detected automatically by the IF model checker using our models. With the "wait-on-reactor" strategy, model checking verified deadlock freedom, as one representative trace shown on the right side of the figure below illustrates.
Wait-on-Connection Strategy | Wait-on-Reactor Strategy |
 |  |
Because of the lower complexity (and accordingly lower overhead) of the "wait-on-connection" strategy, we have been collaborating with Cesar Sanchez, Henny Sipma, and Zohar Manna at Stanford University who are working to develop a suite of deadlock avoidance protocols that can overcome the potential for deadlock hazards noted above for the "wait-on-connection" strategy. We have implemented the simplest of these protocols, called the BASIC-P protocol, in ACE's thread pool reactor, and have developed timed automata models of the protocol operating within the reactor. We are also working to implement and model the other protocols in this family to offer applications having different characteristics and requirements a range of flexible and verifiable options. The following figure shows a comparison of the execution traces produced by checking the models, and by running the same example using our implementation in ACE.
