March 19-21, 2012,
Selma Lagerlöfsvej 300, 9220 Aalborg, DENMARK

Monday March 19 (room 0.2.90)

9.30-10.00          REGISTRATION

10.00-10.15         Opening and welcome by Kim G Larsen and Huibiao Zhu

10.15-11.00         He Jifeng: To be announced

11.00-12.30         Specification and Modeling Formalisms 1

Mikkel Koefoed Jakobsen, Jan Madsen and Michael R. Hansen: A Modelling Framework for Energy Harvesting Aware Wireless Sensor Networks

Line Juhl:  Energy Games

12.30-13.30         Lunch

13.30-15.00         Validation and Analysis Techniques 1

Phan Anh Dung, Michael R. Hansen, Aske Brekling: On Tool Support for Duration Calculus on the basis of Presburger Arithmetic

Alexandre David, Kim G. Larsen: Statistical Model Checking in UPPAAL

Mini Cases / Protocols 1

Ender Yuksel: Cyber Security in Smart Energy

15.00-15.30         Coffee

15.30-17.00         Mini Cases / Protocols 2

Geguang Pu: .To be announced.

Ender Yuksel: From protocols to scenarios

Xenofon Fafoutis, Nicola Dragoni: Adaptive Media Access Control for Energy Harvesting - Wireless Sensor Networks

18.00                     Guided Tour of Aalborg

19.30                     Dinner Princess Juliana

Tuesday March 20 (room 0.2.12)

9.00-10.15           Specification and Modeling Formalisms 2

Huibiao Zhu: To be announced

Radu Mardare: Modular Markovian Process, Logics and Metrics  (joint work with Luca Cardelli, Prakash Panangaden, Kim G Larsen)

10.15- 10.45        Coffee

10.45-11.45         Compsitionality vs Global Characteristics

Roberto Vigo: Securing CPSs: from the attacker scenario to formal verification.

Louis-Marie Traonouez: A parametric counterexample approach for robust timed specifications

11.45-13.00         Cross-level Property Preservation

Yingke Chen: Learning Markov models for stationary system behaviors
(joint with Hua Mao, Thomas D Nielsen, Manfred Jaeger, Kim G Larsen, Brian Nielsen)

Jian Zhang: To be announced

13.00-14.00         Lunch

14.00-17.30         Room 0.2.15

Board Meeting (Agenda will be sent later, but will include a short statement from all Work-package leaders)

19.00                     Dinner at Sohngaardsholm Castle

Wednesday March 21 (room 0.2.90)

9.00- 10.00          He Jifeng: To be announced

10.00-10.45         Tool Prototypes 1

Mads Christian Olesen, Andreas Dalsgaard: OPAAL and LTSMin

10.45-11.15         Coffee

11.15-12.45         Tool Prototypes 2

Peter Bulychev: Timed Games in Phyton
(with Alexandre David, Kim G Larsen, Jean-Francois Raskin, Gilles Geeraerts, ..)

Benoit Delahay: Specification Theories for Stochastic Systems

Zhang Zhangkui: Distributed Model Checking with MapReduce
(with Keiji Heljanko)

12.45-13.45         LUNCH

13.45-14.45         Specification and Modeling Formalisms 3

Jiri Srba: Multi-weighted Modal Transition Systems

14.45-15.15         Coffee

15.15-16.15         Validation and Analysis Techniques 2

Alexandre David, Dehui Du, Marius Mikucionis, Kim G Larsen:  Evaluation of Climate Controllers using UPPAAL SMC

Quantitative Model Checking PhD School

Invited Talks

• Rajeev Alur, University of Pennsylvania, Philadelphia
  Interfaces for Control Components
• Boudewijn Haverkort, University of Twente, Enschede, and Embedded Systems Institute, Eindhoven
  Formal Modeling and Analysis of Timed Systems: Technology Push or Market Pull?
• Oded Maler, VERIMAG, Grenoble
  Performance Evaluation of Schedulers in a Probabilistic Setting

The inauguration event of IDEA4CPS, Center for Foundations of Cyber-Physical Systems, a Sino-Danish research center funded by the Danish National Research Foundation, took place June 1, 2011 at the Department of Computer Science, Aalborg University. From left to right:

• Kristian G. Olesen (head of Department of Computer Science, Aalborg University),
• Li Guangyuan (Institute of Software, Chinese Academy of Science, Beijing and IDEA4CPS),
• Hanne R. Nielson (professor DTU and IDEA4CPS),
• Flemming Nielson (professor DTU, vice-PI IDEA4CPS),
• Thomas Sinkjær (director of Danish National Research Foundation),
• Kim G. Larsen (professor AAU, PI IDEA4CPS),
• Huibiao Zhu (East China Normal University, Shanghai, PI of IDEA4CPS),
• Jan Madsen (deputy head of IMM DTU and IDEA4CPS).

InfinIT afholder den 18. maj 2011 en konference i Aalborg Kongres Kulturcenter under titlen ”IT som Vækstmotor”. På konferencen sættes der specielt fokus på anvendelse af IT indenfor en række forskellige brancer omfattende

• energi
• transport
• frestillingsvirksomheder
• sundhed
• fødevarer

Konferencen tilbyder inspirerende oplæg af nøgle personer fra alle brancher, med efterfølgede workshops hvor IT og branchefolk sættes sammen.

Kom og vær med: registrering kan foretages via InfinIT’s hjemmeside (www.infinit.dk).

We are happy to (re)announce this short, but intense PhD course on the secrets of model checking, in particular for linear time and fairness properties, offered by one of the most prominent and productive researchers in the area.  Amongst several books, together with Ed Clarke and Orna Grumberg,  Doron Peled is the (co-) author of the authority book on the subject.

Marktoberdorf 2010, Vicotory

“Model Checking” is a generic name for methods for automatically checking the compatibility between a model and its formal specification. It is used to verify the correctness of software and hardware systems. The method has been successfully adopted by the hardware and software industry, and provides an automatic exhaustive alternative to software and hardware testing. Model checking usually compares a finite state model of a system (software or hardware against a specification given in some formal notation such as automata or logic.

In this series of lectures we will learn the basic methods and algorithms for model checking and how to use them. We focus on the following topics:

• Modeling of software and hardware systems.
• Software specification using temporal logic and Büchi Automata.
• Translation between logic and automata.
• Model Checking Algorithms.
• Specification and usage  of fairness properties
• How to make it work in practice: abstraction/reduction/BDDs

Time, Venue, ECTS, … :

• Monday January 7 and Tuesday January 8, 2011 (note new dates) Room 0.2.12.
• Aalborg University, Selma Lagerlöfsvej 300, Room 0.2.90, 9220 Aalborg, Denmark.
• 2 ECTS. A successful completion of the course consists in participation of the 2 days lectures and additional reading and solving exercises (approximately 30 hours).
• If you need assistance in finding accommodation we may help you.  Please contact Rikke Uhrenholt (rwu@cs.aau.dk)

Schedule:

• Monday 10.00-12.00 Introduction, Specification Formalisms (LTL) (chapter 5 in Software Reliability Methods)
  
• Monday 12.00-13.00 Lunch
• Monday 13.00-14.00 Automatic Verification (chapter 6 in Software Reliability Methods)
• Monday 14.00-15.30 SPIN I (provided by Ulrik Nyman)

• Tuesday 10.00-11.00 Translating from Logic to Automata (chapter 6 in Software Reliability Methods)
  
• Tuesday 11.00-12.00 The SPIN System
  
• Tuesday 12.00-13.00 Lunch
• Tuesday 13.00-14.00 Fairness, Abstractions
• Tuesday 14.00-15.30 SPIN II (provided by Ulrik Nyman)

Exercises (solutions to be emailed to Kim — kgl@cs.aau.dk) — by Tuesday February 22, 2011)

• Exercise 5.1, 5.2, 5.4, 5.6 and 5.14 (using the constructions(s) provided by Doron) from the following snippet of Joost-Pieter Katoen and Christel Baier: Principles of Model Checking
• SPIN exercises

Registration:

• For registration send email to Kim G. Larsen (kgl@cs.aau.dk) before February 3rd, 2011.

References:

1. D. Peled: Model Checking (23 pages) Mandatory Reading.
2. D. Peled: Software Reliability Methods. Springer; 2001 Main Reading  (we will have a 5 copies available that you may borrow).
3. Slides: http://www.dcs.warwick.ac.uk/~doron/big.ppt
4. E. M. Clarke, O. Grumberg, D. A. Peled. Model Checking. MIT Press; 2000.
5. C. Baier, J-P. Katoen. Principles of Model Checking. MIT Press; 2008.
6. E. A. Emerson, E. M. Clarke. Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons. Science of Computer Programming, Vol. 2; pp. 241-266; 1982.
7. J.Queille, J.Sifakis. Specication and Verication of Concurrent Systems in Caesar. 5th International Symposium on Programming; LNCS 137; Springer; pp. 337-351; 1981.
8. R. Gerth, D. Peled, M. Vardi, P. Wolper. Atomatic Simple on-the-fly Automatic Verication of Linear Temporal Logic. PSTV’95; pp. 3-18; 1995.

Previously Registered Participants:

• Claus Thrane
• Danny Poulsen
• Jiri Srba
• Jonas van Vliet
• Kenneth Lausdahl
• Kenneth Yrke Jørgensen
• Line Juhl
• Mads Christian Olesen
• Radu Mardare
• Rong Pan
• Saleem Vighio
• Sebastian Bauer
• Sune Wolff
• MS. Arifa Bhutto
• Mikael Harkjær Møller
• Yingke Chen
• Phan Anh Dung
• Simon Laursen
• Fabrizio Biondi
• Ulrik Mathias Nyman
  
• Thomas Bøgholm
• Mikkel Larsen Pedersen
• Saulius Samulevicius
• Dalia Kaulakiene
• Wang Zheng