A model of air transport passenger incidents and rights

This paper describes a representation of the legal framework in the air transport passenger's rights domain and the foremost incidents that trigger the top of consumer complaints ranking in the EU. It comprises the development of a small network of three ontologies, formalisation of scenarios, specification of properties and identification of relations. The approach is illustrated by means of a case study based in the context of a real life cancelled flight incident. This is part of an intended support-system that aims to provide both consumers and companies with relevant legal information to enhance the decision-making process.

Design of a generalized tool for the performance assessment under sail based on analytical, numerical and empirical results : a global sailing yacht meta-model

La evaluación de las prestaciones de las embarcaciones a vela ha constituido un objetivo para ingenieros navales y marinos desde los principios de la historia de la navegación. El conocimiento acerca de estas prestaciones, ha crecido desde la identificación de los factores clave relacionados con ellas(eslora, estabilidad, desplazamiento y superficie vélica), a una comprensión más completa de las complejas fuerzas y acoplamientos involucrados en el equilibrio. Junto con este conocimiento, la aparición de los ordenadores ha hecho posible llevar a cabo estas tareas de una forma sistemática. Esto incluye el cálculo detallado de fuerzas, pero también, el uso de estas fuerzas junto con la descripción de una embarcación a vela para la predicción de su comportamiento y, finalmente, sus prestaciones. Esta investigación tiene como objetivo proporcionar una definición global y abierta de un conjunto de modelos y reglas para describir y analizar este comportamiento. Esto se lleva a cabo sin aplicar restricciones en cuanto al tipo de barco o cálculo, sino de una forma generalizada, de modo que sea posible resolver cualquier situación, tanto estacionaria como en el dominio del tiempo. Para ello se comienza con una definición básica de los factores que condicionan el comportamiento de una embarcación a vela. A continuación se proporciona una metodología para gestionar el uso de datos de diferentes orígenes para el cálculo de fuerzas, siempre con el la solución del problema como objetivo. Esta última parte se plasma en un programa de ordenador, PASim, cuyo propósito es evaluar las prestaciones de diferentes ti pos de embarcaciones a vela en un amplio rango de condiciones. Varios ejemplos presentan diferentes usos de PASim con el objetivo de ilustrar algunos de los aspectos discutidos a lo largo de la definición del problema y su solución . Finalmente, se presenta una estructura global de cara a proporcionar una representación virtual de la embarcación real, en la cual, no solo e l comportamiento sino también su manejo, son cercanos a la experiencia de los navegantes en el mundo real. Esta estructura global se propone como el núcleo (un motor de software) de un simulador físico para el que se proporciona una especificación básica. ABSTRACT The assessment of the performance of sailing yachts, and ships in general, has been an objective for naval architects and sailors since the beginning of the history of navigation. The knowledge has grown from identifying the key factors that influence performance(length, stability, displacement and sail area), to a much more complete understanding of the complex forces and couplings involved in the equilibrium. Along with this knowledge, the advent of computers has made it possible to perform the associated tasks in a systematic way. This includes the detailed calculation of forces, but also the use of those forces, along with the description of a sailing yacht, to predict its behavior, and ultimately, its performance. The aim of this investigation is to provide a global and open definition of a set of models and rules to describe and analyze the behavior of a sailing yacht. This is done without applying any restriction to the type of yacht or calculation, but rather in a generalized way, capable of solving any possible situation, whether it is in a steady state or in the time domain. First, the basic definition of the factors that condition the behavior of a sailing yacht is given. Then, a methodology is provided to assist with the use of data from different origins for the calculation of forces, always aiming towards the solution of the problem. This last part is implemented as a computational tool, PASim, intended to assess the performance of different types of sailing yachts in a wide range of conditions. Several examples then present different uses of PASim, as a way to illustrate some of the aspects discussed throughout the definition of the problem and its solution. Finally, a global structure is presented to provide a general virtual representation of the real yacht, in which not only the behavior, but also its handling is close to the experience of the sailors in the real world. This global structure is proposed as the core (a software engine) of a physical yacht simulator, for which a basic specification is provided.

Establishment of medaka (Oryzias latipes) transgenic lines with the expression of green fluorescent protein fluorescence exclusively in germ cells: A useful model to monitor germ cells in a live vertebrate

We have generated transgenic medaka (teleost, Oryzias latipes), which allow us to monitor germ cells by green fluorescent protein (GFP) fluorescence in live specimens. Two medaka strains, himedaka (orange–red variety) and inbred QurtE, were used. The transgenic lines were achieved by microinjection of a construct containing the putative promoter region and 3′ region of the medaka vasa gene (olvas). The intensity of GFP fluorescence increases dramatically in primordial germ cells (PGCs) located in the ventrolateral region of the posterior intestine around stage 25 (the onset of blood circulation). Whole-mount in situ hybridization and monitoring of ectopically located cells by GFP fluorescence suggested that (i) the increase in zygotic olvas expression occurs after PGC specification and (ii) PGCs can maintain their cell characteristics ectopically after stages 20–25. Around the day of hatching, the QurtE strain clearly exhibits sexual dimorphisms in the number of GFP fluorescent germ cells, a finding consistent with the appearance of leucophores, a sex-specific marker of QurtE. The GFP expression persists throughout the later stages in the mature ovary and testis. Thus, these transgenic medaka represent a live vertebrate model to investigate how germ cells migrate to form sexually dimorphic gonads, as well as a potential assay system for environmental substances that may affect gonad development. The use of a transgenic construct as a selective marker to efficiently isolate germ-line-transmitting founders during embryogenesis is also discussed.

Regulation of the myeloperoxidase enhancer binding proteins Pu1, C-EBP alpha, -beta, and -delta during granulocyte-lineage specification.

We have compared the molecular architecture and function of the myeloperoxidase upstream enhancer in multipotential versus granulocyte-committed hematopoietic progenitor cells. We show that the enhancer is accessible in multipotential cell chromatin but functionally incompetent before granulocyte commitment. Multipotential cells contain both Pu1 and C-EBP alpha as enhancer-binding activities. Pu1 is unphosphorylated in both multipotential and granulocyte-committed cells but is phosphorylated in B lymphocytes, raising the possibility that differential phosphorylation may play a role in specifying its lymphoid versus myeloid functions. C-EBP alpha exists as multiple phosphorylated forms in the nucleus of both multipotential and granulocyte-committed cells. C-EBP beta is unphosphorylated and cytoplasmically localized in multipotential cells but exists as a phosphorylated nuclear enhancer-binding activity in granulocyte-committed cells. Granulocyte colony-stimulating factor-induced granulocytic differentiation of multipotential progenitor cells results in activation of C-EBP delta expression and functional recruitment of C-EBP delta and C-EBP beta to the nucleus. Our results implicate Pu1 and the C-EBP family as critical regulators of myeloperoxidase gene expression and are consistent with a model in which a temporal exchange of C-EBP isoforms at the myeloperoxidase enhancer mediates the transition from a primed state in multipotential cells to a transcriptionally active configuration in promyelocytes.

Boston, Massachusetts Region, Digital Elevation Model with Bathymetry

This raster layer represents surface elevation and bathymetry data for the Boston Region, Massachusetts. It was created by merging portions of MassGIS Digital Elevation Model 1:5,000 (2005) data with NOAA Estuarine Bathymetric Digital Elevation Models (30 m.) (1998). DEM data was derived from the digital terrain models that were produced as part of the MassGIS 1:5,000 Black and White Digital Orthophoto imagery project. Cellsize is 5 meters by 5 meters. Each cell has a floating point value, in meters, which represents its elevation above or below sea level.

A framework and tool support for the systematic testing of model-based specifications

Formal specifications can precisely and unambiguously define the required behavior of a software system or component. However, formal specifications are complex artifacts that need to be verified to ensure that they are consistent, complete, and validated against the requirements. Specification testing or animation tools exist to assist with this by allowing the specifier to interpret or execute the specification. However, currently little is known about how to do this effectively. This article presents a framework and tool support for the systematic testing of formal, model-based specifications. Several important generic properties that should be satisfied by model-based specifications are first identified. Following the idea of mutation analysis, we then use variants or mutants of the specification to check that these properties are satisfied. The framework also allows the specifier to test application-specific properties. All properties are tested for a range of states that are defined by the tester in the form of a testgraph, which is a directed graph that partially models the states and transitions of the specification being tested. Tool support is provided for the generation of the mutants, for automatically traversing the testgraph and executing the test cases, and for reporting any errors. The framework is demonstrated on a small specification and its application to three larger specifications is discussed. Experience indicates that the framework can be used effectively to test small to medium-sized specifications and that it can reveal a significant number of problems in these specifications.

The specification of vector autoregressive moving average models

In this paper we propose a new identification method based on the residual white noise autoregressive criterion (Pukkila et al. , 1990) to select the order of VARMA structures. Results from extensive simulation experiments based on different model structures with varying number of observations and number of component series are used to demonstrate the performance of this new procedure. We also use economic and business data to compare the model structures selected by this order selection method with those identified in other published studies.

Forecasting stock returns using model-selection criteria

This paper examines the economic significance of return predictability in Australian equities. In light of considerable model uncertainty, formal model-selection criteria are used to choose a specification for the predictive model. A portfolio-switching strategy is implemented according to model predictions. Relative to a buy-and-hold market investment, the returns to the portfolio-switching strategy are impressive under several model-selection criteria, even after accounting for transaction costs. However, as these findings are not robust across other model-selection criteria examined, it is difficult to conclude that the degree of return predictability is economically significant.

Rice morphogenesis and plant architecture: Measurement, specification and the reconstruction of structural development by 3D architectural modelling

Background and Aims The morphogenesis and architecture of a rice plant, Oryza sativa, are critical factors in the yield equation, but they are not well studied because of the lack of appropriate tools for 3D measurement. The architecture of rice plants is characterized by a large number of tillers and leaves. The aims of this study were to specify rice plant architecture and to find appropriate functions to represent the 3D growth across all growth stages. Methods A japonica type rice, 'Namaga', was grown in pots under outdoor conditions. A 3D digitizer was used to measure the rice plant structure at intervals from the young seedling stage to maturity. The L-system formalism was applied to create '3D virtual rice' plants, incorporating models of phenological development and leaf emergence period as a function of temperature and photoperiod, which were used to determine the timing of tiller emergence. Key Results The relationships between the nodal positions and leaf lengths, leaf angles and tiller angles were analysed and used to determine growth functions for the models. The '3D virtual rice' reproduces the structural development of isolated plants and provides a good estimation of the fillering process, and of the accumulation of leaves. Conclusions The results indicated that the '3D virtual rice' has a possibility to demonstrate the differences in the structure and development between cultivars and under different environmental conditions. Future work, necessary to reflect both cultivar and environmental effects on the model performance, and to link with physiological models, is proposed in the discussion.

Specification and validation of process constraints for flexible workflows

Workflow systems have traditionally focused on the so-called production processes which are characterized by pre-definition, high volume, and repetitiveness. Recently, the deployment of workflow systems in non-traditional domains such as collaborative applications, e-learning and cross-organizational process integration, have put forth new requirements for flexible and dynamic specification. However, this flexibility cannot be offered at the expense of control, a critical requirement of business processes. In this paper, we will present a foundation set of constraints for flexible workflow specification. These constraints are intended to provide an appropriate balance between flexibility and control. The constraint specification framework is based on the concept of pockets of flexibility which allows ad hoc changes and/or building of workflows for highly flexible processes. Basically, our approach is to provide the ability to execute on the basis of a partially specified model, where the full specification of the model is made at runtime, and may be unique to each instance. The verification of dynamically built models is essential. Where as ensuring that the model conforms to specified constraints does not pose great difficulty, ensuring that the constraint set itself does not carry conflicts and redundancy is an interesting and challenging problem. In this paper, we will provide a discussion on both the static and dynamic verification aspects. We will also briefly present Chameleon, a prototype workflow engine that implements these concepts. (c) 2004 Elsevier Ltd. All rights reserved.

Product performance and specification in new product development

This paper deals with product performance and specification in new product development. There are many different definitions of performance and specification in the literature. These are reviewed and a new classification scheme for product performance is proposed. The link between performance and specification is discussed in detail using a new model for the new product development process. The new model involves two stages, with each containing three main phases, and is useful for making decisions with regards to product performance and specification.

Verifying data refinements using a model checker

In this paper, we consider how refinements between state-based specifications (e.g., written in Z) can be checked by use of a model checker. Specifically, we are interested in the verification of downward and upward simulations which are the standard approach to verifying refinements in state-based notations. We show how downward and upward simulations can be checked using existing temporal logic model checkers. In particular, we show how the branching time temporal logic CTL can be used to encode the standard simulation conditions. We do this for both a blocking, or guarded, interpretation of operations (often used when specifying reactive systems) as well as the more common non-blocking interpretation of operations used in many state-based specification languages (for modelling sequential systems). The approach is general enough to use with any state-based specification language, and we illustrate how refinements between Z specifications can be checked using the SAL CTL model checker using a small example.

A case study in specification and implementation testing

Achieving consistency between a specification and its implementation is an important part of software development In previous work, we have presented a method and tool support for testing a formal specification using animation and then verifying an implementation of that specification. The method is based on a testgraph, which provides a partial model of the application under test. The testgraph is used in combination with an animator to generate test sequences for testing the formal specification. The same testgraph is used during testing to execute those same sequences on the implementation and to ensure that the implementation conforms to the specification. So far, the method and its tool support have been applied to software components that can be accessed through an application programmer interface (API). In this paper, we use an industrially-based case study to discuss the problems associated with applying the method to a software system with a graphical user interface (GUI). In particular, the lack of a standardised interface, as well as controllability and observability problems, make it difficult to automate the testing of the implementation. The method can still be applied, but the amount of testing that can be carried on the implementation is limited by the manual effort involved.

Partial completion of activity in business process specification

We examine the current workflow modelling capability from a new angle and demonstrate a weakness of current workflow specification languages in relation to execution of activities. This shortcoming is mainly due to serious limitations of the corresponding computational/execution model behind the business process modelling language constructs. The main purpose of this paper is the introduction of new specification/modelling constructs allowing for more precise representation of complex activity states during its execution. This new concept enables visibility of a new activity state–partial completion of activity, which in turn allows for a more flexible and precise enforcement/monitoring of automated business processes.

Model checking Z specifications using SAL

The Symbolic Analysis Laboratory (SAL) is a suite of tools for analysis of state transition systems. Tools supported include a simulator and four temporal logic model checkers. The common input language to these tools was originally developed with translation from other languages, both programming and specification languages, in mind. It is, therefore, a rich language supporting a range of type definitions and expressions. In this paper, we investigate the translation of Z specifications into the SAL language as a means of providing model checking support for Z. This is facilitated by a library of SAL definitions encoding the Z mathematical toolkit.