Increasing urban cycling rates has become a main objective of mobility policies due to its contribution to social equity and sustainable urban travel. This objective can only be achieved if the activity is perceived as safe and convenient. The design of cycling routes projecting this perception depends on knowing how people move in the city and what the city looks like. However, acquiring such knowledge is challenging since it is distributed in an open set of heterogeneous data sources belonging to a variety of organizations. This paper documents the first step in an ontology-based data access (OBDA)approach to this problem, i.e., it describes the development of an ontology to support the design of cycling routes in the city of Puerto Madryn. We assume a set of competence questions that urban designers are likely to formulate in this context to understand the mobility needs of Puerto Madryn's inhabitants and the different alternatives they have to design cycling routes covering such needs. We derive concepts, relations, attributes and instances from these questions and characterize them using natural language. We specify the resulting ontology using Graphol, a graphic language for OWL 2 developed as part of an OBDA tool stack.

Introducción y objetivosEl secuestro pulmonar es una malformación congénita poco frecuente, caracterizada por un segmento anormal de tejido broncopulmonar irrigado por una arteria aberrante de origen sistémico, proveniente en la mayoría de los casos de la aorta descendente y menos comúnmente del tronco celíaco. Queremos mostrar nuestra experiencia en el manejo quirúrgico de un paciente con secuestro pulmonar intralobar con suplencia arterial proveniente del tronco celíaco, junto a una revisión narrativa de la literatura.ResultadoPresentamos un paciente de 24 años, sin antecedentes de importancia, con cuadro de una semana de evolución de síntomas respiratorios bajos, dolor pleurítico en el hemitórax izquierdo y fiebre subjetiva. Se inicia tratamiento antibiótico empírico por sospecha de neumonía por hallazgos en la radiografía de tórax, sin embargo, por un empeoramiento del cuadro clínico se realiza TAC de tórax contrastada que muestra neumonía necrosante de lóbulo inferior izquierdo. La reconstrucción tridimensional evidencia vasculatura supernumeraria proveniente del tronco celíaco que confluye a lóbulo inferior izquierdo. Cirugía de Tórax realiza toracotomía posterolateral izquierda con hallazgos que se correlacionan con imágenes diagnósticas. El procedimiento no presentó complicaciones y el seguimiento de 3 meses postoperatorio evidencia función pulmonar normal sin complicaciones.ConclusionesEl secuestro pulmonar es una malformación congénita poco frecuente, con una clínica inespecífica, que debe sospecharse ante la presencia de neumonías recurrentes que no responden al manejo antibiótico habitual. La conducta quirúrgica es la más utilizada, sin embargo, se debe individualizar el caso para favorecer los resultados.

El diseño arquitectónico de videojuegos es complejo. Es normal que los videojuegos se proyecten para ser ejecutados sobre una amplia variedad de dispositivos, sistemas operativos, e interpretes. A su vez, siempre se utilizan componentes de software – llamados motores – que proveen un número de funcionalidades básicas, pero plantean limitaciones sobre la plataforma y el entorno de desarrollo. Esto se combina con requerimientos de performance, y en muchos casos de escalabilidad, naturales en este dominio. Por otro lado, los equipos de desarrollo son tipicamente multidisciplinares, lo que dificulta la comunicación de decisiones de diseño. Esta línea plantea la investigación y desarrollo de ontologías para dirigir el diseño arquitectónico de videojuegos. Estas ontologías explicitarán y alinearán las conceptualizaciones utilizadas por las disciplinas involucradas, facilitarán la integración de datos sobre los artefactos relacionados al diseño, y proveerán una teoría lógica para guiar parte del diseño Palabras clave: ontología, videojuegos, diseño arquitectónico.

This paper studies the problem of verifying temporal properties (including liveness properties) of parametrized concurrent systems executed by an unbounded number of threads. To solve this problem we introduce parametrized verification diagrams (PVDs), that extend the so-called generalized verification diagrams (GVDs) adding support for parametrized verification. Even though GVDs are known to be a sound and complete proof system for non-parametrized systems, the application of GVDs to parametrized systems requires using quantification or finding a potentially different diagram for each instantiation of the parameter (number of threads). As a consequence, the use of GVDs in parametrized verification requires discharging and proving either quantified formulas or an unbounded collection of verification conditions. Parametrized verification diagrams enable the use of asinglediagram to represent the proof that all possible instances of the parametrized concurrent system satisfy the given temporal specification. Checking the proof represented by a PVD requires proving only a finite collection of quantifier-free verification conditions. The PVDs we present here assume that the parametrized systems are symmetric, which covers a large class of concurrent and distributed systems, including concurrent data types. Our second contribution is an implementation of PVDs and its integration into Leap, our prototype theorem prover. Finally, we illustrate empirically, using Leap, the practical applicability of PVDs by building and checking proofs of liveness properties of mutual exclusion protocols and concurrent data structures. To the best of our knowledge, these are the first machine-checkable proofs of liveness properties of these concurrent data types.

This article presents design decisions for an ontology-based framework supporting an expert-driven approach to the collaborative acquisition, integration and analysis of information. It describes a three-tier organization in which components facilitate establishing an information system to assist domain experts in addressing multi-causal dynamic situations where heterogeneous information sources must be integrated and the interaction of a variety of actors must be supported in large geographical areas with possibly low or intermittent connectivity levels. The approach and envisioned framework are illustrated with a case-study in the design of bikeways in urban zones.

Knowledge management is key for any organization. Huge amount of data is made available to organizations by pervasive technologies such as smart mobile devices. However, the knowledge to use such data is still missing, and organizations typically fail to exploit it. This paper proposes an architectural design that aims at addressing such problem. It focuses on knowledge management for collaborative systems in which complex and multicausal situations are presented to interacting actors on a large geographical area with possible low connectivity.

El aprendizaje móvil introduce la posibilidad de aprovechar situaciones y contenidos fuera de las aulas, de manera de motivar e involucrar al alumno de nuevas formas. Sin embargo, su adopción es lenta o inexistente. Una de las barreras que explica esta lenta adopción, es la distancia que existe entre la conceptualización que maneja el docente, y la que se requiere para seleccionar una aplicación educativa móvil que se ajuste al entorno educativo de dicho docente. Esta línea de I-D-I plantea utilizar aplicaciones basadas en ontologías para reducir esa distancia conceptual. Esto involucra desarrollar ontologías y prototipos de aplicaciones para anotar el software educativo, y para luego seleccionar los que respondan a una descripción.

1 Dep. de Ing. Eléctrica y Computadoras, Instituto de Inv. en Ingeniería Eléctrica, Universidad Nacional del Sur Av. Alem 1253 Bahía Blanca, (0291) 4595101 ierms@criba.edu.ar 2 Laboratorio de Investigación en Informática (LINVI), Departamento de Informática, UNPSJB Bvd Brown 2051 Puerto Madryn, (0280) 4883585 leo.ordinez@gmail.com, damian_barry@unpata.edu.ar, sergio.firmenich@gmail.com, nahuel.defosse@gmail.com, aljsanchez@gmail.com, robertoc.voogt@gmail.com

Continuous evolution towards very large, heterogeneous, highly dynamic computing systems entails the need for sound and flexible approaches to deal with system modification and re-engineering. The approach proposed in this paper combines an analysis stage, to identify concrete patterns of interaction in legacy code, with an iterative re-engineering process at a higher level of abstraction. Both stages are supported by the tools CoordPat and Archery, respectively. Bi-directional model transformations connecting code level and design level architectural models are defined. The approach is demonstrated in a (fragment of a) case study.

Architectural (bad) smells are design decisions found in software architectures that degrade the ability of systems to evolve. This paper presents an approach to verify that a software architecture is smell-free using the Archery architectural description language. The language provides a core for modelling software architectures and an extension for specifying constraints. The approach consists in precisely specifying architectural smells as constraints, and then verifying that software architectures do not satisfy any of them. The constraint language is based on a propositional modal logic with recursion that includes: a converse operator for relations among architectural concepts, graded modalities for describing the cardinality in such relations, and nominals referencing architectural elements. Four architectural smells illustrate the approach.

In a reconfigurable system, the response to contextual or internal change may trigger reconfiguration events which, on their turn, activate scripts that change the system׳s architecture at runtime. To be safe, however, such reconfigurations are expected to obey the fundamental principles originally specified by its architect. This paper introduces an approach to ensure that such principles are observed along reconfigurations by verifying them against concrete specifications in a suitable logic. Architectures, reconfiguration scripts, and principles are specified in Archery, an architectural description language with formal semantics. Principles are encoded as constraints, which become formulas of a two-layer graded hybrid logic, where the upper layer restricts reconfigurations, and the lower layer constrains the resulting configurations. Constraints are verified by translating them into logic formulas, which are interpreted over models derived from Archery specifications of architectures and reconfigurations. Suitable notions of bisimulation and refinement, to which the architect may resort to compare configurations, are given, and their relationship with modal validity is discussed.

ARCHERY is an architectural description language for modelling and reasoning about distributed, heterogeneous and dynamically reconfigurable systems in terms of architectural patterns. The language supports the specification of architectures and their reconfiguration. This paper introduces a language extension for precisely describing the structural design decisions that pattern instances must respect in their (re)configurations. The extension is a propositional modal logic with recursion and nominals referencing components, i.e., a hybrid mu-calculus. Its expressiveness allows specifying safety and liveness constraints, as well as paths and cycles over structures. Refinements of classic architectural patterns are specified.