Java Pathfinder (JPF) is an open source analysis system that automatically verifies Java programs. The JPF tutorial provides an opportunity to software engineering researchers and practitioners to learn about JPF, be able to install and run JPF, and understand the concepts required to extend JPF. The hands-on tutorial will expose the attendees to the basic architecture framework of JPF, demonstrate the ways to use it for analyzing their artifacts, and illustrate how they can extend JPF to implement their own analyses. One of the defining qualities of JPF is its extensibility. JPF has been extended to support symbolic execution, directed automated random testing, different choice generation, configurable state abstractions, various heuristics for enabling bug detection, configurable search strategies, checking temporal properties and many more. JPF supports these extensions at the design level through a set of stable well defined interfaces. The interfaces are designed to not require changes to the core, yet enable the development of various JPF extensions. In this tutorial we provide attendees a hands on experience of developing different interfaces in order to extend JPF. The tutorial is targeted toward a general software engineering audience-software engineering researchers and practitioners. The attendees need to have a good understanding of the Java programming language and be fairly comfortable with Java program development. The attendees are not required to have any background in Java Pathfinder, software model checking or any other formal verification techniques. The tutorial will be self-contained.

LearnLib is a framework for model-based construction of dedicated learning solutions on the basis of extensible component libraries, which comprise various methods and tools to deal with realistic systems including test harnesses, reset mechanisms and abstraction/refinement techniques. The tutorial will comprise realistic experimentation, like test-based extraction of the user process from Web applications. The two main aims of this tutorial are (1) to familiarize the attendees with the technique of active automata learning: what it is, how it works, what its abilities and limitations are, and how it can be used in a software engineering context. And (2), to educate the attendees in the usage of the free automata learning library LearnLib, by explaining technical concepts, illustrating common use-cases, and specifically emphasize how it’s generic architecture can be used to easily integrate it in their software.

Model-based system engineering has been introduced to cope with the growing complexity of safety-critical systems. Some of the major concerns in model-based system engineering is to properly formalize the system properties and to design the system architecture so that the components are integrated in order to satisfy the system properties. Property-based approaches to system design focus on properties (rather than on behavioral models) and analyze the system properties to find errors very early in the design process, much before the components are implemented. Property specification languages are typically based on temporal logics and have been enriched to take into account real-time and safety aspects. In contract-based design, properties are structured into assumptions and guarantees to specify the properties on component interfaces. First conceived in the context of object-oriented programming, contract-based design is now applied also to the architecture of embedded systems. Contract-based design provides an ideal paradigm for a correct design of system architecture, with a clear description of the expected interaction of each component with its environment. This enables compositional reasoning, independent refinement and a proper reuse of components. The tutorial will introduce the concepts of property- and contract-based design for component-based system architectures in the context of embedded systems. The first part of the tutorial will give an overview of standard languages to describe system properties and architectures and formally define the concept of component interfaces and their semantics. The second part will focus on the contract-based framework provided by the OCRA tool, the property specification language used by OCRA, its support for the specification and verification of contracts refinement, and its usage within the modeling environments of CASE tools.