Published: 14th December 2012 DOI: 10.4204/EPTCS.103 ISSN: 2075-2180 |
Preface | |
Invited Tutorial: Adding Time to Pushdown Automata Parosh Aziz Abdulla, Mohamed Faouzi Atig and Jari Stenman | 1 |
Interactive verification of Markov chains: Two distributed protocol case studies Johannes Hölzl and Tobias Nipkow | 17 |
Invited Presentation: Reinventing Formal Methods: From Boolean-Correctness to Real-Correctness Boudewijn Haverkort | 32 |
Parameterized Metatheory for Continuous Markovian Logic Kim G. Larsen, Radu Mardare and Claus Thrane | 33 |
Invited Presentation: Scalable Set Computations in SpaceEx Goran Frehse | 48 |
Learning Markov Decision Processes for Model Checking Hua Mao, Yingke Chen, Manfred Jaeger, Thomas D. Nielsen, Kim G. Larsen and Brian Nielsen | 49 |
Invited Presentation: Qualitative Tree Languages Olivier Serre | 64 |
Abstract: Non-local Robustness Analysis via Rewriting Techniques Ivan Gazeau, Dale Miller and Catuscia Palamidessi | 65 |
This volume contains the proceedings of the Workshop on Quantities in Formal Methods, QFM 2012, held in Paris, France on 28 August 2012. The workshop was affiliated with the 18th Symposium on Formal Methods, FM 2012.
The focus of the workshop was on quantities in modeling, verification, and synthesis. Modern applications of formal methods require to reason formally on quantities such as time, resources, or probabilities. Standard formal methods and tools have gotten very good at modeling (and verifying) qualitative properties: whether or not certain events will occur. During the last years, these methods and tools have been extended to also cover quantitative aspects, notably leading to tools like e.g. UPPAAL (for real-time systems), PRISM (for probabilistic systems), and PHAVer (for hybrid systems). A lot of work remains to be done however before these tools can be used in the industrial applications at which they are aiming. Particular issues are as follows:
The workshop received four high-quality submissions, all of which were reviewed by three Program Committee members. Based on these reviews, they were all accepted for presentation at the workshop. Three of these submitted papers are contained in these proceedings, of the last contribution only an abstract.
The workshop program also included four invited talks by high-profile researchers within the field:
We would like to thank all authors and speakers for their efforts in making QFM 2012 a successful event. We are also grateful to the members of the Program Committee and the external reviewers for their work in assessing and improving the workshop submissions. We also thank the FM 2012 organizers for hosting our workshop and for their flawless conference organization, the providers of EasyChair for their greatly appreciated conference management system, and the people at EPTCS for their excellent support.
November 2012,
Uli Fahrenberg, Axel Legay and Claus Thrane
For long, the formal methods community has focused on functional correctness of systems. Great theory has been developed, however, the uptake of it in industry has been limited. One of the reasons for this is, I think, the too strong focus on "boolean correctness". Luckily, over the last decade, more and more attention has been paid to formal methods that also address partial correctness in one or another way, be it through the inclusion of probabilities, probabilistic time, stochastic simulation, etc. It is, however, important for the community not to overlook the results that have been delivered in this context for many years already, in classical fields like reliability engineering and performance evaluation.
In this talk, I will address two main topics. First of all, I will sketch a perspective on the use of quantitative methods in system design, a perspective that goes back to (at least) the 1960's. Secondly, if time permits, I will touch upon a concrete quantitative method for the analysis of fluid critical infrastructures (such as water and gas distribution plants) we are currently working upon.
In a variety of application domains such as embedded and cyber-physical systems, model-based design relies on models that incorporate time-driven as well as event-driven behavior. These so-called hybrid systems are difficult to analyze, because even small errors in the analysis algorithm can lead to qualitatively different behaviors. We verify safety properties of hybrid systems by computing their reachable states. Using set-based computations allows us to incorporate computation errors such that the resulting set is a conservative overapproximation of the actual solution. The difficulty is to find set representations for which the necessary operators are efficient to compute but still precise enough. In SpaceEx, our verification tool platform, we have implemented an algorithm that uses two set representations, polyhedra and support functions, to obtain maximum scalability. At each step of the algorithm, we choose the representation that provides the best compromise between speed and accuracy, based on the data and operator. While first-generation tools were limited to a few variables, SpaceEx has been used on hybrids systems with piecewise linear dynamics involving two hundred variables. This talk shall illustrate how combining different set representations makes the approach efficient.
We study finite automata running over infinite binary trees and we relax the notion of accepting run by allowing a negligible set (in the sense of measure theory) of non-accepting branches. In this qualitative setting, a tree is accepted by the automaton if there exists a run over this tree in which almost every branch is accepting. This leads to a new class of tree languages, called the qualitative tree languages that enjoys many properties. Then, we replace the existential quantification - a tree is accepted if there exists some accepting run over the input tree - by a probabilistic quantification - a tree is accepted if almost every run over the input tree is accepting. Together with the qualitative acceptance and the Büchi condition, we obtain a class of probabilistic tree automata with a decidable emptiness problem. To our knowledge, this is the first positive result for a class of probabilistic automaton over infinite trees.
Robustness is a correctness property which intuitively means that if the inputs to a program changes less than a fixed small amount then its output changes only slightly. The study of errors caused by finite-precision semantics requires a stronger property: the results in the finite-precision semantics have to be close to the result in the exact semantics. Compositional methods often are not useful in determining which programs are robust since key constructs---like the conditional and the while-loop---are not continuous. We propose a method for proving a while-loop always returns finite precision values close to the exact values. Our method uses some rewriting theory tools to analyze the possible paths in a program's execution in order to show that while local operations in a program might not be robust, the full program might be guaranteed to be robust. This method is non-local in the sense that instead of breaking the analysis down to single lines of code, it checks certain global properties of its structure. We show the applicability of our method on two standard algorithms: the CORDIC computation of the cosine and Dijkstra's shortest path algorithm.