- Workshops
- Past Workshops
- Schools and Seminars
- International Collaboration
- Publications
- Contributions to Standards
- Course Materials Available Online

February 27th - March 1st 2012 Copenhagen, Denmark |
organised and funded by ARTIST |

There will be lectures and other activities by eight international researchers, each a recognized authority within their field:

Jan Tretmans - Model-based Testing

Such a model serves as a precise and complete specification of what the SUT should do, and, consequently, is a good basis for the generation of test cases. This makes testing faster and less error-prone: millions of test events can be automatically generated from the model, and subsequently executed and the results analysed. And if the model is valid, i.e. expresses precisely what the SUT shall do, then all these tests are provably valid too.

The lecture will give an introduction to model-based testing in general, and then discuss model-based testing for labelled transition systems, including models, systems under test, conformance relations, and a test generation algorithm, which is shown to produce provably sound and exhaustive test suites. Variations and extensions for component-based- and for real-time model-based testing are then presented. A downloadable tool, a demo, and a discussion of industrial applicability will conclude the lecture.

Literature:

J. Tretmans, Model Based Testing with Labelled Transition Systems.

In R. Hierons, et al., Formal Methods and Testing.

LNCS 4949, pp. 1-38, 2008.

J. Schmaltz, J. Tretmans, On Conformance Testing for Timed Systems.

In: F. Cassez, C. Jard (editors), Formats 2008.

LNCS 5215, pp. 250-264. Springer-Verlag, 2008.

The JTorX tool

Slides 1

Slides 2

Wolfgang Thomas - Infinite Games for Verification and Synthesis: Basic Theory and Quantitative Aspects

algorithmic theory of infinite games. This theory is very useful for the understanding of nonterminating reactive systems, and its constructions have many applications in practice, e.g. in controller synthesis. In the first part of the tutorial we start with Church’s Problem on the "solution" of infinite games, and we present the main result emerging from this problem, stating that for regular infinite games one can decide whoof the two players wins, and automatically synthesize a finite-state winning strategy for him. In the second part we address several quantitative aspects of the problem: We briefly mention the question of memory minimization, the solution of games where one player can delay his moves for some time, the question of guaranteeing fast responses in so-called request-response games, and we finally sketch the solution of the most important class of games with quantitive objectives, namely mean-payoff games over finite arenas.

Slides

Javier Esparza - Analysis of Systems with Infinite State Spaces

Control: (possibly recursive) procedures and process creation require to enrich the notion of state with unbounded stacks or sets.

Data: the use of any datatype with an infinite range, like integers, reals, lists, queues, etc. potentially leads to an infinite state space.

Parameterization: distributed algorithms (like algorithms for mutual exclusion, leader election, byzantine agreement, etc.) are often designed to work for an arbitrary number of processes, i.e., a distributed algorithm is in fact an infinite infinite family of systems. Checking that all elements of the family satisfy a property can be reduced to checking that one single infinite-state system satisfies it.

The model-checking community started to analyze these different infinities in the mid 90s, and some generic techniques for dealing with them started to emerge. In the course I introduce them, and apply them to three classes of systems: timed automata, broadcast protocols, and pushdown systems.

Slides

Patrice Godefroid - Software Model Checking

SMC 1.0: Software Model Checking via Systematic Testing (VeriSoft, CHESS, etc. and application to communication software)

SMC 2.0: Software Model Checking via Abstraction (SLAM, BLAST, etc. and application to device drivers)

SMC 3.0: Software Model Checking via Dynamic Test Generation (DART, SAGE, etc. and application to security testing)

Holger Hermanns - Compositional Stochastic Modeling and Verification

Background material:

From Concurrency Models to Numbers

Recordings and Slides

Axel Legay - Statistical Model Checking

Slides 1

Slides 2

Joel Ouaknine - Metric Temporal Logics

Abstract: I will survey the classical, real-time, and time-bounded theories of verification, highlighting key differences and similarities among them, and presenting some recent developments in the field.

Lecture 2: Decision problems for Metric Temporal Logic

Abstract: I will discuss some key decision problems for Metric Temporal Logic (and fragments), such as satisfiability and model checking.

Slides 1

Slides 2

Slides 3

Slides 4

Andrzej Wasowski - Compositional Design and Verification of Real-time Systems

The lecture will involve a case study in modeling of a leader election protocol, demonstrated with the tool ECDAR. We will demonstrate ECDAR and its parametric extension that reasons about robustness.

Homepage of the ECDAR tool

Slides 1

Slides 2

Slides 3

Slides 4

(c) Artist Consortium, All Rights Reserved - 2006, 2007, 2008, 2009