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
The user experience of ubiquitous environments is a determining factor in their success. The characteristics of such systems must be explored as early as possible to anticipate potential user problems, and to reduce the cost of redesign. However, the development of early prototypes to be evaluated in the target environment can be disruptive to the ongoing system and therefore unacceptable. This paper reports on an ongoing effort to explore how model-based rapid prototyping of ubiquitous environments might be used to avoid actual deployment while still enabling users to interact with a representation of the system. The paper describes APEX, a framework that brings together an existing 3D Application Server with CPN Tools. APEX-based prototypes enable users to navigate a virtual world simulation of the envisaged ubiquitous environment. The APEX architecture and the proposed CPN-based modelling approach are described. An example illustrates their use.

Abstract
The current diversity of available devices and form factors increases the need for model-based techniques to support adapting applications from one device to another. Most work on user interface modelling is built around declarative markup languages. Markup languages play a relevant role, not only in the modelling of user interfaces, but also in their implementation. However, the languages used by each community (modellers/developers) have, to a great extent evolved separately. This means that the step from concrete model to final interface becomes needlessly complicated, requiring either compilers or interpreters to bridge this gap. In this paper we compare a modelling language (UsiXML) with several markup implementation languages. We analyse if it is feasible to use the implementation languages as modelling languages. © 2012 Springer-Verlag.

Abstract
Ubiquitous computing (ubicomp) systems involve complex interactions between multiple devices and users. This complexity makes it difficult to establish whether: (1) observations made about use are truly representative of all possible interactions; (2) desirable characteristics of the system are true in all possible scenarios. To address these issues, techniques are needed that support an exhaustive analysis of a system's design. This paper demonstrates one such exhaustive analysis technique that supports the early evaluation of alternative designs for ubiquitous computing environments. The technique combines models of behavior within the environment with a virtual world that allows its simulation. The models support checking of properties based on patterns. These patterns help the analyst to generate and verify relevant properties. Where these properties fail then scenarios suggested by the failure provide an important aid to redesign. The proposed technique uses APEX, a framework for rapid prototyping of ubiquitous environments based on Petri nets. The approach is illustrated through a smart library example. Its benefits and limitations are discussed. Copyright 2012 ACM.

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.