John Hatcliff spoke at this morning's BYU Computer Science colloquium. John is a professor of Computer Science at Kansas State University. He's speaking on Model-driven development, analysis, and optimization in a system called Cadena.
The project is based on using middleware to form abstractions of distriburted computing components. The talk is focused on a real-time CORBA event service. The "model-driven" portion of the talk discusses formalisms for building high-assurance distributed systems. The framework supports plugging in various light-weight specification, analysis, and verification systems.
The work was done in the context of an avionics mission control system project sponsored by DARPA through Boeing. In a typical situation, a component, A, computes some data that is read by other components (B1, B2, etc.). A publishes a dataAvailable event and then Bk calls a getData method on A to fetch the data. Bk may or may not fetch the data from A depending on its state.
The Boeing challenge problems included things like calculating forward and backward data dependence and trace the parts of the system influenced by data produced by a particular component (architectural slicing). Boeing had heuristics about priorities that various tasks had to run at depending on the dependencies and couplings. Other issues included dependency interactions.
Here's a specific problem: If components 1 is in mode A when component 2 produces an event E, when will component 3 consume data F? This is a classic model checking problem.
Cadena is an Eclipse plugin that provides support for analysis of middleware architectures, specifically, the CORBA component model (CCM). This analysis can solve specific problems like the one above and other's that Boeing was interested in.
Components can have synchronous and asynchronous connections to each other. Cadena uses CORBA IDL to describe these interfaces. Code templates are automatically generated that can be filled in with the business logic. This is completely integrated in Eclipse and uses the Eclipse Java facilities.
Cadena provides a graphical, spreadsheet, and textual view of how components are connected together. These all operate from the same model, so that changing any one updates all three. Cadena provides tools within the graphical view that do graphical analysis of the overall system including forward and backward slicing, cycle checking, and so on. The spreadsheet view allows components to be filtered and sorted for managing large numbers of components. Pulldown menus include only type-safe choice for component connections.
Configuration and deployment information (in XML) is automatically generated so that components can be assembled on specific network nodes.
Cadena requires engineers to annotate the CORBA IDL with some semantic information so that model checking can analyze the design. This information includes, in order of increasing effort and strength of verification, port action dependencies, state-based dependencies, and component transition semantics. This is a nice iterative approach to getting semantic specification from engineers since they can see real results from easy actions and understand that adding more semantic information will increase the level of analysis they can do. The tool also can check that the semantic specification tracks through to the Java code.
One of the goals was to simplify the view of the system topology by hiding components and connections based on the mode the system is in. The tool can automatically generate these views. In the graphical view, changing the mode of a particular component simplifies the view to show just the components and connections that will be active in that mode.
This talk was an interesting intersection of two things that have held great interest for me in my professional life: formal methods and distributed component-based architectures. Its surprising to me that there aren't more tools for analyzing component-based architectures (and service-based architectures) given the modularity of those designs. Cadena shows that this type of analysis is both possible and beneficial.
