"Analyzing Event-driven Component-based Designs"

Matt Dwyer, Kansas State University

Tuesday, April 22, 2003 at 10:00 A.M.

Room 506, CIT 5th Floor

The use of component models such as Enterprise Java Beans and the CORBA Component Model (CCM) in application development is expanding. Even in real-time safety/mission-critical domains, component-based development is beginning to take hold as a mechanism for incorporating non-functional aspects such as real-time, quality-of-service, and distribution. To form an effective basis for development of such systems, we believe that support for reasoning about correctness properties of component-based designs is essential.

In this talk, we present Cadena -- an integrated environment for building and modeling CCM systems. Cadena provides facilities for defining component types using CCM IDL, specifying dependency information and transition system semantics for these types, assembling systems from CCM components, visualizing various dependence relationships between components, specifying and verifying correctness properties of models of CCM systems derived from CCM IDL, component assembly information, and Cadena specifications, and producing CORBA stubs and skeletons implemented in Java. We are applying Cadena to avionics applications built using Boeing's Bold Stroke framework.

Presenter Bio: Matthew B. Dwyer is an Associate Professor in the Department of Computing and Information Sciences at Kansas State University. He co-directs work on the Bandera, Cadena and Bogor projects which are developing tool platforms for applying model checking techniques to software design notations and source code. Prior to joining Kansas State in 1995, he completed his PhD at the University of Massachusetts at Amherst; in his dissertation work he developed FLAVERS which applies program flow analysis techniques to reason about application specific safety properties. His interests in automated program analysis were kindled by his experiences as a Senior Engineer with Intermetrics. Inc. from 1985 through 1990. Matt learned most of what he knows about software by working on a variety of embedded system development projects, which were a rich source of subtle concurrency related bugs, and by developing a range of software tools, including source level debuggers, code generators, and the global optimizer for a family of C compilers. He learned most of what he knows about herding cats by serving as the program chair of the SPIN Software Model Checking Workshop in 2001 and the ACM Workshop on Program Analysis for Software Tools and Engineering in 2002; he will try to put that to good use as program chair for the ACM SIGSOFT Symposium on Foundations of Software Engineering in 2004.

Host: Shriram Krishnamurthi