Abstract
As formal verification tools gain popularity, the problem arises of making them more accessible to engineers. A correct understanding of the logics in which properties are expressed is needed in order to guarantee that properties correctly encode the intent of the verification process. Writing appropriate properties, in a logic suitable for verification, is a skilful process. Errors in this step of the process can create serious problems since a false sense of security if gained with the analysis. However, when compared to the effort put into developing and applying modelling languages, little attention has been devoted to the process of writing properties that accurately capture verification requirements. This paper illustrates how a collection of property patterns, and its tool support, can help in simplifying the process of generating logical formulae from informally expressed requirements. © 2009 IFAC.

Abstract
Ubiquitous computing poses new usability challenges that cut across design and development. We are particularly interested in "spaces" enhanced with sensors, public displays and personal devices. How can prototypes be used to explore the user's mobility and interaction, both explicitly and implicitly, to access services within these environments? Because of the potential cost of development and design failure, the characteristics of such systems must be explored using early versions of the system that could disrupt if used in the target environment. Being able to evaluate these systems early in the process is crucial to their successful development. This paper reports on an effort to develop a framework for the rapid prototyping and analysis of ambient intelligence systems.

Abstract
This paper is concerned with support for the process of usability engineering. The aim is to use formal techniques to provide a systematic approach that is more traceable, and because it is systematic, repeatable. As a result of this systematic process some of the more subjective aspects of the analysis can be removed. The technique explores exhaustively those features of a specific design that fail to satisfy a set of properties. It also analyzes those aspects of the design where it is possible to quantify the cost of use. The method is illustrated using the example of a medical device. While many aspects of the approach and its tool support have already been discussed elsewhere, this paper builds on and contrasts an analysis of the same device provided by a third party and in so doing enhances the IVY tool.

Abstract
Automation systems according to IEC 61850 are a powerful solution for station automation. Engineering of such distributed systems is however a non-trivial task which requires different approaches and enhanced tool support. In this paper the authors (i) present how IEC 61850 is viewed and is being adopted by a utility and vendor, (ii) discuss its engineering potential and current issues, (iii) point-out global requirements for next generation tools, (iv) present the InPACT project which is tackling some of these concerns and (v) propose key elements of visual languages as one contributing enhancement.

Abstract

Abstract
A transition system can be presented either as a binary relation or as a coalgebra for the powerset functor, each representation being obtained from the other by transposition. More generally, a coalgebra for a functor F generalises transition systems in the sense that a shape for transitions is determined by F, typically encoding a signature of methods and observers. This paper explores such a duality to frame in purely relational terms coalgebraic refinement, showing that relational (data) refinement of transition relations, in its two variants, downward and upward (functional) simulations, is equivalent to coalgebraic refinement based on backward and forward morphisms, respectively. Going deeper, it is also shown that downward simulation provides a complete relational rule to prove coalgebraic refinement. With such a single rule the paper defines a pre-ordered calculus for refinement of coalgebras, with bisimilarity as the induced equivalence. The calculus is monotonic with respect to the main relational operators and arbitrary relator F, therefore providing a framework for structural reasoning about refinement.