Published: 10th December 2009 DOI: 10.4204/EPTCS.13 ISSN: 2075-2180 |
Preface | |
Adaptive Scheduling of Data Paths using Uppaal Tiga Israa AlAttili, Fred Houben, Georgeta Igna, Steffen Michels, Feng Zhu and Frits Vaandrager | 1 |
Markovian Testing Equivalence and Exponentially Timed Internal Actions Marco Bernardo | 13 |
Quantitative Safety: Linking Proof-Based Verification with Model Checking for Probabilistic Systems Ukachukwu Ndukwu | 27 |
Modelling Clock Synchronization in the Chess gMAC WSN Protocol Mathijs Schuts, Feng Zhu, Faranak Heidarian and Frits Vaandrager | 41 |
Strong, Weak and Branching Bisimulation for Transition Systems and Markov Reward Chains: A Unifying Matrix Approach Nikola Trčka | 55 |
Verifying Real-Time Systems using Explicit-time Description Methods Hao Wang and Wendy MacCaull | 67 |
This volume contains the papers presented
at the 1st Workshop on Quantitative Formal Methods: Theory and Applications, which was held in
Quantitative Formal Methods deals with
systems whose behaviour of interest is more than the traditional Boolean
``correct'' or ``incorrect'' judgment. Today there are many quantitative
aspects of system design: they include timing (whether discrete, continuous or
hybrid); probabilistic aspects of success or failure including cost and reward;
and quantified information flow. The aim of the workshop was to create a new
forum where current and novel theories and application areas of quantitative
methods could be discussed, together with the verification techniques that
might apply to them. The workshop invited three distinguished speakers, whose
talks illustrated both the diversity of quantitative aspects in the design of
modern applications and the theory required for their formal treatment:
Marco Bernardo (Universitá di Urbino)
Michael Butler (
Holger Hermanns (Universitat des Saarlandes)
In response to the call for papers we
received 15 full paper submissions. The programme committee selected 6 full
papers for presentation at the workshop and publication in these proceedings.
Additional four submissions were selected for presentation at the workshop:
they represent preliminary work with the potential to open up significant new
areas for research.
Mario Bravetti (
Pieter Collins (CWI, The
Georgios Fainekos (NEC Labs
Ansgar Fehnker (NICTA,
Goran Frehse (
David de Frutos-Escrig (Complutense
University of Madrid, Spain)
Bjarne Helvik (
Antonín Kučera (
Larissa Meinicke (Macquarie University, Australia)
Anna Philippou (
Jeremy Sproston (
Paulo Tabuada (
Elena Troubitsyna
(Ĺ
Verena Wolf (
and subreferees
Pepijn Crouzen (
Luuk Groenewegen (
Yolanda Ortega-Mallén
(Complutense
Oleg Sokolsky (
Anton Tarasyuk (Ĺ
We would like to thank the authors of the submitted papers, the invited speakers, the members of the programme committee, and their subreferees for their contribution, and to all workshop participants for making this event fruitful and worthwhile. The organizers gratefully acknowledge the financial support from FME and IPA, and the organizational support from the FMweek 2009 organizers Erik de Vink and Tijn Borghuis.
The QFM'09 Organizing Committee
Suzana Andova
Pedro D'Argenio
Pieter Cuijpers
Annabelle McIver
Jasen Markovski
Carroll Morgan
Manuel Núńez