T1: Model Checking for Software

Description:
Model checking consists of the exhaustive exploration of the state space of a dynamic system.  Recently, there has been a trend towards applying model checking to computer software.  However, model checking of software is a tough problem, due to the increased complexity of typical software applications vs. hardware.  To gain wider acceptance, model checking must also be made more accessible to software developers.  This tutorial will give an overview of the main principles and tools for model checking, and will give a survey of some recent progress in in model checking applied to software.  There will be two parts, devoted respectively to explicit-state and symbolic techniques.

Explicit-state model checking explores each individual state of the system individually.  The SPIN tool from Bell Labs is one of the most widely used in this category.  We will address the explicit-state analysis of actual source code written in  popular programming languages such as C, C++ and JAVA. It is clear that model checking by itself will often not be enough to analyze programs due to the large  state-spaces of these programs. We will introduce some of the approaches  currently being used to model  check programs with  special emphasis on the Java  PathFinder (JPF) model  checker and the  role of complementary analyses such as abstraction, static analysis and runtime analysis within JPF.
 
Symbolic model checking uses efficient encodings of logic formulas, such as binary decision diagrams (BDDs), to represent and explore whole sets of system states in a single operation.  For systems that can be suitably represented, this allows the exploration of huge state spaces of 10^50 states and more.  We will present SMV, a well-known symbolic model checker from Carnegie Mellon
University, with an input language for describing finite state systems and their properties in the CTL temporal logic.  We will then illustrate the analysis of domain-specific modeling languages, such as those developed at NASA for model-based autonomous space-craft controllers, by automated translation of those languages to SMV.

Dr. Charles Pecheur is a research scientist at NASA Ames Research Center. He is developing and applying tools to verify model-based autonomy software, in particular using the SMV symbolic model checker.
 
Dr. Willem Visser is a research scientist at NASA Ames Research Center.  He is currently one of the developers of Java PathFinder 2, a native model checker for Java programs.

T2: The Role of Graph Transformation in Software Engineering and Requirements Engineering

Description:
Graphical representations are an obvious means to describe various aspects of software systems. Many widely used methods in requirements engineering and software design are based on graphs and graph changes. These graph manipulation are systematically investigated in the area of graph transformation. This formalism provides a variety of benefits important in the context of visual development, e.g., the combination of intuitive usability with the formal basis of visual specifications. A graph transformation step is described in a rule-based manner by defining parts of the graph structure before and after a transformation.

To handle several distributed parts of a graph where each part can be changed independently of others or in a synchronized way, distributed graph transformation has been developed. Here, graph transformation is employed twice: to describe the dynamic reconfiguration of the overall network of components, and to model evolving data and object structures within the components.

The main goal of this tutorial is to give an overview on the many application areas of graph transformation in the context of requirements engineering and software design and to impart a profound insight into the techniques of graph transformation based on algebra (category theory). In addition, tool support in form of a graph transformation machine implemented in Java is presented.

Two major case studies are discussed in order to demonstrate how the techniques presented in this tutorial work. The first case study refers to requirements engineering and tackles the multiple perspectives problem. We sketch how distributed graph transformation serves as a natural underlying formalism for the ViewPoints framework and how this approach helps to support multiple perspectives integration, Inter-ViewPoint negotiation and inconsistency management. The second case study refers to classical software engineering problems centered around architecture design. We discuss the possibility to represent semantic properties of components by the techniques presented in this tutorial with the final aim of realizing semantics-directed component negotiation and dynamic architecture (re-) configuration. Both case studies include a brief presentation of tool support developed for each case study on top of the general graph transformation tool.

Michael Goedicke is professor for computer science at the Department of Mathematics and Computer Science at the University of Essen, Germany. He studied Computer Science at the University of Dortmund and received there his Diploma Degree (Masters Degree) in Computer Science in 1980. He received his Ph.D. in 1985 and his Habilitation in 1993 from the Department of Computer Science of the University of Dortmund as well. His special field of interest is specification of software systems and software engineering. He is principal investigator in various national and international research projects and currently conducting research in formal methods and languages for requirements engineering.

Torsten Meyer is research assistant at the Department of Mathematics and Computer Science at the University of Essen, Germany. He studied Business Computing at the University of Essen and received there his Diploma Degree (Masters Degree) in 1995. He received his Ph.D. in 2000 from the Department of Computer Science of the University of Essen as well. His special fields of interest are software architecture, configurable distributed systems, requirements engineering and graph transformation.

Gabriele Taentzer is working in the field of graph transformation since more than 10 years. After studying computer science at the Technical University of Berlin she received her Diploma degree in 1990 and her Ph.D. in 1996. She has extensive teaching experience including a lecture on the European School on Graph Transformation. She coorganized the last workshop on graph transformation which took place as a satellite event of ETAPS 2000 in Berlin this year. She is coeditor of two special issues on graph transformation appearing in the journals MSCS and SCP. Her research addresses the application of graph transformation to software engineering and the visual development of distributed systems.
Gabriele Taentzer is working in the group of Prof. Hartmut Ehrig at the Technical University of Berlin. Hartmut Ehrig is a leading authority in the field of graph transformation.

T3: Synchronous Programming of Reactive Systems: Principles, Languages, Compilers, Program Validation

Description:
Reactive systems are computer systems which maintain a continuous, real-time, interaction with an external, possibly physical, environment. Synchronous programming is an abstract point of view on reactive systems, which considers such a system as a synchronous product of automata. A transition of each automaton corresponds to an atomic, conceptually instantaneous, reaction of the reactive component to events coming either from the environment or from other synchronous components.

Based on this point of view, several programming languages have been proposed, mainly in France. In this tutorial, we will consider two of them: The imperative language Esterel, and the data-flow language Lustre. The basic principles of the languages will be first presented and illustrated. Then we will expain some common problems and techniques related to the semantics and compilation of synchronous languages. The addressed class of reactive systems being generally highly critical, program validation is an important issue. This is why we wil finally present available validation techniques and tools (formal verification, automatic testing).

Nicolas Halbwachs is "Research Director" at CNRS. His first work was on abstract interpretation of programs, with Patrick Cousot. In 1984, he obtained his "State Thesis", at "Institut National Polytechnique de Grenoble", under the supervision of Paul Caspi, on a formal model of real-time system behavior. Since then, he was one of the main designers of the synchronous data-flow language Lustre. He successively worked on the language design, compilation to software and hardware, and on formal verification and testing of synchronous programs. He is strongly involved in the industrial transfer of Lustre technology.

T4: Component Technologies - An Overview

Description:
This tutorial will provide an overview of component technologies to software engineering researchers and practitioners. We will review local component technologies, such as Microsoft's Component Object Model and Sun's Java Beans. We will then indicate distributed object technologies, including Sun's Remote Method Invocation and the OMG's Common Object Request Broker Architecture. We will then highlight how these two technologies merged and let to distributed component models. We will discuss these by comparing Microsoft's Distributed Component Model with Sun's Enterprise Java Beans and the OMG's CORBA Component Model.

Dr. Wolfgang Emmerich is a Lecturer in Computer Science at University College London. He has authored numerous papers about distributed software engineering and a long standing interest in distributed object and component technologies. Wolfgang has recently published a textbook on "Engineering Distributed Objects" with John Wiley & Sons. He is also actively consulting in industry through his consultancy firm Zuehlke Engineering.

Back to The ASE2000 Homepage

Maintained by Jerry Gannod (gannod@asu.edu)