Science in Venice

Venice is beautiful at any time of year but particularly in the fading summer. So an invitation to a technical meeting held there, attended by good friends and with an informal programme that gave lots of scope for discussion was welcome. The meeting was organised by an loose group of European Research Council grant holders (Ghezzi, Uchitel, Mylopoulos & Kriatkowska) and, though there was no announced theme or title, it had a strong, and I judge important, emergent focus. To appreciate this focus and to understand the wide ranging consequences of the work it is necessary for me to set some context.

Reasoning about complex software systems, particularly verifying the key properties a system holds, is a well established challenge in software engineering research. Recently there have been significant advances which have allowed techniques, principally based on 'model-checking', hitherto confined to small systems, to be used on practically sized systems. These advances have largely been in the computational methods used to handle the very large state spaces on which model-checking is based. Conventional model-checking reasons over states of a system and can say if a property (such as freedom from a 'deadlock') holds, and generate a counter-example if it does not hold. The properties and the underlying representation of the system are respectively 'functional' and 'deterministic'. The most interesting properties and systems, from a usage standpoint, are 'non-functional', resource constrained, and stochastic. The main theme of the meeting was then the development of approaches that combine model-checking with probabilistic and quantitative reasoning. Though this is a largely technical pursuit it has broader implications.

The question of the relationship between computer science and engineering is a difficult one. Much meaningless drivel has been written about it. I have learned over time that it is, on the whole, a topic best avoided. It is clear that, whatever the similarities, the mathematical and analytical tools deployed by computer scientists exhibit significant differences: computer science has largely (though not exclusively) used discrete mathematics and logic, while engineering has largely (though not exclusively) deployed continuous methods. The classes of system that computer scientist are now interested in: ultra-large scale, operating autonomously in dynamic environments, and sensitive to performance, energy usage etc, require the sort of analysis hitherto restricted to conventional engineering.

What is exciting, is the possibility that, rather than straightforwardly borrowing from engineering, a wholly new set of methods that bring together qualitative (for want of a better term) and quantitative reasoning are being developed. For sure, there is a shortage of convincing applications and a lack of tool support, but these are early days. The prospect of a methodogical convergence is, I believe, of major disciplinary significance. So with the dying strains of wheeled suitcases being dragged over cobble stones by exhausted tourists (a characteristic venetian sound), with a Bellini in hand and a plate of bigoli with an anchovy salsa in prospect, I eagerly await further developments.