Abstract Unmanned aerial vehicle (UAV) co-operative systems are complex cyber-physical systems that integrate a high-level control algorithm with pre-existing closed implementations of lower-level vehicle kinematics. In model-driven development, simulation is one of the techniques that are usually applied, together with testing, in the analysis of system behaviours. This work proposes a method and tools to validate the design of UAV co-operative systems based on co-simulation and formal verification. The method uses the Prototype Verification System, an interactive theorem prover based on a higher-order logic language, and the Functional Mock-up Interface, a widely accepted standard for co-simulation. In this paper, results on the co-simulation and proofs of safety requirements of a representative co-ordination algorithm are shown and discussed in a scenario where quadcopters are deployed and perform space-coverage operations.

Modern vehicles contain an ecosystem of several electronic units able to exchange data using the serial communication provided by the CAN bus. This protocol can be afflicted by a plethora of attacks that can expose the driver and the passengers to risks for their safety. In this paper we propose a method to detect potential attacks in automotive networks. We start from the analysis of a log obtained from a simulation and we consider a formal verification environment to verify whether the formal model we built from the log is safe. As a proof of concept, we evaluate the proposed method in a case study related to adaptive cruise control, to preliminarily demonstrate its effectiveness.

This paper presents a methodology for the formal modeling of security attacks on cyber-physical systems, and the analysis of their effects on the system using logic theories. We consider attacks only on sensors and actuators. A simulated attack can be triggered internally by the simulation algorithm or interactively by the user, and the effect of the attack is a set of assignments to the variables. The effects of the attacks are studied by injecting attacks in the system model and simulating them. The overall system, including the attacks, the system dynamics and the control part, is co-simulated. The INTO-CPS framework has been used for co-simulation, and the methodology is applied to the Line follower robot case study of the INTO-CPS project.

This paper presents a methodology, with supporting tool, for formal modeling and analysis of software components in cyber-physical systems. Using our approach, developers can integrate a simulation of logic-based specifications of software components and Simulink models of continuous processes. The integrated simulation is useful to validate the characteristics of discrete system components early in the development process. The same logic-based specifications can also be formally verified using the Prototype Verification System (PVS), to gain additional confidence that the software design complies with specific safety requirements. Modeling patterns are defined for generating the logic-based specifications from the more familiar automata-based formalism. The ultimate aim of this work is to facilitate the introduction of formal verification technologies in the software development process of cyber-physical systems, which typically requires the integrated use of different formalisms and tools. A case study from the medical domain is used to illustrate the approach. A PVS model of a pacemaker is interfaced with a Simulink model of the human heart. The overall cyber-physical system is co-simulated to validate design requirements through exploration of relevant test scenarios. Formal verification with the PVS theorem prover is demonstrated for the pacemaker model for specific safety aspects of the pacemaker design.

Health care practices increasingly rely on complex technological infrastructure, and new approaches to the integration of information and communication technology in those practices lead to the development of such concepts as integrated clinical environments and smart intensive care units. These concepts refer to hospital settings where therapy relies heavily on inter-operating medical devices, supervised by clinicians assisted by advanced monitoring and co-ordinating software. In order to ensure safety and effectiveness of patient care, it is necessary to specify the requirements of such socio-technical systems in the most rigorous and precise way. This paper presents an approach to the formalization of system requirements for communication networks deployed in integrated clinical environment, based on the higher-order logic language of a theorem-proving environment, the Prototype Verification System.

In this paper a simulator of soft errors (SEUs) in the configuration memory of SRAM-based FPGAs is presented. The simulator, named ASSESS, adopts fault models for SEUs affecting the configuration bits controlling both logic and routing resources that have been demonstrated to be much more accurate than classical fault models adopted by academic and industrial fault simulators currently available. The simulator permits the propagation of faulty values to be traced in the circuit, thus allowing the analysis of the faulty circuit not only by observing its output, but also by studying fault activation and error propagation. ASSESS has been applied to several designs, including the miniMIPS microprocessor, chosen as a realistic test case to evaluate the capabilities of the simulator. The ASSESS simulations have been validated comparing their results with a fault injection campaign on circuits from the ITC'99 benchmark, resulting in an average error of only 0.1%.

This paper presents a novel charge equalization technique seamlessly integrated into a modular Battery Management System (BMS) for lithium-ion (Li-ion) batteries. The charge equalizer is a crucial element for an effective use of a Li-ion battery consisting of many series-connected cells. We describe a fully distributed charge equalizer based on a circular balancing bus, which outperforms other recently published approaches. Its safety requirements have formally been verified using a model checker, showing that formal methods and, in particular, the Symbolic Analysis Laboratory environment, can be effective to verify the safety requirements of a BMS.

Testing SEUs in the configuration memory of SRAM-based FPGAs is very costly due to their large configuration memory, therefore it is necessary to optimize the generation of test patterns. In particular, in order to reduce the effort required of automatic test pattern generators, it is useful to identify early the unexcitable faults, i.e., those faults that cannot be excited by any combination of input signals. In this paper, the unexcitability of SEUs affecting the configuration bits controlling the routing resources of SRAM-based FPGAs is considered. Since this part of the configuration memory contains the largest number of configuration bits, its testing is particularly onerous. Faults in the routing resources are modeled considering the actual electrical behavior of the affected interconnections, thus the resulting fault model is more accurate than the classical open/short model usually considered. This paper introduces a methodology to prove the unexcitability of these faults. The methodology has been implemented in a tool based on a formal specification language (SAL) and a model checker (SAL-SMC). Results from the application of the tool to some circuits from the ITC'99 benchmark are reported.

Lithium-ion batteries are increasingly being used in safety-critical applications, such as automotive, avionics and aerospace systems. They require the adoption of an electronic control system, called Battery Management System (BMS), to guarantee their safe and effective operation. Therefore, the reliability of the BMS is of paramount importance. In this paper, we analyze the effects of Single Event Upsets (SEUs) occurring in the control logic of an important BMS subsystem, i.e., the charge equalizer. Moreover, some SEU mitigation techniques based on logic redundancy are presented and their effectiveness is compared through fault simulation.

We propose an un-excitability prover for Single Event Upset (SEU) faults affecting the configuration memory of logic resources of SRAM-FPGA systems. In particular, we focus on the subset of untestable faults that cannot even be excited, with the aim of optimizing the generation of test patterns, in particular for in-service testing. SEUs in configuration bits of the logic resources actually used by the system are addressed. This makes our fault model much more accurate than the classical stuck-at fault model. The tool relies on the SAL specification language for the modeling of netlists, and on the SAL model checker for the proof of the un-excitability of faults. Results from the application of the tool to some circuits from the ISCAS and ITC benchmarks are reported.

We describe a simulation-based fault injection technique for calculating the probability of failures caused by SEUs in the configuration memory of SRAM-FPGA systems. Our approach relies on a model of FPGA netlists realised with the Stochastic Activity Networks (SAN) formalism. We validate our method by reproducing the results presented in other studies for some representative combinatorial circuits, and we explore the applicability of the proposed technique by analysing the actual implementation of a circuit for the generation of Cyclic Redundancy Check codes.

We describe a simulation-based fault injection technique for failure probability and fault observability assessment of SRAM-FPGA systems. Our approach relies on a model of FPGA netlists realised with the Stochastic Activity Networks formalism. Faults can be injected into the model either stochastically or exhaustively one at a time. Fault propagation is traced to the output pins, using a four-valued logic that enables faulty signals to be tagged and recognized. We considered some of the ITC'99 benchmarks as examples.

Data replication is an important aspect in a data grid for increasing fault tolerance and availability. Many grid replication tools or middleware systems deal with read-only files which imply that replicated data items are always consistent. However, there are several applications that do require updates to existing data and the respective replicas. In this article, we present a replica consistency service that allows for replica updates in a single-master scenario with lazy update synchronisation. The system allows for updates of (heterogeneous) relational databases, and it is designed to support flat files as well. It keeps remote replicas synchronised and partially ("lazily") consistent. We report on the design and implementation of a novel "relaxed" replica consistency service and show its usefulness in a typical application use case.