In recent years there has been an increasing move towards analyzing software programs with the aid of model checking. In this tutorial we will focus on one of the first model checkers developed specifically for analyzing programs - Java PathFinder (JPF). JPF was awarded the 2003 Engineering Innovation award from NASA's Office of Aerospace Technology. JPF is freely available and the development became an open-source project in April 2005. JPF has been used on numerous NASA applications, including, Mars Rover control, Deep-Space 1 fault protection, and Shuttle ground control software as well as on software from companies such as Fujitsu.

JPF is an explicit-state model checker that analyzes Java programs on the bytecode level. Since it works on the bytecode level, it can deal with all Java's language features, including, concurrency, dynamic class loading, dynamic creation of threads and objects, garbage collection, exception handling, etc. The tutorial will highlight the main capabilities of the tool and also its current weaknesses. One of the core design decisions was to create a modular tool that could easily be understood and extended by others. A core component of the tutorial will be an introduction to the tool architecture as well as the features making it extensible (Listener interfaces and the Model Java interface). In addition we will discuss the features of the tool that make model checking Java programs tractable, these will include, state compression and storage, dynamic partial-order reduction and using search heuristics.

To give an indication of the current research direction of JPF the last part of the tutorial will focus on the tool's new features, such as the symbolic execution and test-case generation facilities. JPF supports symbolic execution of linear integer arithmetic as well dynamically allocated structured data (e.g. linked lists, red-black trees, etc.). We will show how a simple extension of JPF allows the combination of symbolic execution, predicate abstraction and shape analysis for efficient test-input generation.

We will conclude the tutorial with a discussion of our experiences of using the tool for the past five years and where we believe the biggest challenges for software model checking is in the future.

This half-day tutorial gives an overview of the current state-of-the-art in software visualization. Soft- ware visualization encompasses the development and evaluation of methods for graphically representing diRerent aspects of software, including its structure, its execution, and its evolution. In contrast to visual programming and diagramming for software design, software visualization is not so much concerned with the construction, but with the analysis of programs and their development process. Software visual- ization combines techniques from areas like software engineering, programming languages, data mining, computer graphics, information visualization and human-computer interaction. Topics covered in this tutorial include static program visualization, algorithm animation, visual debugging, as well as the visu- alization of the evolution of software. In particular we identify common principles illustrated by many examples and give pointers to tools available today.

Stephan Diehl is a full professor for computer science and chair of software engineering at University Trier. He studied computer science and computational linguistics at Saarland University, and as a Fulbright scholar at Worcester Polytechnic Institute, Massachusetts. He received his PhD from Saarland University as a scholar of the German Research Foundation (DFG) working in the group of Prof. Reinhard Wilhelm. Stephan Diehl's research interests include programming languages and compiler design, web technologies, educational software and visualization, in particular software visualization. He teaches courses on software visualization in academia as well as industry (for the Deutsche Informatik Akademie www.dia-bonn.de) and has been heavily involved in various international software visualization related events.

Model checking tries to explore the entire behavior of a system by investigating each reachable system state. Recently, verification of Java programs has become increasingly important, and several model checkers for Java programs have been created. However, existing software model checkers can only explore a single process and are not applicable to networked applications, where several processes interact. Most non-trivial programs which are in use today use network communication. Recent novel approaches overcome this gap between distributed applications and model checker capabilities.

Process centralization is a technique that allows model checking of distributed applications: Processes are converted into threads and merged into a single application. Networked applications can then run as one multi-threaded application. This approach is applicable if all programs to be merged are available in the same format and interprogram communication can be modeled accurately. Previous work by Stoller and Liu inlined parts of one program in another one, modeling certain patterns of interaction using Remote Method Invocation (RMI) under Java. Very recent work extends this to a fully transparent replacement of TCP/IP network communication [1], making this approach suitable for testing, debugging, and software model checking. This tutorial focuses on model checking such applications, including the treatment of all possible interleavings of threads, network messages, and non-determinismregarding possible network failures. Alternatives to centralization will also be presented. The target language is Java, but ideas from this tutorial are also applicable to other programming languages.

The tutorial will cover very recent work, but will still be very practically oriented. Theoretical background is given as far as necessary. The focus will be on concrete problems arising from converting multi-process applications to a multi-threaded program, and from modeling network communication.

Cyrille Artho has completed his Ph.D. at ETH Zurich, Switzerland, in May 2005. From June 2006 onwards, he started his post-doctoral research at the National Institute of Informatics in Tokyo, Japan. He has given several introductory lectures on Model Checking while working together with NII researchers on an advanced course about model checking for distributed Java programs. A first installment of this lecture will have been completed prior to this tutorial, and the survey paper will also be based on material used in the lecture.

A measure for the quality of software is be the extent to which it corresponds to the business objectives and requirements it was designed for. The earlier those who elicit the requirements and those who will use the software can be involved in the development process, the better the results will be, and the lower the cost and time of development. This applies especially to the development of complex B2B transactions, which may be a long and tedious task, as it requires the collaboration of business and IT experts from all business parties of the value-creation chain.

From a business point of view, the following challenges must be addressed to enable electronic business collaboration:

• On a conceptual level, the common planning and coordination of business activities presupposes that all parties involved have the same understanding of the business model. They need to agree on which customers they will address and understand their respective needs. They need to have a common view on the products and services they produce to meet those needs, and they need to clarify who adds what to the value creation and what each party expects in return.
• On an operational level, the business processes of each partner in the supply chain must be aligned with those of its suppliers, intermediaries and customers. This involves a fairly detailed conception of the ideal flow of goods, financial resources and information between the supply chain parties throughout the value creation process. The question that must be answered in this phase is ghow do we organize ourselves in terms of our value creation activities, the information exchange needed to support them and the rules that help us coordinate and manage our collaboration?h

While the first level of collaboration focuses on whether what we do is the right thing and that every actor involved understands and buys into the business idea, the second challenge is about doing things right, that is, to structure and organize the business activities of each actor in a way that we achieve our common goals, i.e. to produce a maximum of value for our customers while keeping costs as low as possible.

In order for us to deal with both of these levels of collaboration and to keep them in coherence, a necessary prerequisite is to consider the whole value creation process (end-to-end transactions)as opposed to a standard B2B scenario that takes the viewpoint of only two business actors and describes the way that they collaborate with each other.

From a SE point of view, the following issues need to be addressed:

• A communication issue between business people and IT developers, especially when the requirements are put down in natural language and may be ambiguous.
• The complexity of the transaction, that spans the whole value-creation process and involves multiple companies.
• The time to market for the development of a new business transaction, from its conception to its deployment.

This tutorial presents the audience with an integrated method to design and validate end-to-end B2B transactions. Starting with a description of the business model that gives rise to business collaboration, the audience is presented a systematic approach to develop a sound and integrated business transaction.

Sophie Ramel obtained her engineer diploma in an high school (ENSEEIHT) in Toulouse in France, in the computer science and applied mathematics field. She came to the CRP Henri Tudor where she works as a a project manager and R&D engineer on different projects, including a project on the automatic animation of B2B transactions modeled in UML; She acquired competencies in the field of software engineering, especially on Java-related technologies, XML and web services, as well as in IT modelling, analysis and IT architectures. Sophie is in charge of an open source integration project, she is member of the free software innovation platform of the CRP Henri Tudor and works on a methodology for software engineering with open-source/free software components.

Michael Schmitt is scientific coordinator and project manager at the CRP Henri Tudor. He has a Masterfs degree from UMIST/England and an MBA from the University of Saarland. He worked for over 10 years in the field of electronic business both in the private and public sector. Before Michael joined the CITI, he was responsible for the European EDI & B2B clearing center at Avnet Electronics Marketing in Munich, a large distributor of electronic components.