Search

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.

When designing Wireless Sensor Networks it is important to analyze their security risks and provide adequate solutions for protecting them from malicious attacks. Unfortunately, perfect security cannot be achieved, for performance reasons. Therefore, designers have to devise security priorities, and select security mechanisms accordingly. However, in the early stages of the design process, the concrete effects of security attacks on the system may not be clearly identified. In this paper, we propose a framework that integrates formal verification and network simulation for enabling designers to evaluate the effects of attacks, identify possible security mechanisms, and evaluate their effectiveness, since design time. Formal methods are used to build the abstract model of the application, together with a set of attacks, and to state properties of general validity. The simulator measures the impact of the attacks in terms of common network parameters, like energy consumption or computational effort. Such information can be used to select adequate security mechanisms, then the initial abstract model can be refined to adopt them, and finally prove that former system properties are still verified. The framework relies on UPPAAL for formal modeling and verification and uses the Attack Simulation Framework on top of Castalia as a network simulator. As proof of concept, a case study is shown.

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 defined in the Controller. The global effects of the attacks are studied by injecting attacks in the system model and co-simulating the overall system, including the system dynamics and the control part. Interesting properties of the behavior of the system under attack can also be formally proved by theorem proving. 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. The theorem prover of PVS has been used for deriving formal proofs of invariants of the system under attack.

This paper reports on our experience in developing training material for a hospital, in the form of an interactive simulation of a medical device routinely used in the hospital. The subject device is a commercial contrast media injector used in Computed Tomography (CT) scans. The specification of the device was reverse engineered using in combination the user manual, direct interaction with the real device, and the results of a field study we conducted that focused on how expert users routinely operate the device. The interactive simulation greatly helped to identify critical workflows that could induce accidental use errors that lead to dangerous situations such as failure to correctly detect air-in-line before starting the injection. The interactive simulation proved also useful to stimulate a constructive discussion within a multidisciplinary team of engineers and clinicians, about possible design improvements to the device that could prevent the identified critical workflows.

This paper presents a methodology to integrate computer-assisted theorem proving into a standard workflow for model-based development that uses a block-based language as a modeling and simulation tool. The theorem prover provides confidence in the results of the analysis as it guides the developers towards a correct formalization of the system under development., Electronic Communications of the EASST, Volume 79: Second Interactive Workshop on the Industrial Application of Verification and Testing, ETAPS 2020 Workshop (InterAVT 2020)

This work proposes a method for the development of cyber-physical systems starting from a high-level representation of the control algorithm, performing a formal analysis of the algorithm, and co-simulating the algorithm with the controlled system both at high level, abstracting from the target processor, and at low level, i.e., including the emulation of the target processor. The expected advantages are a smoother and more controllable development process and greater design dependability and accuracy with respect to basic model-driven development. As a case study, an automatic transmission control has been used to show the applicability of the proposed approach.

Service composition and supporting transactions across composed services are among the major challenges characterizing service-oriented computing. REpresentational State Transfer (REST) is one of the approaches used for implementing Web services that is gaining momentum thanks to its features making it suitable for cloud computing and microservices-based contexts. This paper introduces ReLock, a resilient RESTful transaction model introducing general purpose transactions on RESTful services by a layered approach and a two-phase locking mechanism not requesting any change to the RESTful services involved in a transaction.

A framework for co-simulation of human–machine interfaces in Cyber-Physical Systems (CPS) is presented. The framework builds on formal (i.e. mathematical) methods. It aims to support the work of formal methods experts in charge of modelling and analysing safety-critical aspects of user interfaces in CPS. To carry out these modelling and analysis activities, formal methods experts usually need to engage with domain experts that may not fully understand the mathematical details of formal analysis results. The framework presented in this work mitigates this communication barrier by allowing formal methods experts to create interactive prototypes driven by formal models. The prototypes closely resemble the visual appearance of the system being developed. They can be used to discuss details of the formal analysis effort without showing any mathematical detail. An existing prototyping toolkit based on formal methods is used as baseline technology. Novel functionalities are developed for automatic generation of interactive prototypes supporting the Functional Mockup Interface (FMI), a de-facto standard technology for simulation of complex systems. Using the FMI interface, the prototypes can be integrated with simulations of other system components. The architecture of the framework is presented, along with a verification of core aspects of its functionalities. A case study based on a medical system is used to demonstrate the capabilities of the framework.

This work aims at demonstrating the benefits of integrating co-simulation and formal verification in the standard design flow of a brushless power drive system for precision robotic applications. A sufficient condition on controller gain for system stability is derived from the system’s mathematical model, including a control algorithm for the reduction of cogging torque. Then, using co-simulation and design space exploration, fine tuning of the controller gain parameters has been executed, exploiting the results from the formal verification.

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, 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.

We are concerned with systems, particularly safety-critical systems, that involve interaction between users and devices, such as the user interface of medical devices. We therefore developed a MISRA C code generator for formal models expressed in the PVSio-web prototyping toolkit. PVSio-web allows developers to rapidly generate realistic interactive prototypes for verifying usability and safety requirements in human-machine interfaces. The visual appearance of the prototypes is based on a picture of a physical device, and the behaviour of the prototype is defined by an executable formal model. Our approach transforms the PVSio-web prototyping tool into a model-based engineering toolkit that, starting from a formally verified user interface design model, will produce MISRA C code that can be compiled and linked into a final product. An initial validation of our tool is presented for the data entry system of an actual medical device., In Proceedings F-IDE 2016, arXiv:1701.07925