Abstract
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 verification might be possible. Less attention, however, has been devoted to the process of writing properties that accurately capture the requirements that need verification. This is however a crucial aspect of the verification process. Writing appropriate properties, in a logic suitable for verification, 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. Copyright

Abstract

Abstract
This paper presents a new Visual Notation for QUI modelling and testing (VAN4GUIM) which aims to hide, as much as possible, formalism details inherent to models used in model-based testing (MBT) approaches and to promote the use of MBT in industrial environments providing a visual front-end for modelling which is more attractive to testers than textual notation. This visual notation is developed as five different UML profiles and based on three notations/concepts: Canonical Abstract Prototyping notation; ConcurTaskTrees (CTT) notation; and the Window Manager concept. A set of translation rules was defined in order to automatically perform conversion from VAN4GUIM to Speck GUI models are developed with VAN4GUIM notation then translated automatically to Spec# that can be then completed manually with additional behaviour not included in the visual model. As soon as a Spec# model is completed, it can be used as input to Spec Explorer (model-based testing tool) which generates test cases and executes those tests automatically.

Abstract
Traveler attitudes and preferences as well as demographic variables are important components of travel behavior. By using travel attitudes, factor and cluster analyses were conducted to segment the sample. Six distinct groups were extracted: transit enthusiasts, anxious status seekers, carless riders, green cruisers, frugal travelers, and obstinate drivers. The segments showed unique combinations of attitudes with distinct travel behaviors and various degrees of intention to use public transportation. Gender differences were then investigated, and the results suggest that women and men exhibit differences in attitudes, preferences, and behaviors. The design of strategies to promote alternatives to car use should target the market segments that are most motivated to change, focusing on the attitudes that can induce a change, such as pro transit or sensibility to the environment.

Abstract
Height mapping of shallow water areas is an important task for many commercial and scientific applications like river navigability, infrastructure maintenance or natural resource monitoring. The use of an autonomous boat presents several advantages that case the use of synthetic aperture images to create three-dimensional topographic maps through interferometric techniques. Sample data obtained during test trials illustrate how synthetic aperture can be used to generate imagery and bathymetry data.

Abstract
Integrated optics is a mature technology with standard applications to telecommunications. Since the pioneering work of Berger et al. 1999 beam combiners for optical interferometry have been built using this technology. Classical integrated optics device production is very expensive and time consuming. The rapid production of devices using hybrid sol-gel materials in conjunction with UV laser direct writing techniques allows overcoming these limitations. In this paper this technology is tested for astronomical applications. We report on the design, fabrication and characterization of multiaxial two beam combiners and a coaxial beam combiner for astronomical interferometry. Different multiaxial two beam combiner designs were tested and high contrast (better than 90%) was obtained with a 1.3 mu m laser diode and with an SLID (lambda(0) = 1.26 mu m, FWHM of 60 nm). High contrast fringes were produced with 1.3 mu m laser diode using the coaxial two beam combiner. These results show that hybrid sol-gel techniques produce devices with high quality, allowing the rapid prototyping of new designs and concepts for astronomy.