Abstract
In this paper we present a computer assisted proof of the correctness of a partial derivative automata construction from a regular expression within the Coq proof assistant. Tins proof is part of a formalization of Kleene algebra and regular languages in Coq towards their usage in program certification.

Abstract
This paper is concerned with the scaleable and systematic analysis of interactive systems. The motivating problem is the procurement of medical devices. In such situations several different manufacturers offer solutions that support a particular clinical activity. Apart from cost, which is a dominating factor, the variations between devices are relatively subtle and the consequences of particular design features are not clear from manufacturers' manuals, demonstrations or trial uses. Despite their subtlety these differences can be important to the safety and usability of the device. The paper argues that formal analysis of the range of offered devices can provide a systematic means of comparison. The paper also explores barriers to the use of such techniques, demonstrating how layers of specification may be used to make it possible to reuse common specification. Infusion pumps provide a motivating example. A specific model is described and analysed and comparison between competitive devices is discussed. © Formal Methods for Interactive Systems 2011.

Abstract
The design of safe industrial controllers is one of the most important domains related to Automation Systems research. To support it, synthesis and analysis techniques are available. Among the analysis techniques, two of the most important are Simulation and Formal Verification. In this paper these two techniques are used together in a complementary way. Understanding plant behaviour is essential for obtaining safe industrial systems controllers: hence, plant modelling is crucial to the success of these techniques. A two step approach is presented: first, the use of Simu ation and, second, the use of Formal Verification of Industrial Systems Specifications. The specification and plant models used for each technique are described. Simulation and Formal Verification results are presented and discussed. The approach presented in the paper can be applied to real industrial systems, and obtain safe controllers for hybrid plants. The Modelica modelling language and Dymola simulation environment are used for Simulation purposes, and Timed Automata formalism and the UPPAAL real-time model-checker are used for Formal Verification purposes.

Abstract
This paper describes an approach to the model-based testing of graphical user interfaces from task models. Starting from a task model of the system under test, oracles are generated whose behaviour is compared with the execution of the running system. The use of task models means that the effort of producing the test oracles is reduced. It does also mean, however, that the oracles are confined to the set of expected user behaviours for the system. The paper focuses on solving this problem. It shows how task mutations can be generated automatically, enabling a broader range of user behaviours to be considered. A tool, based on a classification of user errors, generates these mutations. A number of examples illustrate the approach. Copyright 2011 ACM.

Abstract
It is increasingly common to find research on the usability of E-learning systems. From the results of these investigations, it seems clear that most of them point to the need for a critical discussion about usability evaluation methods for specific education systems, particularly on the importance of methods focus on the primary users. However, it also seems to be urgent and essential to investigate how ergonomic analysis has been applied, as well as the necessary adaptations to such usability analysis methods, in order to set up assessments which are more consistent with the nature of the systems. It is now known that, in general terms, users go through several stages of interaction with the system throughout the period of tasks execution. In each of these interaction phases, their behavior and actions can lead them to success, or failure, with regard to compliance with the pre-set goals. Many of the commonly used usability evaluation methods do not stop to analyze the interactions occurring in the context of use. This paper presents a critical review of usability evalution for E-learning systems.

Abstract
Problem statements often resort to superlatives such as in eg. "...the smallest such number", "...the best approximation", "...the longest such list" which lead to specifications made of two parts: one defining a broad class of solutions (the easy part) and the other requesting the optimal such solution (the hard part). This paper introduces a binary relational combinator which mirrors this linguistic structure and exploits its potential for calculating programs by optimization. This applies in particular to specifications written in the form of Galois connections, in which one of the adjoints delivers the optimal solution being sought. The framework encompasses re-factoring of results previously developed by Bird and de Moor for greedy and dynamic programming, in a way which makes them less technically involved and therefore easier to understand and play with. © 2011 Springer-Verlag.