The conference will take place in the CC building on the campus of the University of Twente. Here you can find travel information to get to the University, and here is a map of the campus showing where the CC building is.
|
Wednesday, 20 March 2002 |
Programme to be announced
| Thursday, 21 March 2002 |
Programme to be announced
| Friday, 22 March 2002 |
Matthew Dwyer
Kansas State University, Dept. of Computing and Info. Sciences
234 Nichols Hall, Manhattan, KS 66506
dwyer@cis.ksu.edu
Model checking techniques have been an effective means for finding subtle defects in hardware designs and communication protocols. The increased use of concurrent software in embedded applications and the widespread adoption of Java with its built-in concurrency constructs have led researchers to attempt to adapt model-checking techniques to software. To date, this effort has been hindered by several obstacles including construction of correct tractable models from programs with enormous state spaces, appropriate specification of checkable software requirements, and interpretation of long, and potentially abstract, counterexample traces.
In this talk, we describe Bandera — an integrated collection of tools for model-checking concurrent Java software that attempts to overcome the obstacles described above. Bandera is a model compiler in the sense that it takes Java source code as input and compiles it to a program model expressed in the input language of one of several existing verification tools including Spin, dSpin, and JPF. Program slicing and abstract interpretation components are used during compilation to customize the program model with respect to the properties being checked. Bandera is like a debugger in the sense that it maps counterexamples produced by back-end model checkers back to the source code level, and it allows the user to replay program execution both forwards and backwards along the path of the counterexample.
We will present an overview of several case studies using Bandera that provide positive evidence of the effectiveness of model checking realistic properties of non-trivial concurrent software. These case studies also point out the need for additional functionality to enable scaling of software model checking to even larger and more complex systems. Finally, we conclude with a description of the latest public release of the Bandera toolset and our plans for future functionality.
Steve Schneider
Department of Computer Science, Royal Holloway, University of London
S.Schneider@cs.rhul.ac.uk
Formal methods for verifying authentication protocols tend to assume an idealised, perfect form of encryption. This approach has been spectacularly successful in finding flaws, but when we aim for proofs of correctness then we need to consider this assumption more carefully, and perhaps to weaken it to reflect properties of real cryptographic mechanisms. This paper reviews the existing CSP approach to verifying protocols, and considers how algebraic properties of real cryptographic mechanisms can be incorporated within a rank function verification. The approach is illustrated with an authentication protocol which makes use of exclusive-or.
Carolyn Talcott
SRI International, 333 Ravenswood Avenue, Menlo Park CA 94025SRI
clt@cs.stanford.edu
Middleware such as Corba ORBs, DCOM, or Java Beans provide programming abstractions for interoperation of diverse components in an open distributed setting. More recent middleware initiatives focus on resource management, security, and dependability services supporting a wide range of coordination and Quality of Service (QoS) requirements and allowing applications programmers to focus on functionality and intrinsic performance issues. As computer systems become more and more complex and ubiquitous it is increasingly important to have robust and powerful middleware that can achieve a high degree of reliability and assurance where needed. For example, as networks become more programmable it will be essential to minimize failures not only by simulation and testing, but also by formal modeling and analysis at many levels of abstraction. For adaptability and extensibility middleware services themselves need to be built from component services. Middleware services for resource management such as scheduling, protocols providing security and reliability, load balancing and stream synchronization, execute concurrently with each other and with application activities and can therefore potentially interfere with each other in subtle ways.
The Two Level Actor Model (TLAM) is a mathematical framework designed for reasoning about the interaction and composition of resource management activities in open distributed systems, and their dynamic installation and modification. The TLAM is based on the actor model of object-based distributed computation. As the name suggests, in the TLAM, a system is composed of two kinds of actors, base-level actors and meta-level actors, distributed over a network of processing nodes. Base-level actors carry out application-level computation, while meta-level actors are part of the runtime system (middleware) that manages system resources and controls the runtime semantics of the base level. The TLAM model has been applied to reasoning about services such as migration, distributed garbage collection, and QoS-based multimedia services.
The TLAM approach to modeling middleware components is to develop a family of specifications from different points of view and at different levels of abstraction and to establish entailment relations between specifications from different points of view. From a global point of view we specify the end-to-end service provided by a system in response to a request. This can be refined by expressing system wide properties in terms of of abstract properties of the underlying network. From a local point of view we specify constraints on the behavior and distribution of a group of meta-actors. This local behavior point of view can be further refined by specifying algorithms for the actions of individual actors. The staging and refinement of specifications provides a form of modularity, scalability, and reusability. It reduces the task of implementation to that of implementing individual abstract behaviors or algorithms. Behavior level specifications can be used to guide or check implementations or even serve as executable prototypes.
In this talk, we will briefly review the TLAM model and methodology and discuss extensions to model communication and real-time services. We will also discuss the relation of the TLAM architecture to the architectures developed in several ongoing middleware initiatives, and show how the TLAM can be used to specify and analyze services in these platforms.
