Secure tracking for critical applications : communications, GPS and future Galileo services

Tracking/remote monitoring systems using GNSS are a proven method to enhance the safety and security of personnel and vehicles carrying precious or hazardous cargo. While GNSS tracking appears to mitigate some of these threats, if not adequately secured, it can be a double-edged sword allowing adversaries to obtain sensitive shipment and vehicle position data to better coordinate their attacks, and to provide a false sense of security to monitoring centers. Tracking systems must be designed with the ability to perform route-compliance and thwart attacks ranging from low-level attacks such as the cutting of antenna cables to medium and high-level attacks involving radio jamming and signal / data-level simulation, especially where the goods transported have a potentially high value to terrorists. This paper discusses the use of GNSS in critical tracking applications, addressing the mitigation of GNSS security issues, augmentation systems and communication systems in order to provide highly robust and survivable tracking systems.

Probabilistic verification of satellite systems for mission critical applications

In this thesis, we present a quantitative approach using probabilistic verification techniques for the analysis of reliability, availability, maintainability, and safety (RAMS) properties of satellite systems. The subject of our research is satellites used in mission critical industrial applications. A strong case for using probabilistic model checking to support RAMS analysis of satellite systems is made by our verification results. This study is intended to build a foundation to help reliability engineers with a basic background in model checking to apply probabilistic model checking to small satellite systems. We make two major contributions. One of these is the approach of RAMS analysis to satellite systems. In the past, RAMS analysis has been extensively applied to the field of electrical and electronics engineering. It allows system designers and reliability engineers to predict the likelihood of failures from the indication of historical or current operational data. There is a high potential for the application of RAMS analysis in the field of space science and engineering. However, there is a lack of standardisation and suitable procedures for the correct study of RAMS characteristics for satellite systems. This thesis considers the promising application of RAMS analysis to the case of satellite design, use, and maintenance, focusing on its system segments. Data collection and verification procedures are discussed, and a number of considerations are also presented on how to predict the probability of failure. Our second contribution is leveraging the power of probabilistic model checking to analyse satellite systems. We present techniques for analysing satellite systems that differ from the more common quantitative approaches based on traditional simulation and testing. These techniques have not been applied in this context before. We present the use of probabilistic techniques via a suite of detailed examples, together with their analysis. Our presentation is done in an incremental manner: in terms of complexity of application domains and system models, and a detailed PRISM model of each scenario. We also provide results from practical work together with a discussion about future improvements.

Enhancing the trust of location acquisition systems for critical applications and location-based security services

This paper identifies a number of critical infrastructure applications that are reliant on location services from cooperative location technologies such as GPS and GSM. We show that these location technologies can be represented in a general location model, such that the model components can be used for vulnerability analysis. We perform a vulnerability analysis on these components of GSM and GPS location systems as well as a number of augmentations to these systems.

From gearstick to joystick – Challenges in designing new interventions for the safety-critical driving context

Consumer electronics increasingly find their way into cars and are often portrayed as unwanted distractions. As part of our endeavour to capitalise on these technologies as safety tools rather than safety threats, we suggest to use smartphones, head-up displays, vehicle interfaces, and other digital gadgets: a) as readily available and lightweight sensing devices, and b) as platforms for engaging interventions that provide safe stimuli in real- time while driving. In our effort to make safe driving behaviours more fun, we explore ways to apply gamification to driving. In this paper, we illustrate the need for a careful balance between fun and safety and reveal ethical issues that arise when introducing new technology interventions into this complex and safety- critical design space.

Safety-critical medical device development using the UPP2SF model translation tool

Software-based control of life-critical embedded systems has become increasingly complex, and to a large extent has come to determine the safety of the human being. For example, implantable cardiac pacemakers have over 80,000 lines of code which are responsible for maintaining the heart within safe operating limits. As firmware-related recalls accounted for over 41% of the 600,000 devices recalled in the last decade, there is a need for rigorous model-driven design tools to generate verified code from verified software models. To this effect, we have developed the UPP2SF model-translation tool, which facilitates automatic conversion of verified models (in UPPAAL) to models that may be simulated and tested (in Simulink/Stateflow). We describe the translation rules that ensure correct model conversion, applicable to a large class of models. We demonstrate how UPP2SF is used in themodel-driven design of a pacemaker whosemodel is (a) designed and verified in UPPAAL (using timed automata), (b) automatically translated to Stateflow for simulation-based testing, and then (c) automatically generated into modular code for hardware-level integration testing of timing-related errors. In addition, we show how UPP2SF may be used for worst-case execution time estimation early in the design stage. Using UPP2SF, we demonstrate the value of integrated end-to-end modeling, verification, code-generation and testing process for complex software-controlled embedded systems. © 2014 ACM.

Digital radiography using digital detector arrays fulfills critical applications for offshore pipelines

Digital radiography in the inspection of welded pipes to be installed under deep water offshore gas and oil pipelines, like a presalt in Brazil, in the paper has been investigated. The aim is to use digital radiography for nondestructive testing of welds as it is already in use in the medical, aerospace, security, automotive, and petrochemical sectors. Among the current options, the DDA (Digital Detector Array) is considered as one of the best solutions to replace industrial films, as well as to increase the sensitivity to reduce the inspection cycle time. This paper shows the results of this new technique, comparing it to radiography with industrial films systems. In this paper, 20 test specimens of longitudinal welded pipe joints, specially prepared with artificial defects like cracks, lack of fusion, lack of penetration, and porosities and slag inclusions with varying dimensions and in 06 different base metal wall thicknesses, were tested and a comparison of the techniques was made. These experiments verified the purposed rules for parameter definitions and selections to control the required digital radiographic image quality as described in the draft international standard ISO/DIS 10893-7. This draft is first standard establishing the parameters for digital radiography on weld seam of welded steel pipes for pressure purposes to be used on gas and oil pipelines.

CRITICAL APPLICATIONS OF SW 846 US EPA METHODS TO EVALUATION OF MARINE SAMPLES QUALITY

Technical evaluation of analytical data is of extreme relevance considering it can be used for comparisons with environmental quality standards and decision-making as related to the management of disposal of dredged sediments and the evaluation of salt and brackish water quality in accordance with CONAMA 357/05 Resolution. It is, therefore, essential that the project manager discusses the environmental agency`s technical requirements with the laboratory contracted for the follow-up of the analysis underway and even with a view to possible re-analysis when anomalous data are identified. The main technical requirements are: (1) method quantitation limits (QLs) should fall below environmental standards; (2) analyses should be carried out in laboratories whose analytical scope is accredited by the National Institute of Metrology (INMETRO) or qualified or accepted by a licensing agency; (3) chain of custody should be provided in order to ensure sample traceability; (4) control charts should be provided to prove method performance; (5) certified reference material analysis or, if that is not available, matrix spike analysis, should be undertaken and (6) chromatograms should be included in the analytical report. Within this context and with a view to helping environmental managers in analytical report evaluation, this work has as objectives the discussion of the limitations of the application of SW 846 US EPA methods to marine samples, the consequences of having data based on method detection limits (MDL) and not sample quantitation limits (SQL), and present possible modifications of the principal method applied by laboratories in order to comply with environmental quality standards.

Safety report on the treatment of safety-critical systems in transport airplanes.

"NTSB/SR-06/02."

Implementation of a triple modular redundant FPGA based safety critical system for reliable software execution

This paper describes the implementation of a TMR (Triple Modular Redundant) microprocessor system on a FPGA. The system exhibits true redundancy in that three instances of the same processor system (both software and hardware) are executed in parallel. The described system uses software to control external peripherals and a voter is used to output correct results. An error indication is asserted whenever two of the three outputs match or all three outputs disagree. The software has been implemented to conform to a particular safety critical coding guideline/standard which is popular in industry. The system was verified by injecting various faults into it.