Carlos E. Silva

Engineering correct software is one of the grand challenges of computer science. Practical design and verification methodologies to ensure correct software can have a substantial impact on how programs are built by the industry. As human-machine systems become more functional, they also become more complex. Consequently, the interactions between the machine and its users becomes less predictable and more difficult to analyse. Using Model Checking it is possible to automatically analyse the behaviour of a modelled system. Hence, different authors have investigated the applicability of model checking to the analysis of human-machine interactions. The IVY workbench is a tool that supports system design and verification, by providing a model checking based integrated modelling and analysis environment. The tool is based around a plugin architecture, and although it features a verification results' analyser, it thus far lacked the ability to visually expose the sequence of events that lead to a system failure on a system's prototype. We propose the AniMAL plugin as an extension to the IVY workbench, providing automatic user interface prototyping and verification results' animation, while allowing thorough customisation.

In recent years, several approaches to the analysis of automation systems dependability through the application of formal verification techniques have been proposed. Much of the research has been concerned with the modelling languages used, and how best to express the automation systems, so that automated verication might be possible. Less attention, however, has been devoted to the process of writing properties that accurately capture the requirements that need verication. This is however a crucial aspect of the verication process. Writing appropriate properties, in a logic suitable for verication, is a skilful process, and indeed there have been reports of properties being wrongly expressed. In this paper we put forward a tool and a collection of property patterns that aim at providing help in this area.

In recent years, advances in software tools have made it easier to analyze interactive system specifications, and the range of their possible behaviors. However, the effort involved in producing the specifications of the system is still substantial, and a difficulty exists regarding the specification of plausible behaviors on the part of the user. Recent trends in technology towards more mobile and distributed systems further exacerbates the issue, as contextual factors come in to play, and less structured, more opportunistic behavior on the part of the user makes purely task-based analysis difficult. In this paper we consider a resourced action approach to specification and analysis. In pursuing this approach we have two aims - firstly, to facilitate a resource-based analysis of user activity, allowing resources to be distributed across a number of artifacts, and secondly to consider within the analysis a wider range of plausible and opportunistic user behaviors without a heavy specification overhead, or requiring commitment to detailed user models.

We propose a new hybrid protocol for cryptographically secure biometric authentication. The main advantages of the proposed protocol over previous solutions can be summarised as follows: (1) potential for much better accuracy using different types of biometric signals, including behavioural ones; and (2) improved user privacy, since user identities are not transmitted at any point in the protocol execution. The new protocol takes advantage of state-of-the-art identification classifiers, which provide not only better accuracy, but also the possibility to perform authentication without knowing who the user claims to be. Cryptographic security is based on the Paillier public key encryption scheme.

Many interesting emerging applications involve the coordination of a large number of service instances, for instance, as targets for dissemination or sources in information gathering. These applications raise hard architectural, scalability, and resilience issues that are not suitably addressed by centralized or monolithic coordination solutions.

In this paper we propose a lightweight approach to service coordination aimed at such application scenarios. It is based on gossiping and thus potentially fully decentralized, requiring that each participant is concerned only with a small number of peers. Although being obviously simple and scalable, it has been shown that gossip-based protocols lead to emergent strong resilience guarantees.

We illustrate the approach with WS--PushGossip, a proof-of-concept coordination protocol based upon the WS--Coordination framework. Besides presenting WS--PushGossip, we illustrate its usefulness with a sample application, and outline a middleware implementation based on Apache Axis2.

Unstructured overlay networks are a key component of many peer-to-peer systems. These overlays exhibit a set of interesting properties that derive from their inherent randomness. In this fast abstract we briefly discuss the key aspects that need to be considered when attempting to bias the structure of unstructured networks, such that it becomes possible to improve the efficiency of applications and services executed at the top level, without impairing the correctness of the overlay.

Galculator is the name of the prototype of a proof assistant of a special brand: it is solely based on the algebra of Galois connections. When combined with the pointfree transform and tactics such as the indirect equality principle, Galois connections offer a very powerful, generic device to tackle the complexity of proofs in program verification. The paper describes the architecture of the current Galculator prototype, which is implemented in Haskell in order to steer types as much as possible. The prospect of integrating the Galculator with other proof assistants such as e.g. Coq is also discussed.