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


Jan Tretmans - Model-based Testing
Systematic testing of software plays an important role in the quest for improved software quality. Testing, however, turns out to be an error-prone, expensive, and time-consuming process. Model-based testing is one of the promising technologies to meet the challenges imposed on software testing. In model-based testing a system under test (SUT) is tested against a formal description, or model, of the SUT’s behaviour.
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
The tutorial gives a fast introduction into the main concepts and results of the
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
Model-checking research initially focused on the verification of systems with a possibly large but finite state space. This was adequate for hardware systems, but much less so for software, where verysimple systems can already have infinite state-spaces. The sources of infinity can be roughly classified into three groups:
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
My three lectures will present a brief introduction to software model checking (SMC):
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
Discrete-state Markov processes are very common models used for performance and dependability evaluation of, for example, distributed information and communication systems. Over the last fifteen years, compositional model construction and model checking algorithms have been studied for these processes, and variations thereof, especially processes incorporating nondeterministic choices. In this paper we give a survey of model checking and compositional model construction for such processes in discrete and continuous time.
Background material:
From Concurrency Models to Numbers
Recordings and Slides

Axel Legay - Statistical Model Checking
The probabilistic model checking problem consists in deciding whether a stochastic system satisfies some property with a probability greater or equal to a certain threshold. There are several numerical algorithms for solving such problems. Unfortunately, they do not scale up to realistic systems. Moreover, they cannot approximate undecidable problems. In this lecture, we will show that techniques coming from the area of statistics can be used to efficiently solve/approximate the probabilistic model checking problem. We will mainly focus on hypothesis testing and its implementation within the UPPAAL-SMC model checker. Several real-life applications will be demonstrated.
Slides 1
Slides 2

Joel Ouaknine - Metric Temporal Logics
Lecture 1: A Survey of Classical, Real-Time, and Time-Bounded Verification
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
We will introduce the approach to compositional design of real-time systems, supported with verification by refinement checking. The basic modeling language used in the lecture is Timed I/O automata, so Timed Automata with control information. After introducing basics of the model, its semantics, and a few basic results we will continue to define a specification theory that allows to reason about abstractions of timed systems, including the notions of specification, implementation and a satisfaction/refienement relation that relates the two. Then we will show composition operators(conjunction, disjunction, parallel composition and quotienting) and how they can be used to build specifications of systems. We will combine them to build (finite) inductive proofs of correctness using refinements. We will also discuss robustness properties of real time specifications, and show simple rules that govern compositional design under certain robustness properties.
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

Réalisation Axome - Création de sites Internet