ArtistDesign NoE

55. Social event

Fabrizio Biondi — 2012-01-04T10:34:30Z

Dinner & Bowling

The social event will take place on Tuesday the 28th.

It will consist of a three course dinner (http://www.dgi-byen.com/restaurant/) followed by 2 hours bowling for everybody in DGI byen (http://www.dgi-byen.com/bowling/). The dinner will start at 18.30.

To go from ITU (Rued Langgaards Vej 7, 2300 København S) to DGI byen (Tietgensgade 65, 1704 København V) by public transportation you'll have to take bus 33 towards Rådhuspladsen from Hørgården bus stop on Amagerfælledvej. Get down at Stormgade/Glyptoteket and just follow Tietgensgade until you reach the destination.

The cost of social event is included in the registration fee.

43. Program

Fabrizio Biondi — 2012-01-04T10:33:24Z

All lectures are held at Auditorium 1, IT University, Rued Langgaards Vej 7, Copenhagen.

Monday

8:15 Reception opens in front of the Auditorium 1, ground floor in the Atrium

9:00 - 10:45 Axel Legay - Statistical Model Checking

10:45 - 11:15 Coffee break

11:15 - 13:00 Holger Hermanns - Compositional Stochastic Modeling and Verification

13:00 - 14:00 Lunch

14:00 - 15:45 Andrzej Wasowski - Compositional Design and Verification of Real-time Systems

15:45 - 16:15 Coffee break

16:15 - 18:00 Joel Ouaknine - A Survey of Classical, Real-Time, and Time-Bounded Verification

Tuesday

8:30 - 10:15 Axel Legay - Statistical Model Checking

10:15 - 10:45 Coffee break

10:45 - 12:30 Holger Hermanns - Compositional Stochastic Modeling and Verification

12:30 - 13:30 Lunch

13:30 - 14:15 Andrzej Wasowski - Compositional Design and Verification of Real-time Systems

14:15 - 15:15 Javier Esparza - Analysis of Systems with Infinite State Spaces

15:15 - 15:45 Coffee break

15:45 - 17:30 Joel Ouaknine - Decision problems for Metric Temporal Logic

18:30 Social event

Wednesday

8:30 - 10:15 Wolfgang Thomas - Infinite Games for Verification and Synthesis: Basic Theory and Quantitative Aspects

10:15 - 10:45 Coffee break

10:45 - 12:30 Jan Tretmans - Model-based Testing

12:30 - 13:15 Lunch

13:15 - 15:00 Jan Tretmans - Model-based Testing

15:00 - 15:30 Coffee break

15:30 - 17:20 Javier Esparza - Analysis of Systems with Infinite State Spaces

Thursday

8:30 - 10:15 Wolfgang Thomas - Infinite Games for Verification and Synthesis: Basic Theory and Quantitative Aspects

10:15 - 10:45 Coffee break

10:45 - 11:30 Jan Tretmans - Model-based Testing

11:30 - 12:30 Patrice Godefroid - Software Model Checking

12:30 - 13:30 Lunch

13:30 - 14:45 Patrice Godefroid - Software Model Checking

14:45 - 15:15 Coffee break

15:15 - 16:30 Patrice Godefroid - Software Model Checking

70. Organizers

Fabrizio Biondi — 2012-01-04T10:31:14Z

The PhD school is organized by Kim G. Larsen, Axel Legay and Andrzej Wąsowski (program co-chairs), Louis-Marie Traonouez and Fabrizio Biondi (local organizers).

30. Registration

Fabrizio Biondi — 2011-12-28T14:20:36Z

Registration to the school is now closed.

Please do not pay any fee without taking contact to Louis-Marie Traonouez first. The registration fee for the school is 1200 DKK, and your registration is only valid once we have received the fee at the following bank account:

Beneficiary: Aalborg Universitet Fredrik Bajers Vej 5 9100 Aalborg

CVR nr. 29102384

VAT. no. DK 29102384

Bank: Danske Bank Algade 53, 9000 Aalborg

Reg. nr: 3201 Konto nr: 9189629

IBAN nr: DK6730000009189629

SWIFT CODE: DABADKKK

Please state ”63343 + your name + your affiliation” on the statement of the transfer. It is important that you specify "63343" as a reference; otherwise our accounting system will not know the purpose of the transfer and we might not receive your money. Please note that due to technical limitations on our side, payment by credit card is not possible.

The registration fee covers meals and refreshments during the school and a social event. Please take care that all fees for transfer, currency conversion etc. are payable by you, so that we receive the exact amount of 1200 DKK. Your registration will be acknowledged once we receive the fee.

Note that we have a no-refunds policy. Once your registration has been received, no refunds will be possible. Also, the number of participants is limited, so we recomend early registration. The deadline for registering is the 7th of February.

For any question contact Louis-Marie Traonouez.

Participants successfully completing the school will be awarded 2 ECTS.

40. Lecturers

Fabrizio Biondi — 2011-12-28T14:01:58Z

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