Abstract In automotive engineering, vehicle platooning is a proposed method for improving convoy movements by coordinating them to increase the safety and efficiency of transportation systems. The complexity and stochastic nature of platooning systems provide difficulties for traditional model-checking techniques. However, Statistical Model Checking (SMC) offers a solution by using statistical inference to probabilistically evaluate system features. This paper shows that Uppaal SMC offers a robust framework for assessing platooning systems across various operational scenarios, combining statistical analysis and formal verification methodologies. The behaviour of the platoon is modelled stochastically to cover a wide range of driving scenarios and road surfaces. Using SMC, it has been possible to gauge the safety and functionality of the platoon by estimating the probability of several properties.

Cyber-Physical Systems (CPSs) are a large class of systems characterized by networked co-operating sub-systems, that perceive surrounding environment via sensors and actuators. Cybersecurity is relevant in CPSs because, on the one hand, these systems expose a wide cyber-attack surface while, on the other hand, a security infringement may translate into a safety infringement. This work presents a methodology for developing an intrusion detection system for CPSs based on neural networks. The methodology exploits a digital twin of the CPS to generate traces of executions. An instrumented approach is used to extend the digital twin model by introducing functions that simulate the effects of various class of attacks on the system. The instrumented digital twin is used to gather data of the system’s behaviour with and without attacks. Collected data are used for training the neural network. To illustrate the methodology we consider a case-study featuring an Adaptive Cruise Control System in autonomously driving vehicles. A Multi-Layer Perceptron neural network is trained to detect attacks to sensors. Results show an high accuracy in detecting attacks.

Machine Learning approaches have been successfully used for the creation of high-performance control components of cyber–physical systems, where the control dynamics result from the combination of many subsystems. However, these approaches may lack the trustworthiness required to guarantee their reliable application in a safety-critical context. In this paper, we propose a combination of interval arithmetic and theorem-proving verification techniques to analyze safety properties in closed-loop systems that embed neural network components. We show the application of the proposed approach to a model-predictive controller for autonomous driving comparing the neural network verification performance with other existing tools. The results show that open-loop neural network verification through interval arithmetic can outperform existing approaches proving properties with a smaller time overhead. Furthermore, we demonstrate the capability of combining the two approaches to construct a formal model of the network in higher-order logic of the controlled system in a closed-loop.

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.

This paper presents an approach to create high-fidelity models suited for digital twin application of distributed multi-agent cyber–physical systems (CPSs) exploiting the combination of simulation units through co-simulation. This approach allows for managing the complexity of cyber–physical systems by decomposing them into multiple intertwined components tailored to specific domains. The native modular design simplifies the building, testing, prototyping, and extending CPSs compared to monolithic simulator approaches. A system of platoon of vehicles is used as a case study to show the advantages achieved with the proposed approach. Multiple components model the physical dynamics, the communication network and protocol, as well as different control software and external environmental situations. The model of the platooning system is used to compare the performance of Vehicle-to-Vehicle communication against a centralized multi-access edge computing paradigm. Moreover, exploiting the detailed model of vehicle dynamics, different road surface conditions are considered to evaluate the performance of the platooning system. Finally, taking advantage of the co-simulation approach, a solution to drive a platoon in critical road conditions has been proposed. The paper shows how co-simulation and design space exploration can be used for parameter calibration and the design of countermeasures to unsafe situations.

Cyber-physical systems (CPSs) are systems in which digital and physical entities cooperate. When CPSs execute safety-critical tasks, monitoring of their behavior is of main concern. The CPS should be moved to a safe state in case of malfunctions. This demo shows how an on-line supervisor can be developed for a Line Follower Robot, starting from a digital model of the robot.

This paper presents an approach to create high fidelity Digital-Twin models for distributed multi-agent cyber-physical systems based on the combination of simulating components, generated from different modeling languages, each tailored for the specific domain of the subsystem. The approach specifically addresses the wireless communication domain, exploiting a Python module as a simulating component to evaluate the impact of network delay among the distributed elements of the system under analysis. A case study with a platoon of four vehicles following a leading car, all modeled in Simulink, is used to show the applicability of the approach, allowing the comparison between a Vehicle-to-Vehicle communication against a centralized multi-access edge computing paradigm.

Wireless Sensor Networks (WSNs) are particularly prone to security attacks. However, it is well-known that perfect security is not achievable. Therefore, it is important to identify threats and evaluate their severity, for prioritizing the security countermeasures to be adopted, even since design time. In this work, we propose an approach that binds formal methods and network simulation for assessing the effects of security attacks on WSN applications from design time, starting from the abstract model of the system. Formal methods make it possible to build abstract system models and state properties of general validity, but cannot provide any concrete measurement regarding the network and the application. On the other hand, network simulators can provide precise and realistic information about simulated scenarios only. As a proof of concept, we design and prototype an application-level communication protocol, which is simulated both on attack free and attack scenarios. First, the protocol's formal properties are specified and proved via UPPAAL. Then, the resulting UPPAAL model is used to automatically generate a network model for the WSN simulator Castalia. Finally, the network model is simulated against attack free and attack scenarios, for gathering realistic information about the protocol behavior and performance.

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.

Android malware is increasing from the point of view of the complexity and the harmful actions. As a matter fact, malware writers are developing sophisticated techniques to infect mobile devices very closed to their counterpart for personal computers. One of these threats is represented by the possibility to control the infected devices from the attacker i.e., the so-called botnet. In this paper a method able to identify botnet in Android environment through model checking is proposed. Starting from the malicious payload definition, the proposed method is able to detect and to localize the code related to the malicious botnet. We experiment real-world botnet based Android malware, obtaining encouraging results.

In the last decades, FPGAs have been increasingly used in many different mission critical applications, such as the avionics and aerospace ones. Thus, research interest in studying faults in FPGAs has seen a sharp increase, especially for those applications that require high dependability and must operate in harsh environments. The increase of resources available in FPGA devices has caused a huge growth in routing complexity. Nowadays, more than 80% of transistors in modern FPGAs are related to the routing infrastructure. The analysis of faults related to routing structure of FPGA devices is a hard task due to the lack of tools working at low-level, limited information availability about interconnection structure from vendors and, above all, no automated testing workflow for such kind of resources. In this paper, we introduce PyXEL, an integrated environment realized to automatize the analysis of fault effects in FPGAs routing structure. PyXEL is a Python-based framework that allows to easily manipulate FPGAs bitstreams in order to inject specific faults and to analyze their behavior. Moreover, PyXEL provides an easy way to build and run experimental workflow interacting directly with Xilinx Vivado and ISE allowing to select routing resources to test and logically analyze results. We demonstrated the feasibility and the advantages of our approach exploiting PyXEL to gain insight into the electrical effects of faults in the routing interconnections of the Xilinx Artix-7.

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.

This paper presents a method to check data secure flow in security annotated AUTOSAR models. The approach is based on information flow analysis and abstract interpretation. The analysis computes the lowest security level of data sent on a communication, according to the annotations in the model and the code of runnables. An abstract interpreter executes runnables on abstract domains that abstract from real values and consider only data dependency levels. Data secure flow is verified if data sent on a communication always satisfy the security annotation in the model. The work has been developed in the EU project Safure, where modeling extensions to AUTOSAR have been proposed to improve security in automotive communications.

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.

Bytecode verification is a key point in the security chain of the Java platform. This feature is only optional in many embedded devices since the memory requirements of the verification process are too high. In this article we propose an approach that significantly reduces the use of memory by a serial/parallel decomposition of the verification into multiple specialized passes. The algorithm reduces the type encoding space by operating on different abstractions of the domain of types. The results of our evaluation show that this bytecode verification can be performed directly on small memory systems. The method is formalized in the framework of abstract interpretation.

Java applets run on a Virtual Machine that checks code integrity and correctness before execution using a module called the Bytecode Verifier. Java Card technology allows Java applets to run on smart cards. The large memory requirements of the verification process do not allow the implementation of an embedded Bytecode Verifier in the Java Card Virtual Machine. To address this problem, we propose a verification algorithm that optimizes the use of system memory by imposing an ordering on the verification of the instructions. This algorithm is based on control flow dependencies and immediate postdominators in control flow graphs.

This paper presents an approach to analyze stack-based assembly code with respect to leakages of private information. We consider systems implementing a multilevel security policy, where the security levels form a lattice. The approach is based on abstract interpretation of the operational semantics. We consider a representative subset of instructions of conventional stack-based assembly languages. We define a collecting small-step semantics of the language, enhanced to convey the level of the information flow during execution: this is accomplished by annotating each value with the level of the information on which it depends. Then we define an abstract semantics of the language that abstracts from actual data and maintains only the annotations on the security level. We give sufficient conditions the abstract semantics must satisfy to ensure secure information flow. The use of abstract interpretation allows, on one side, being semantics based, to accept as secure a wide class of programs, and on the other side, being rule based, to be automated fully. In fact we show how it may be combined with a model checking technique, where the conditions for security are described by temporal logic formulae that can be automatically checked on the abstract representation of the program.

Abstract A method is presented for checking secure information flow in Java bytecode, assuming a multilevel security policy that assigns security levels to the objects. The method exploits the type‐level abstract interpretation of standard bytecode verification to detect illegal information flows. We define an algorithm transforming the original code into another code in such a way that a typing error detected by the Verifier on the transformed code corresponds to a possible illicit information flow in the original code. We present a prototype tool that implements the method and we show an example of application. Copyright © 2004 John Wiley & Sons, Ltd.

When an applet is sent over the internet, Java Virtual Machine code is transmitted and remotely executed. Because untrusted code can be executed on the local computer running the web browser security problems may arise. We present a method to check illicit flows in Java bytecode, that exploits the type-level abstract interpretation of bytecode verification. We present an algorithm transforming a bytecode into another one that, when abstractly executed by the standard bytecode verifier, reveals illicit information flows. We show an example of application of the method.

The Java Virtual Machine embodies a verifier which performs a set of checks on bytecode programs before their execution. The verifier performs a data-flow analysis applied to a type-level abstract interpretation of the code. The current implementations of the bytecode verifier present a significant problem: there are legal Java programs which are correctly compiled into a bytecode that is rejected by the verifier. Also the more powerful verification techniques proposed in several papers suffer from the same problem. In this paper we propose to enhance the bytecode verifier to accept such programs, maintaining the efficiency of current implementations. The enhanced version is based on a domain of types which is more expressive than the one used in standard verification.

Abstract This paper proposes a modelling approach suitable for formalizing fault tolerant systems, taking into account different fault scenarios. Verification of the properties of such systems is then performed using model checking. A general framework for the formal specification and verification of fault tolerant systems is defined starting from these principles, and experience with its application to two case studies is then presented. Copyright © 2002 John Wiley & Sons, Ltd.

This paper presents an approach for the specification and the verification of the correctness of fault tolerant system designs achieved by the application of fault tolerant techniques. The approach is based on process algebras, equivalence theory and temporal logic. The behaviour of the system in the absence of faults is formally specified and faults are assumed as random events which interfere with the system by modifying its behaviour. The fault tolerant technique is formalized by a context that specifies how replicas of the system cooperate to deal with faults. The system design is proved to behave correctly under a given fault hypothesis by proving the observational equivalence between the system design specification and the fault-free system specification. Additionally, model checking of a temporal logic formula which gives an abstract notion of correct behaviour can be applied to verify the correctness of the design. The opportunities given by the expression of the fault hypothesis using temporal logic are discussed. The actual usability of the approach in real case studies is supported by the availability of automatic tools for equivalence checking and for proving the temporal logic properties by model checking.

The paper presents an approach for the specification and verification of the correctness of dependable system designs achieved by the application of fault tolerant techniques based on equivalence relations and model checking techniques. The behaviour of the system in absence of faults is formally specified and faults are assumed as random events which interfere with the system by modifying its behaviour. The fault tolerant technique is formalized by a context, which specifies how replicas of the system cooperate to deal with faults. The system design is proved to satisfy the correctness property under a given fault hypothesis, by proving the observational equivalence between the system design specification and the fault free system specification. Additionally, model checking of a temporal logic formula which gives an abstract notion of correct behaviour can be applied to verify the correctness of the design.