International School on
Tool-based Rigorous Engineering of Software Systems

info.santoslab.org/event/stress2012 [poster]

Crete, Greece — October 10-14, 2012
(co-located with ISoLA 2012)

The International School on Tool-based Rigorous Engineering of Software Systems series aims to provide top-quality lectures and innovative pedagogical material that provide young researchers with:

• Instruction in existing and emerging formal methods and software engineering techniques that are tool-supported and process-oriented,
• Insights into how software is developed in the real world, including emphasis on domains such as safety/mission-critical software and embedded systems where the development effort associated with tool-based formal methods promises greatest returns,
• Case-studies and example domains in which formal methods have been successfully transitioned into actual development along with insights in how to bridge the gap between research tools and actual development processes,
• Additional pedagogical resources and personal contacts that they can explore for the purpose of increasing the impact of their research.

The 2012 School will feature lecturers with significant experience in software engineering, verification and validation techniques, software models, product lines, resource constrained systems, and medical device integration.   Lectures will discuss various aspects of technologies, tools, and process models for supporting rigorous development throughout a system’s lifecycle.

Medical Application Platforms for Medical Device Integration (Wed., Oct. 10)

John Hatcliff and Patrice Chalin (Kansas State University)

Medical devices historically have been monolithic units – developed, validated, and approved by regulatory authorities as stand- alone entities. Despite the fact that modern medical devices increasingly incorporate connectivity mechanisms that enable device data to be streamed to electronic health records and displays that aggregate data from multiple devices, connectivity is not being leveraged to allow an integrated collection of devices to work together as a single system to automate clinical work flows.  The Medical Device Coordination Framework (MDCF) is an open source middleware framework and an accompanying model-based development environment that can be used to integrate medical devices and implement apps that coordinate the actions of a collection of medical devices to accomplish a clinical task.   Developed jointly by researchers at Kansas State University and the University of Pennsylvania, the MDCF allows one to implement a “systems of systems” paradigm for medical devices. Such a paradigm shows great promise for supporting many applications that increase both the safety and effectiveness of medical care as well as the efficiency of clinical workflows. This tutorial will describe MDCF’s primary components and illustrate how the MDCF can be used to implement a variety of medical apps including multi-device safety interlocks, integrated displays, and multi-device “smart alarms”.   The tutorial will also discuss safety and regulatory issues being investigated with collaborators at the US Food and Drug Administration, Underwriters Laboratories, and the CIMIT Medical Device Plug-n-Play interoperability program.

The Sireum/Kiasan Symbolic Execution Framework and Symbolic Execution of SPARK and Java-like programs (Thu., Oct. 11)

Robby and Patrice Chalin (Kansas State University)

In recent years, symbolic execution has seen renewed interests as a program analysis technique. One such application is for verification of software contracts. Kiasan is an extensible symbolic execution framework with state-of-the-art algorithms, Eclipse-based visualization and user interface designed to support software contract checking.  Kiasan provides a number of novel capabilities that make it especially well suited for checking properties of a variety of modern software artifacts, for building your own symbolic execution engine, and for using it to teach symbolic execution concepts.  The tutorial will formally discuss foundational symbolic execution techniques, Kiasan's modular and extensible architecture, and will illustrate the ability to customize Kiasan's symbolic execution engine for specific domains.

Constraint-Based Variability Modelling (Fri., Oct. 12)

Tiziana Margaria (University of Potsdam) and Sven Jörges

Constraint-based variability modeling is flexible, declarative approach to managing variability. Product variants are defined in a top-down manner by successively restricting the admissible combinations of product artifacts until a specific product variant is determined. In this lecture, we illustrate the range of constraint-based variability modeling by discussing in particular two of its extreme flavors: constraint-guarded variability modeling and constraint-drivenvariability modeling. The former applies model checking to establish the global consistency of product variants which are built by manual specification of variations points, whereas the latter uses synthesis technology to fully automatically generate product variants that satisfy all given constraints. Each flavor is illustrated by means of a concrete case study, which will also be used during the tutorial on the variability tools suite.

Dynamic Testing of Reactive Systems: A learning-Based Approach (Sat., Oct. 13)

Bernhard Steffen (TU Dortmund) and Falk Howar (Carnegie Mellon University - Silicon Valley)

This lecture will provide an introduction to active learning of Mealy machines, an automata model particularly suited for modeling the behavior of realistic reactive systems. Active learning is characterized by its alternation of an exploration phase and a testing phase. During exploration phases so-called membership queries are used to construct hypothesis models of a system under learning. In testing phases so-called equivalence queries are used to compare respective hypothesis models to the actual system. These two phases are iterated until a valid model of the target system is produced. We will stepwise elaborate on this simple algorithmic pattern, its underlying correctness arguments, its limitations, and, in particular, methods to overcome apparent hurdles for practical application. This comprises ways to address real world applications, as well as the treatment of infinite data domains by abstraction refinement and/or innovative model structures like Register Automata. In combination with the LearnLib tutorial this should provide students and outsiders of the field with an intuitive account of the high potential of this challenging research area in particular concerning the control and validation of evolving reactive systems.

A Modest Approach to Rigorous Engineering of Resource Constrained Systems (Sun., Oct. 14)

Holger Hermanns and and Arnd Hartmanns (Saarland University)

MODEST is a behavioral modeling language for stochastic timed systems, which allow the representation of both probabilistic and real-time aspects together with nondeterministic decisions and abstractions. Rooted in process algebra, it has an expressive syntax enriched with features from programming languages, leading to concise models with a clearly defined semantics. A key idea behind MODEST is the single formalism, multiple-solution approach: A range of analysis options such as discrete-event simulation and different variants of model checking are available for a single MODEST model. An integrated design environment links to model checkers such as CADP, PRISM, or UPPAAL for analysis. This tutorial gives an introduction to the MODEST language and its underlying semantics, followed by a survey of the current state of analysis approaches and successful applications of MODEST to a broad range of case studies, with a particular focus on systems operating under power and runtime constraints.

Full day lectures will be held from Wednesday, Oct. 10, until Saturday, Oct. 13 (the week day assigned to each lecture is shown after the lecture title in the "Lectures" section above), with the following daily schedule:

  9:00 - 10:30 Lecture
 10:30 - 11:00 break
 11:00 - 12:30 Lecture (and Exercises & Tools)
 12:30 - 14:00 lunch
 14:00 - 15:30  Exercises & Tools
 15:30 - 16:00 break
 16:00 - 16:30 Wrap-up & discussion

Medical Device Coordination Framework (MDCF) – Enabling a New Paradigm of Medical Device Systems

John Hatcliff and Patrice Chalin (Kansas State University)

The Medical Device Coordination Framework is an open source middleware framework and an accompanying model-based development environment that can be used to integrate medical devices and implement apps that coordinate the actions of a collection of medical devices to accomplish a clinical task.

Sireum/Kiasan – An Extensible Symbolic Execution Framework

Robby and Patrice Chalin (Kansas State University)

The Sireum/Kiasan framework provides a number of novel capabilities that make it especially well suited for checking properties of a variety of modern software artifacts, for building your own symbolic execution engine, and for using it to teach symbolic execution concepts.

LearnLib – A Framework for Active Automata Learning

Malte Isberner and Maik Merten

The LearnLib (LL) 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. Its construction style allows application experts to control, adapt, and evaluate complex learning processes with minimal programming expertise.

The LearnLib tutorial will comprise realistic experimentation, like test-based extraction of the user process from Web applications, as well as the inference of Register Automata, a highly expressive model structure that is particularly suited to handle protocols or similar value-independent control structures. The goal is to provide participants with hands-on experience with a revolutionary new approach to system-level dynamic validation.

jABC – The jABC Variability Tool Suite: Flexible Management of Variant-Rich Processes

Anna-Lena Lamprecht and Stefan Naujokat

The jABC framework is a tool suite that supports model-driven, service oriented development of variant-rich processes. Addressing the complete life cycles of the processes, the jABC provides rich means for their design, verification, execution, and deployment. In particular, the jABC framework is unique in its application of different flavors of formal methods throughout the development process, which is facilitated by the formally defined structure of its process models. This is particularly valuable when dealing with complex product lines.

This tutorial focuses on the jABC's means for constraint-based variability modeling for variant-rich processes as discussed in the corresponding lecture. It aims at providing the participants with a hands-on experience of constraint-guarded variability modeling using the GEAR model checker and constraint-driven variability modeling using the PROPHETS process synthesis plugin. After a “warm-up” with a set of simple introductory examples, participants will be brought to contact with more complex, existing applications to further explore the different features of the constraint-based approaches to variability modeling.

MODEST Toolset

Holger Hermanns and and Arnd Hartmanns (Saarland University)

The MODEST Toolset is a collection of programs that support the construction and analysis of models specified in the Modest language for real-time, distributed and stochastic systems.