Proceedings Quantities in Formal Methods

TL;DR

This paper discusses the integration of quantitative reasoning, such as time and resources, into formal methods, highlighting recent advances and ongoing challenges in applying these techniques to industrial-scale systems.

Contribution

It reviews recent developments in modeling, verification, and synthesis involving quantities in formal methods, emphasizing the extension of tools to handle quantitative properties.

Findings

Quantitative formal methods are increasingly used in system modeling.

Tools like UPPAAL, PRISM, and PHAVer support quantitative analysis.

Challenges remain for industrial adoption of these methods.

Abstract

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.