ARTIST2 Graduate Course on: Automated Formal Methods for Embedded Systems 2008

June 16-24, 2008       DTU - Lyngby, Denmark organised and funded by ARTIST 


Preliminary plan.


Morning Introduction to the course, modeling of finite-state systems
Afternoon Computation tree logic (CTL) and CTL model checking

Tuesday- Symbolic methods I: Finite state

Morning Circuit equivalence and propositional SAT solving
Afternoon Symbolic representation of transition systems, reachability
(both bounded and full), symbolic CTL model checking

Wednesday - Symbolic methods II: Hybrid state

Morning Hybrid discrete-continuous automata models
Afternoon: Verification by approximation

Thursday - Symbolic techniques III: Satisfiability for large arithmetic formulae

Morning SAT modulo theory
Afternoon Lab exercises

Friday - Symbolic techniques III: Satisfiability for large arithmetic formulae

Morning Robust semantics of arithmetic formulae, satisfiability procedures for undecidable arithmetic
Afternoon Lab exercises


A strong interest shift from single robot to mulrirobot systems
has been taken place in robotics during recent years. Multirobot
systems are considered as physically embodied multi agent systems
constrained with the laws of physics. Planning and coordination of
multirobot systems are generally approached with a centralized
controller in mind. Coordination methods for systems involving
large number of robots like in robot swarms can be scaled up by
using fully distributed coordination architectures only. That sets
a new challenge to formal methods supporting the design and
verification of multirobot systems.
The focus of this course is on techniques and software-tools that
can be used to assess the quality and correctness of multirobot
systems’ behavior. The course emphasizes tools and techniques for
model-based development and formal verification of multirobot
system designs, particularly for model construction, model-based
reactive planning and mission verification. The topic is
illustrated with two case-studies: synthesis of the planning unit
for an assistive Scrub Nurse Robot and verification of a
self-stabilizing robot swarm coordination algorithm. The course
will contain a mix of lecturing and hands-on exercises especially
built around the Uppaal tool suite.


To be decided

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

Réalisation Axome - Création de sites Internet