942 research outputs found
A Logical Verification Methodology for Service-Oriented Computing
No full textWe introduce a logical verification methodology for checking behavioural properties of service-oriented computing systems. Service properties are described by means of SocL, a branching-time temporal logic that we have specifically designed to express in an effective way distinctive aspects of services, such as, e.g., acceptance of a request, provision of a response, and correlation among service requests and responses. Our approach allows service properties to be expressed in such a way that
they can be independent of service domains and specifications. We show an instantiation of our general methodology that uses the formal language COWS to conveniently specify services and the expressly developed software tool CMC to assist the user in the task of verifying SocL formulae over service specifications. We demonstrate feasibility and effectiveness of our methodology by means of the specification and the analysis of a case study in the automotive domain
A Model Checking Approach for Verifying COWS Specifications
No full textWe introduce a logical verification framework for checking functional properties of service-oriented applications formally specified using the service specification language COWS. The properties are described by means of SocL, a logic specifically designed to capture peculiar aspects of services. Service behaviours are abstracted in terms of Doubly Labelled Transition Systems, which are used as the interpretation domain for SocL formulae. We also illustrate the SocL model checker at work on a bank service scenario specified in COWS
Deformations of semi-smooth varieties
No full textFor a singular variety X, an essential step to determine its smoothability and study its deformations is the understanding of the tangent sheaf and of the sheaf T-X(1) := epsilon(l)(xt) (Omega(X), O-X). A variety is semi-smooth if its singularities are etale locally the product of a double crossing point (uv = 0) or a pinch point (u(2) - v(2)w = 0) with affine space; equivalently, if it can be obtained by gluing a smooth variety along a smooth divisor via an involution with smooth quotient. Our main result is the explicit computation of the tangent sheaf and the sheaf T(X)1 for a semi-smooth variety X in terms of the gluing data
A Framework to Evaluate 5G Networks for Smart and Fail-Safe Communications in ERTMS/ETCS
No full textETCS is an European system for high speed trains control and protection within ERTMS, the European standard for rail traffic management system. ERTMS/ETCS implementations use GSM-R for communications. As GSM-R is becoming obsolete, the adoption of more advanced technologies is investigated for next generation trains. New communication systems for railway infrastructures are expected to overcome the limitations of GSM-R, providing enhanced performance and reliability, as well as safety and security functionality to meet the requirements of the future signalling systems, control and users’ applications. While 4G technologies (LTE and LTE-A) are currently tested in a few field trials, railway operators should consider that fifth generation (5G) mobile communications technologies will soon be available. One of the foundational aspects of the 5G architecture is control-plane programmability, achieved through the SDN paradigm. Being aware that in a railway scenario this opportunity can be exploited to dynamically reconfigure the network behavior to better match the communication flows produced by moving trains, we aim at defining a framework, integrating formal modeling and analysis tools and techniques into a network emulator, to evaluate the impact on ERTMS/ETCS safety and security deriving from the adoption of an SDN model in the communication infrastructure. In this paper we describe a first step towards this objective, by presenting a first proof-of-concept implementation of the framework and its use to reproduce a simple railway infrastructure. In our current implementation, Finite State Machines are used to model communication protocols between ERTMS/ETCS entities and to automatically produce code and Promela models. Generated code is directly used to control the network behavior while the Promela model allows to generate and verify a network configuration by model checking
Imágenes a preservar en la tumba de Neferhotep (TT49)
No full textTabla de contenidos: El proyecto de conservación de la tumba de Neferhotep del Instituto de Investigaciones de Arte y Cultura del Oriente Antiguo / M. V. Pereyra. El monumento y su propietario / A. Zingarelli, S. Fantechi. Las expresiones plásticas en TT49 / N. Alzogaray, M. S. Vera. La preservación de la tumba de Neferhotep / S. Brinkmann, B. Graue, Chr. Verbeek. El universo de imágenes a recuperar en TT49 / M. V. Pereyra. La futura gestión del sitio / M. V. Pereyra.Fil: Zingarelli, Andrea. Universidad Nacional de La Plata. Facultad de Humanidades y Ciencias de la Educación; Argentina
The New Readout System of the NA62 LKr Calorimeter
No full textThe NA62 experiment [1] at CERN SPS (Super Proton Synchrotron) accelerator aims at studying Kaon decays with high precision. The high resolution Liquid Krypton (LKr) calorimeter, built for the NA48 [2] experiment, is a crucial part of the photon-veto system; to cope with the demanding NA62 re- quirements,itsback-endelectron icshadtobecompletelyrenewed. The new readout system is based on the Calorimeter REAdout Module (CREAM) [3], a 6U VME board whose design and pro- duction was sub-contracted to CAEN [4], with CERN NA62 group continuously supervising the de velopment and production phase. The first version of the board was delivered by the manufacturer in March 2013 and, as of June 2014, the full board production is ongoing. In addition to describing the CREAM board, all aspects of the new LKr readout system, including its integration within the NA62 TDAQ scheme, will be treated
A Vision of Intelligent Train Control
No full textThe progressive adoption of artificial intelligence and advanced communication technologies within railway control and automation has brought up a huge potential in terms of optimisation, learning and adaptation, due to the so-called “self-x” capabilities; however, it has also raised several dependability concerns due to the lack of measurable trust that is needed for certification purposes. In this paper, we provide a vision of future train control that builds upon existing automatic train operation, protection, and supervision paradigms. We will define the basic concepts for autonomous driving in digital railways, and summarise its feasibility in terms of challenges and opportunities, including explainability, autonomic computing, and digital twins. Due to the clear architectural distinction, automatic train protection can act as a safety envelope for intelligent operation to optimise energy, comfort, and capacity, while intelligent protection based on signal recognition and obstacle detection can improve safety through advanced driving assistance
Recommended from our members
Toric Stacks
No full textThe first purpose of this dissertation is to introduce and develop a theory of toric stacks which encompasses and extends the notions of toric stacks defined by Lafforgue, Borisov-Chen-Smith, Fantechi-Mann-Nironi, Iwanari, and Satriano, as well as classical toric varieties. In addition to introducing a broader class of smooth toric stacks, the definition we introduce allows singularities. The second purpose is to characterize toric stacks in a "bottom up" fashion, similar to the treatment of smooth toric Deligne-Mumford stacks by Fantechi-Mann-Nironi and the characterization of toric varieties as "abstract toric schemes" which are reduced, separated, and normal
Invisible Thermoplasmonic Indium Tin Oxide Nanoparticle Ink for Anti-counterfeiting Applications
No full textIn this study, we present a thermoplasmonic transparent ink based on a colloidal dispersion of indium tin oxide (ITO) nanoparticles, which can offer several advantages as anti-counterfeiting technology. The custom ink could be directly printed on several substrates, and it is transparent under visible light but is able to generate heat by absorption of NIR radiation. Dynamic temperature mapping of the printed motifs was performed by using a thermal camera while irradiating the samples with an IR lamp. The printed samples presented fine features (in the order of 75 μm) and high thermal resolution (of about 250 μm). The findings are supported by thermal finite-element simulations, which also allow us to explore the effect of different substrate characteristics on the thermal readout. Finally, we built a demonstrator comprising a QR Code invisible to the naked eye, which became visible in thermal images under NIR radiation. The high transparency of the printed ink and the high speed of the thermal reading (figures appear/disappear in less than 1 s) offer an extremely promising strategy toward low-cost, scalable production of photothermally active invisible labels
Chern Numbers of Uniruled Threefolds
No full textIn this paper we show that the Chern numbers of a smooth Mori fibre space in dimension three are bounded in terms of the underlying topological manifold. We also generalise a theorem of Cascini and the second named author on the boundedness of Chern numbers of certain threefolds to the case of negative Kodaira dimension
- …
