Jun 27, 2012
Overview
9-12 November, 2012
The history and motivation for quantitative formal methods.
Quantitative Formal Methods deal with systems whose behaviour of interest is more than the traditional Boolean “correct” or “incorrect” judgment. That includes timing (whether discrete, continuous or hybrid), as well as probabilistic aspects of success or failure including cost and reward, and quantified information flow.
The major challenge for researchers is to develop quantitative techniques that are both supple and relevant: the former is important because theories that amplify our reasoning powers are key to understanding system behaviour; the latter is important because our ultimate goal is to improve the practice of developing, deploying and certifying actual running software in the field.
There has been intense research in the development of semantic methods and associated tools for the analysis of quantitative properties of systems, resulting in a number of mature tools having impressive portfolios of case studies.
Modelling and verification challenges.
One of the major challenges in this area is that generic verification systems are difficult to apply. For example wireless protocols are large and complex and even if current algorithmic analysis (such as used in model checking) are able analyse them in principle, the modelling languages and approaches typically used in these tools do not include advanced structuring mechanisms to describe them nor the semantic detail to interpret them in a form to which algorithmic techniques can be directly applied, or even modelled. Moreover some of the semantic issues are yet to be resolved; this is the case for security systems where there is not yet agreement as to semantic structures that apply both to the specific characteristics of the systems (measurement of information flow) and the abstraction techniques that are typically used in verification techniques. Similarly in wireless applications and the smart grid, more tailored methods capturing their characteristics tend to have much greater traction than general formal methods.
From the practical verification perspective there is a great deal of untapped potential both in recent theoretical and developing tool capabilities. Researchers have a better understanding of how to apply theoretical structures including categorical features, metric spaces and domain spaces which show how to take advantage of algorithmic techniques which similarly have been developing, but without necessarily with a particular semantics in mind. It is now within reach of researchers to bring together those advances to apply them to modern systems which rely on critical, quantified analysis.
Meeting goals.
The broad aims of this proposed meeting are to explore effective modelling and analysis methods with which to tackle the above challenging problems. Through a focussed study of a selection of these case studies, the goal is to bring together existing and emerging techniques in semantics and algorithms, possibly combining them in new ways. The hope is to obtain powerful new verification techniques able to tackle the quantitative aspects of modern system designs.