20th IEEE/ACM International Conference on
Automated Software Engineering

Long Beach, California, USA, November 7-11, 2005

Model checking has proven to be an effective technology for verification and debugging in hardware and more recently in software domains. We believe that for model checking technology to be effectively applied to software, model checking tools must directly support language constructs found in modern object-oriented languages like Java and C# and underlying checking algorithms must make use of sophisticated analyses similar to those found in optimizing compilers to reduce model checking costs. Moreover, recent trends in both the requirements for software systems and the processes by which systems are developed suggest that domain-specific model checking engines may be more effective than general purpose model checking tools.

The Bogor model checking framework is an extensible and highly modular explicit-state model checking framework that aims to overcome limitations of existing model checking tools that fail to provide direct support modeling software, and to enable more effective incorporation of domain knowledge into verification models and associated model checking algorithms and optimizations.

This four hour tutorial will cover the following topics related to Bogor's design principles, graphical user interface and visualizations, internal architecture and APIs, working with architectural elements to create customized domain-specific model-checking engines, and example deployments of Bogor in large scale development/verification environments.

• Bogor Overview: An introduction to the challenges of model checking modern multi-threaded object-oriented systems, Bogor's overarching philosophy for addressing these challenges, and illustrations of the primary capabilities of Bogor via its Eclipse-based user interface
• Bogor Architecture -- Designing for OO Support and Extensibility: An overview of the internal architecture of Bogor focusing on its rationale for (a) supporting the complexities of checking highly dynamic concurrent object-oriented systems and (b) for enabling customization of core algorithms/representations and adding new constructs to Bogor's modeling language via the Bogor extension mechanism.
• Customizing Bogor -- Building Your Own Domain Specific Model Checker: Step-by-step illustrations of how to easily add new domain-specific commands/expressions to Bogor's modeling language and how to increase model checking effectiveness by tailoring Bogor's internal algorithms to the characteristics of a particular domain.
• Bogor Applications -- Bogor Deployed in Large-Scale Software Development Tools: Examples of how Bogor has been customized/extended to form the core model checking engine of several robust software development tools including the Cadena model-driven development environment for component-based real-time distributed systems, and the next generation of the Bandera tool set for model checking concurrent Java software. This will include a discussion of how a variety of forms of program analysis (including blends of static and dynamic alias and escape analysis) are used to drive state representation and state-space reduction strategies.

Bogor is freely distributed in an open-source format, and a variety of forms of supporting documentation and example repositories can be found on the project web-site http://bogor.projects.cis.ksu.edu.

The software engineering community increasingly recognizes the importance and value of dynamic analysis for program understanding. A dynamic analysis runs a program and observes its execution. Dynamic analysis for program understanding produces output, or feeds into a subsequent analysis, that enables programming tasks or increases human understanding of the code; this transcends traditional dynamic analysis for testing or optimization.

Dynamic analysis complements traditional static analyses, such as compilers and type checkers, that have similar goals. Once largely ignored by the research community due to unsoundness, of late there has been a flowering of research in this area. Often, a dynamic analysis is more precise and can better handle incomplete programs, programs written in multiple languages, and analysis of program environments, among other situations.

This tutorial will explore the active new area of program analysis for program understanding and software engineering. It will cover theoretical background, implementation techniques, and applications, with particular focus on applications to practical programming tasks and on developing new applications. It will also present tools that you can use or build on in your practice or research, with the opportunity for hands-on experience, if there is interest.

The tutorial format will encourage questions, discussion, and interaction, in order to enable participants to get the most out of it.

The objective of this tutorial is to introduce attendees to some new attitudes and conceptual tools for constructed complex system design, that we have found to be very helpful in modeling, analyzing, and understanding very large and complex systems. This tutorial will include a short guided session on how to use these techniques for system modeling, software design, and general system engineering and integration.

In Software Engineering, Component-based Development (CBD) is an important emerging topic, promising long sought after benefits like increased reuse and reduced time-to-market (and hence software production cost). However, there are at present many obstacles to overcome before CBD can succeed. For one thing, CBD success is predicated on a standardised market place for software components, which does not yet exist. In fact currently CBD even lacks a universally accepted terminology. Existing component models adopt different component definitions and composition operators. Therefore much research remains to be done. We believe that the starting point for this endeavour should be a thorough study of current component models, identifying their key characteristics and comparing their strengths and weaknesses. A desirable side-effect would be clarifying and unifying the CBD terminology. In this tutorial, we present a clear and concise exposition of all the current major software component models, including a taxonomy. The purpose is to distill and present knowledge of current software component models, as well as to present an analysis of their properties with respect to commonly accepted criteria for CBD. The taxonomy also provides a starting point for a unified terminology.