Software designs and specifications often describe how the resultant code is suppose to behave. Software model checking and related activities statically investigate software behavior to ensure that it meets a particular specification. We have developed a tool that uses model checking techniques to do large-scale checking of dynamic specifications in real Java systems. The tool starts with a finite state specification of the properties to check in terms of abstract events. It first finds all instances in the Java system where this specification is applicable. For each such instance, it creates an abstract model of the software with respect to the events and then checks this model against the specification. In addition to testing if the condition is guaranteed to hold or to fail, the system also provides the information needed to do run time checking of the specification.

Bio:
Steven Reiss is Professor of Computer Science at Brown University where he has been on the faculty since 1977. His research interests and expertise lie in the area of programming environments and software visualization. His previous programming environments include PECAN, GARDEN, FIELD, DESERT, and BLOOM. FIELD pioneered the concept of message-based (control) integration, illustrated a variety of program visualizations, and served as the basis for HP's Softbench, Sun's Tooltalk and DEC's FUSE environments. The most recent environment, BLOOM, provides a practical approach to software visualization, letting the user define new, high-quality visualizations of static and dynamic data in a matter of minutes.

Current research being undertaken by Dr. Reiss includes the visualization and analysis of the dynamics of complex software systems, using constraints to integrate the various artifacts associated with a software system, checking dynamic properties of software, and the development of an environment to support the notion of a single dynamic programming running on all machines and doing everything.