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.

Quantitative modelling.

The success of these case studies suggests that it is possible to apply quantitative modelling techniques to novel emerging technologies. The following provide topical examples.

1. High-Speed trains.

The move to high-speed trains implies on-board signal displays to ensure a high degree of safety compliance. In turn this depends on the provision of reliable radio communications between the train cockpit and the and the static track-signalling system. The evaluation of safety is inherently quantitative, with the safety thresholds described in terms of average braking time, and the scenarios considered must take account of several trains, and uncertain terrain. Preliminary quantitative models of such systems provide only a partial evaluation, limited by the ability to explore only a few simplified scenarios. China and

New Zealand are currently investing in high-speed train technology, thus this application domain is very relevant for the Asia/Pacific region.

2. Quantitative security systems.

Security leaks can be formulated and measured in terms of quantitative rather than qualitative information flows. There is currently no agreement however on appropriate semantic domains on which to justify abstraction and verification techniques. With more elaborate semantic models it would be possible to provide realistic abstractions of security protocols capturing acceptable thresholds on their information leaks. Security is a worldwide concern.

3. Wireless communications for mesh networks.

Wireless networks operate in uncertain environments, and are susceptible to measurable failure rates. When used in large safety critical systems the cost of failure must be guaranteed to remain within some threshold of tolerance. The usual engineering methods to evaluate wireless protocols are based on simulation, but can be effectively augmented with more accurate models of protocol design giving the possibility of exploring a number of design variations in a wide range of scenarios. Wireless communications have a great many applications, and are of worldwide concern.

4. Smart electricity grid.

The aim of a smart grid is to use predicted consumption requirements (from users for example) in order to balance the load across a large catchment area. If this were possible then the reliability of the whole network would be considerably improved. The normal engineering methods such as testbeds to carry out the analysis in the development of such as system is hampered by high cost. An alternative is formal analysis. As for our other examples the appropriate models include probability, and quantitative information.

Typical analyses could explore the efficiency of appliance rescheduling, the accuracy of load predictions and whether these predictions can used effectively to balance the load across the network.

Smart grids are of considerable interest in Australia and Asia.

All of these examples can be regarded in principle as probabilistic, timed systems, but in practice they are often too large, or too complicated to be handled by traditional (e.g. model checking) methods, either because of “state space explosion” or the limitations of language expressivity provided by traditional verification systems.

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. In particular for a selection of the above challenge problems, the agenda of the meeting would be to:

1. Extract and specify the analysis problems;

2. Determine whether the current state-of-the-art tools can be applied to the specified problem, and to what extent.

3. If deficiencies in current techniques emerge, then their range or extent would be determined, eg limitations due to modelling languages, or semantics etc.

In Asia there are a number of strong research teams already working in the area of quantitative semantics and verification tools. Our proposed invitees include many of those researchers as well as a number of key researchers from the United States and Europe.

Scope, topics and proposed meeting format.

The focus of this proposed meeting is to share and disseminate new (mathematical) semantic, modelling techniques and novel tool developments which are needed for modern system analysis. Assuming a 4 day meeting we propose to focus on two or three of the examples sketched above, spending one day on each case study. We would hope to have an expert on the problems we select who could describe the problem domain and its specific challenges. The remaining part of the day would be spent exploring possible solutions, including the suitability of current techniques and how they might apply, as well as surveying the kinds of study which would contribute to the analysis.

The remaining day(s) would be spent on general discussions on techniques such as tool support, semantic structures, language and verification techniques which could apply to any of the problems. Topics for general discussion are expected to include

• Formal modeling of quantitative behaviour:
• Formal verification, testing, analysis as above.
• Formal analysis of quantitative performance, broadly understood.
• Industrial case-studies on any (combination) of the above, e.g., performance evaluation, security systems with probabilistic behaviour, risk analysis,
  
• Quantitative techniques in refinement, simulation and bisimulation;
• Quantitative algebraic and rewriting techniques.