Simulation and analysis of cyber-physical systems

Dipartimento di Ingegneria dell'informazione, Università di Pisa

This page is a summary of the research activities on simulation and analysis of digital sytems, based on formal methods, carried out at the Department of Information Engineering at the University of Pisa.

Co-simulation and formal integrated development environments

[SEFM 2019]
Maurizio Palmieri, Hugo Daniel Macedo. Automatic Generation of Functional Mock-Up Units from Formal Specifications , Software Engineering and Formal Methods (SEFM 2019), LNCS vol 12226. Springer, Cham, pp. 601--623, 2020. [ bib | DOI ]

abstract  This paper reports on the approach used to augment a transition system tool with automatic Functional Mock-up Units (FMU) generation. To verify the FMU properties, the same transition system can be translated into a formal language. Among intrinsic system properties, transition systems are associated with the following two: the disjointedness and the coverage, which assert that the controller is deterministic and defined for every possible input. This paper shows how both properties are enforced when proving the type checking conditions derived by the PVS theorem prover.
[SoftwSystModel 2020]
Maurizio Palmieri, Cinzia Bernardeschi, Paolo Masci. A framework for FMI-based co-simulation of human-machine interfaces , Software and Systems Modeling, vol. 13, no. 3, pp. 601--623, 2020. [ bib | DOI ]

abstract  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.
[Energies 2020]
Cinzia Bernardeschi, Pierpaolo Dini, Andrea Domenici, Maurizio Palmieri, Sergio Saponara. Formal Verification and Co-Simulation in the Design of a Synchronous Motor Control Algorithm , Energies, vol. 13, no. 16, pp. 4057, 2020. [ bib | DOI ]

abstract  Mechatronic systems are a class of cyber-physical systems, whose increasing complexity makes their validation and verification more and more difficult, while their requirements become more challenging. This paper introduces a development method based on model-based design, co-simulation and formal verification. The objective of this paper is to show the applicability of the method in an industrial setting. An application case study comes from the field of precision servo-motors, where formal verification has been used to find acceptable intervals of values for design parameters of the motor controller, which have been further explored using co-simulation to find optimal values. The reported results show that the method has been applied successfully to the case study, augmenting the current model-driven development processes by formal verification of stability, formal identification of acceptable parameter ranges, and automatic design-space exploration.
[JCVHT 2020]
Cinzia Bernardeschi, Andrea Domenici, Maurizio Palmieri. Formalization and co-simulation of attacks on cyber-physical systems , Journal of Computer Virology and Hacking Techniques, vol. 16, pp. 63-77, 2020. [ bib | DOI ]

abstract  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 behaviour 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.
[ICISSP 2019]
Cinzia Bernardeschi, Andrea Domenici, Maurizio Palmieri. Modeling and Simulation of Attacks on Cyber-physical Systems, In 5th International Conference on Information Systems Security and Privacy (ICISSP 2019), Prague, Czech Republic, 23-25 February 2019. [ bib |  DOI ]

Abstract. 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.
[STAF 2018 (1)]
Maurizio Palmieri, Cinzia Bernardeschi, Andrea Domenici, Adriano Fagiolini. Demo: Co-simulation of UAVs with INTO-CPS and PVSio-web , In Software Technologies: Applications and Foundations (STAF 2018), LNCS 11176, Toulouse, France, June 26, 2018. [ bib |  DOI ]

Abstract. This demo shows our ongoing work on the co-simulation of co-operative Unmanned Aerial Vehicles (UAVs). The work is based on the INTO-CPS co-simulation engine, which adopts the widely accepted Functional Mockup Interface (FMI) standard for co-simulation, and the PVSioweb prototyping tool, that extends a system simulator based on the PVS logic language with a web-based graphical interface. Simple scenarios of Quadcopters with assigned different tasks, such as rendez- vous and space coverage, are shown. We assumed a linearized dynamic model for Quadcopters formalized in OpenModelica, and a linearized set of equations for the flight control module written in C language. The co-ordination algorithm is modeled in PVS, while PVSio-web is used for graphical rendering of the co-simulation.
[STAF 2018 (2)]
Cinzia Bernardeschi, Andrea Domenici, Maurizio Palmieri. Towards Stochastic FMI Co-simulations: Implementation of an FMU for a Stochastic Activity Networks Simulator , In Software Technologies: Applications and Foundations (STAF 2018), LNCS 11176, Toulouse, France, June 26, 2018. [ bib |  DOI | preprint  | slides  ]

abstract  The advantage of co-simulation with respect to traditional single-paradigm simulation lies mainly in the modeling flexibility it affords in composing large models out of submodels, each expressed in the most appropriate formalism. One aspect of this flexibility is the modularity of the co-simulation framework, which allows developers to replace each sub-model with a new version, possibly based on a different formalism or a different simulator, without changing the rest of the co-simulation. This paper reports on the replacement of a sub-model in a co-simulation built on the INTO-CPS framework. Namely, an existing co-simulation of a water tank, available in the INTO-CPS distribution, has been modified by replacing the tank sub-model with a sub-model built as a Stochastic Activity Network simulated on Möbius, a tool used to perform statistical analyses of systems with stochastic behavior. This work discusses aspects of this redesign, including the necessary modifications to the Möbius sub-model. In this still preliminary work, the Stochastic Activity Network features related to stochastic models have not been used, but a simple deterministic model has proved useful in indicating an approach to the integration of Stochastic Activity Networks into a co-simulation framework.
[IE3TSE 2018]
Cinzia Bernardeschi, Andrea Domenici, Paolo Masci A PVS-Simulink Integrated Environment for Model-Based Analysis of Cyber-Physical Systems , IEEE Transactions on Software Engineering, vol. 44, n. 6, pp. 512-533, 2018. [ bib |  DOI |  draft ]

abstract  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.
[SEFM 2017a>]
Andrea Domenici, Adriano Fagiolini, Maurizio Palmieri. Integrated simulation and formal verification of a simple autonomous vehicle , In 1st Workshop on Formal Co-Simulation of Cyber-Physical Systems, A satellite event of SEFM2017, Trento, Italy, September 5, 2017. [ bib |  DOI | preprint  | slides  ]

abstract  This paper presents a proof-of-concept application of an approach to system development based on the integration of formal verification and co-simulation. A simple autonomous vehicle has the task of reaching an assigned straight path and then follow it, and it can be controlled by varying its turning speed. The correctness of the proposed control law has been formalized and verified by interactive theorem proving with the Prototype Verification System. Concurrently, the system has been co-simulated using the Prototype Verification System and the MathWorks Simulink tool: The vehicle kinematics have been simulated in Simulink, whereas the controller has been modeled in the logic language of the Prototype Verification System and simulated with the interpreter for the same language available in the theorem proving environment. With this approach, co-simulation and formal verification corroborate each other, thus strengthening developers' confidence in their analysis.
[SEFM 2017 (1)]
Mauizio Palmieri, Cinzia Bernardeschi, Paolo Masci. Co-simulation of semi-autonomous systems: the Line Follower Robot case study , In 1st Workshop on Formal Co-Simulation of Cyber-Physical Systems, A satellite event of SEFM2017, Trento, Italy, September 5, 2017. [ bib |  DOI ]

abstract  Semi-autonomous systems are capable of sensing their environment and perform their tasks autonomously, but they may also be supervised by humans. The shared manual/automatic control makes the dynamics of such systems more complex, and undesirable and hardly predictable behaviours can arise from human-machine interaction. When these systems are used in critical applications, such as autonomous driving or robotic surgery, the identification of conditions that may lead the system to violate safety requirements is of main concern, since people actually entrust their life on them. In this paper, we extend an FMI-based co-simulation framework for cyber-physical systems with the possibility of modelling semi-autonomous robots. Co-simulation can be used to gain more insights on the system under analysis at early stages of system development, and to highlight the impact of human interaction on safety. This approach is applied to the Line Follower Robot case study, available in the INTO-CPS project.
[F-IDE 2016]
Gioacchino Mauro, Harold Thimbleby, Andrea Domenici, Cinzia Bernardeschi. Extending a user interface prototyping tool with automatic MISRA C code generation , In 3rd Workshop on Formal Integrated Development Environment (F-IDE 2016), Limassol, Cyprus, November 8, 2016. [ bib |  DOI |  http  |   slides ]

abstract  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.
[CARDIOTECHNIX 2014]
Cinzia Bernardeschi, Andrea Domenici, and Paolo Masci. Integrated Simulation of Implantable Cardiac Pacemaker Software and Heart Models. 2d International Congress on Cardiovascular Technology (CARDIOTECHNIX 2014), Rome, Italy, 2014. [ bib | slides | http | CARDIOTECHNIX 2014 web site ]

abstract  This paper presents an approach for integrated simulation of pacemaker models and heart models, each developed with the appropriate formalism. Heart models are developed in MathWorks, a powerful tool for the simulation of complex systems, whereas pacemakers are developed in PVS, a theorem-proving environment enabling both simulation and formal verification of safety requirements. The two tools communicate over a Web-based interface, which makes it possible to integrate the simulation of the MathWorks model of the heart and the PVS model of the pacemaker. In this paper, we illustrate the architecture developed for integrated simulation of the pacemaker-heart system and present an example application for realistic models.

Higher-order logic

The higher-order logic language of the Prototype Verification System has been used to formalize, verify, and simulate systems with dependability constraints.
[ARSBM 2019]
Cinzia Bernardeschi, Andrea Domenici, Paolo Masci. Logic-Based Formalization of System Requirements for Integrated Clinical Environments, In P. Liò and P. Zuliani (eds): Automated Reasoning for Systems Biology and Medicine, Computational Biology, vol. 30, 2019. [ bib |  DOI ]

Abstract. The concepts of integrated clinical environments and smart intensive care units refer to complex technological infrastructures where health care relies on interoperating medical devices monitored and coordinated by software applications under human supervision. These complex socio-technical systems have stringent safety requirements that can be met with rigorous and precise development methods. This chapter presents an approach to the formalization of system requirements for integrated clinical environments, using the Prototype Verification System, a theorem-proving environment based on a higher-order logic language. The approach is illustrated by modeling safety-related requirements affecting various aspects of an integrated clinical environment, and in particular the communication network. A simple but realistic wireless communication protocol will be used as an example of computer-assisted verification.
[ICTS4eHEALTH 2016]
Cinzia Bernardeschi, Andrea Domenici, Paolo Masci. Modeling Communication Network Requirements for an Integrated Clinical Environment in the Prototype Verification System , In 4th ICTS4eHealth Workshop, 2016 IEEE Symposium on Computers and Communication (ISCC), Messina, Italy, June 27 - 30, 2016. [ bib |  DOI |  http ]

abstract  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.
[IPL 2016]
Cinzia Bernardeschi, Andrea Domenici. Verifying safety properties of a nonlinear control by interactive theorem proving with the Prototype Verification System , Information Processing Letters vol. 116, no. 6, pp. 409--415, 2015. [ bib |  DOI |  http |  preprint ]

abstract  Interactive, or computer-assisted, theorem proving is the verification of statements in a formal system, where the proof is developed by a logician who chooses the appropriate inference steps, in turn executed by an automatic theorem prover. In this paper, interactive theorem proving is used to verify safety properties of a nonlinear (hybrid) control system.
[MOBIHEALTH 2015]
Cinzia Bernardeschi, Andrea Domenici, Paolo Masci. Towards a Formalization of System Requirements for an Integrated Clinical Environment EAI Endorsed Transactions on Self-Adaptive Systems vol. 16, no. 6, Dec. 2015. [ bib |  DOI |   http ]

abstract  Interoperability of medical devices, and their interface to clinicians and patients, are critical issues for the safety and effectiveness of patient care. Ongoing efforts strive at establishing standards for integrated clinical environments, which may connect and co-ordinate several medical devices and interface them to patients, clinicians, and hospital information systems. In this paper, an approach to the formalization of system requirements for an integrated clinical environment is presented. The formalization relies on the higher-order logic language of the Prototype Verification System.
[IJAS 2011]
Cinzia Bernardeschi, Luca Cassano, Andrea Domenici, and Paolo Masci. Simulation and Test-Case Generation for PVS Specifications of Control Logics. International Journal on Advances in Software, 4(3 & 4):327-341, 2011. [ bib | http]

abstract  We describe a framework for the simulation of control logics specified in the higher-order logic of the Prototype Verification System. The framework offers a library of predefined modules, a method for the composition of more complex modules, and an event-driven simulation engine. A developer defines a system architecture by composing its model out of library modules, possibly introducing new module definitions, and simulates the behaviour of the system model by providing its input waveforms, which are given as functions from time to logic levels. The generation of simulation scenarios (test cases) can be automated by using parametric waveforms that can be instantiated through universal and existential quantifiers. We demonstrate the simulation capabilities of our framework on two simple case studies from a nuclear power plant application. The main feature of this approach is that our formal specifications are executable. Moreover, once the simulation experiments give developers sufficient confidence in the correctness of the specification, the logic models can serve as the basis for its formal verification.
[COMPUTATION TOOLS 2010]
Cinzia Bernardeschi, Luca Cassano, Andrea Domenici, and Paolo Masci. Debugging PVS specifications of control logics via event-driven simulation. In Computation Tools 2010, Lisbon, Portugal, November 21-26 2010. IARIA. [ bib ]

abstract  In this paper we present a framework aimed at simulating control logics specified in the higher-order logic of the Prototype Verification System (PVS). The framework offers a library of predefined modules, a method for the composition of more complex modules, and an event-driven simulation engine. A developer simulates the specified system by providing its input waveforms as functions from time to logic levels. Once the simulation experiments give sufficient confidence in the correctness of the specification, the model can serve as a basis for the formal verification of desired properties of interest. A simple case study from a nuclear power plant application is shown.

Stochastic Activity Networks

The ASSESS tool is a simulator based on a Stochastic Activity Networks model of digital circuits, which has been used for the simulation and analysis of the effects of Single Event Upsets in SRAM-based FPGAs. The simulator is built upon the Möbius tool and works in conjunction with an EDIF parser and external tools, such as E2STAR and GABES.
[PhD THESIS]
Luca Cassano. Analysis and Test of the Effects of Single Event Upsets Affecting the Configuration Memory of SRAM-based FPGAs. Ph.D. thesis, Dottorato di Ricerca in Ingegneria dell'informazione, Scuola di Dottorato in Ingegneria "Leonardo da Vinci", Università di Pisa. 2013. (Winner of the European semi-finals of the TTTC's E. J. McCluskey Doctoral Thesis Award, 2014). [ http |
[IE3TCAD 2014]
Cinzia Bernardeschi, Luca Cassano, Andrea Domenici, Luca Sterpone. ASSESS: A Simulator of Soft Errors in the Configuration Memory of SRAM-Based FPGAs. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 33, no. 9, pp. 1342-1355, Sept. 2014. [ bib |  DOI |  draft ]

abstract  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%.
[IECON 2013]
Federico Baronti, Cinzia Bernardeschi, Luca Cassano, Andrea Domenici, Roberto Roncella, and Roberto Saletti. Mitigation of Single Event Upsets in the Control Logic of a Charge Equalizer for Li-ion Batteries. In 39th Annual Conference of the IEEE Industrial Electronics Society (IECON 2013), Vienna, Austria, 2013. [ bib |  DOI |  slides ]

abstract  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.
[JSA 2013]
Cinzia Bernardeschi, Luca Cassano, Mario G. C. A. Cimino, and Andrea Domenici. GABES: a Genetic Algorithm Based Environment for SEU Testing in SRAM-FPGAs, Journal of Systems Architecture, vol. 59, pages 1383-1254, 2013. [ bib |  DOI |  draft ]

abstract  Testing of FPGAs is gaining more and more interest because of the application of FPGA devices in many safety-critical systems. We propose GABES, a tool for the generation of test patterns for application-dependent testing of SEUs in SRAM-FPGAs, based on a genetic algorithm. Test patterns are generated and selected by the algorithm according to their fault coverage: Faults are injected in a simulated model of the circuit, the model is executed for each test pattern and the respective fault coverage is computed. We focus on SEUs in configuration bits affecting logic resources of the FPGA. This makes our fault model much more accurate than the classical stuck-at model. Results from the application of the tool to some circuits from the ITC'99 benchmarks are reported. These results suggest that this approach may be effective in the inspection of safety-critical components of control systems implemented on FPGAs.
[DFT 2012]
Cinzia Bernardeschi, Luca Cassano, Andrea Domenici, and Luca Sterpone. Accurate Simulation of SEUs in the Configuration Memory of SRAM-based FPGAs. In Proceedings of the 25th IEEE International Symposium on Defect and Fault Tolerance in VLSI and Nanotechnology Systems (DFT2012), pages 115-120, IEEE, 2014. [ bib | DOI ]

abstract  SRAM-based FPGAs are more and more relevant in a growing number of applications, ranging from the automotive to the aerospace ones. Designers of safety-critical applications demand accurate methodologies to evaluate the Single Event Upsets (SEUs) sensitivity of their designs. In this paper, we present an accurate simulation method for the evaluation of the effects of SEUs in the configuration memory of SRAM-based FPGAs. The approach is able to simulate SEUs affecting the configuration memory of both logic and routing resources since it is able to accurately model the electrical behavior of SEUs in the configuration memory. Detailed experimental results on a large set of benchmark circuits are provided and the comparison with fault injection experiments is shown in order to validate the accuracy of the proposed method. The results clearly demonstrate the benefits of our approach since simulation results predict almost completely the results obtained through fault injection.
[WRC 2012]
Cinzia Bernardeschi, Luca Cassano, Mario Giovanni Cosimo Antonio Cimino, and Andrea Domenici. Application of a Genetic Algorithm for Testing SEUs in SRAM-FPGA Systems. In 6th HiPEAC Workshop on Reconfigurable Computing (WRC 2012), 2012. [ bib| http  ]

abstract  Testing of FPGAs is gaining more and more interest because of the employment of FPGA devices in many safety-critical application fields. We propose a prototype of a tool for the generation of test patterns for application-dependent testing of SEUs in SRAM-FPGAs based on a genetic algorithm. We focus on SEUs affecting logic resources of the FPGA. SEUs in any configuration bit are addressed, making our fault model much more accurate than the classical stuck-at fault model. Results from the application of the tool to some circuits from the ISCAS and ITC benchmarks are reported.
[COMPUTATION TOOLS 2011]
Cinzia Bernardeschi, Luca Cassano, Andrea Domenici, and Paolo Masci. A Tool for Signal Probability Analysis of FPGA-Based Systems. In Proceedings of the 2nd International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking (COMPUTATION TOOLS 2011), pages 13-18, 2011. [ bib ]

abstract  We describe a model of Field Programmable Gate Array based systems realised with the Stochastic Activity Networks formalism. The model can be used (i) to debug the circuit design synthesised from the high level description of the system, and (ii) to calculate the signal probabilities and transition densities of the circuit design, which are parameters that can be used for reliability analysis, power consumption estimation and pseudo random testing. We validate the developed model by reproducing the results presented in other studies for some representative combinatorial circuits, and we explore the applicability of the proposed model in the analysis of real-world devices by analysing the actual implementation of a circuit for the generation of Cyclic Redundancy Check codes.
[FPL 2011]
Cinzia Bernardeschi, Luca Cassano, and Andrea Domenici. Failure Probability and Fault Observability of SRAM-FPGA Systems. In International Conference on Field Programmable Logic and Applications (FPL2011), pages 385-388. IEEE, sep 2011. [ bib | DOI ]

abstract  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.
[DDECS 2011]
Cinzia Bernardeschi, Luca Cassano, and Andrea Domenici. Failure probability of SRAM-FPGA systems with Stochastic Activity Networks. In IEEE 14th International Symposium on Design and Diagnostics of Electronic Circuits Systems (DDECS 2011), pages 293-296. IEEE, apr 2011. [ bib | DOI ]

abstract  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.
[VALID 2011]
Cinzia Bernardeschi, Luca Cassano, Andrea Domenici, Giancarlo Gennaro, and Mario Pasquariello. Simulated Injection of Radiation-Induced Logic Faults in FPGAs. In Proceedings of the 3rd International Conference on Advances in System Testing and Validation Lifecycle (VALID 2011), pages 84-89. IARIA, 2011. [ bib | http]

abstract  SRAM-FPGA systems are simulated with a model based on the Stochastic Activity Networks (SAN) formalism. Faults are injected into the model and their propagation is traced to the output pins using a four-valued logic that enables faulty logical signals to be tagged and recognized without recurring to a comparison with the expected output values. Input vectors are generated probabilistically based on assumed signal probabilities. By this procedure it is possible to obtain a statistical assessment of the observability of different faults for the generated inputs. The analysis of a 2-out-of-2 voter is shown as a case study.

Model checking

Model checking techniques have been used, with the SAL framework, to prove the unexcitability or untestability of faults induced by SEU in SRAM-based FPGAs.
[IVLSIJ 2016]
Cinzia Bernardeschi, Luca Cassano, Andrea Domenici, Luca Sterpone. UA2TPG: An Untestability Analyzer and Test Pattern Generator for SEUs in the Configuration Memory of SRAM-based FPGAs , Integration, the VLSI Journal, vol. 55, pp. 85--97, 2016. [ bib |  DOI |   http ]

abstract  This paper presents UA2TPG, a static analysis tool for the untestability proof and automatic test pattern generation for SEUs in the configuration memory of SRAM-based FPGA systems. The tool is based on the model-checking verification technique. An accurate fault model for both logic components and routing structures is adopted. Experimental results show that many circuits have a significant number of untestable faults, and their detection enables more efficient test pattern generation and on-line testing. The tool is mainly intended to support on-line testing of critical components in FPGA fault-tolerant systems.
[IE3TII 2014]
Federico Baronti, Cinzia Bernardeschi, Luca Cassano, Andrea Domenici, Roberto Roncella, and Roberto Saletti. Design and Safety Verification of a Distributed Charge Equalizer for Modular Li-ion Batteries. IEEE Transactions on Industrial Informatics, vol. 10, no. 2, pp. 1003-1011, May 2014. [ bib |  DOI ]

abstract  This paper presents a novel charge equalization technique seamlessly integrated into a modular Battery Man- agement 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.
[GLSVLSI 2013]
Cinzia Bernardeschi, Luca Cassano, and Andrea Domenici. Unexcitability Analysis of SEUs Affecting the Routing Structure of SRAM-based FPGAs. In Proceedings of the 23rd ACM International Conference on Great Lakes Symposium on VLSI (GLSVLSI'13), pages 7-12, ACM, 2013. [ bib | DOI |  preprint ]

abstract  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.
[IOLTS 2012]
Cinzia Bernardeschi, Luca Cassano, and Andrea Domenici. SEU-X: A SEu un-eXcitability prover for SRAM-FPGAs. In 2012 IEEE 18th International On-Line Testing Symposium (IOLTS), pages 25-30, jun 2012. [ bib | DOI ]

abstract  We propose an untestability 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 can not 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 untestability of faults. Results from the application of the tool to some circuits from the ISCAS and ITC benchmarks are reported.

On-line testing of radiation-induced faults

[IE3TETC 2016]
Dario Cozzi, Sebastian Korf, Luca Cassano, Jens Hagemeyer, Andrea Domenici, Cinzia Bernardeschi, Mario Porrmann, Luca Sterpone OLT(RE)2: an On-Line on-demand Testing approach for permanent Radiation Effects in REconfigurable systems , IEEE Transactions on Emerging Topics in Computing, vol. PP, 2016. [ bib |  DOI |  http ]

abstract  Reconfigurable systems gained great interest in a wide range of application fields, including aerospace, where electronic devices are exposed to a very harsh working environment. Commercial SRAM-based FPGA devices represent an extremely interesting hardware platform for this kind of systems since they combine low cost with the possibility to utilize state-of-the-art processing power as well as the flexibility of reconfigurable hardware. In this paper we present OLT(RE)2: an on-line on-demand approach to test permanent faults induced by radiation in reconfigurable systems used in space missions. The proposed approach relies on a test circuit and on custom place-and-route algorithms. OLT(RE)2 exploits partial dynamic reconfigurability offered by today’s SRAM-based FPGAs to place the test circuits at run-time. The goal of OLT(RE)2 is to test unprogrammed areas of the FPGA before using them, thus preventing functional modules of the reconfigurable system to be placed on areas with faulty resources. Experimental results have shown that (i) it is possible to generate, place and route the test circuits needed to detect on average more than 99 % of the physical wires and on average about 97 % of the programmable interconnection points of an arbitrary large region of the FPGA in a reasonable time and that (ii) it is possible to download and run the whole test suite on the target device without interfering with the normal functioning of the system.
A short overview of the above activities, applied to FPGAs, is found in this paper:
[AHS 2013]
Cinzia Bernardeschi, Luca Cassano, and Andrea Domenici. Formal approaches to SEU testing in FPGAs. In 2013 NASA/ESA Conference on Adaptive Hardware and Systems (AHS-2013), Torino, Italy, 2013. [ bib | DOI ]

abstract  Various formal approaches can be used to study FPGA-based systems in relationships to faults, in particular to SEUs. Formal approaches, such as high-order logic, model checking, or Stochastic Activity Networks, have been used for fault simulation, analysis of (un)testability, and test pattern generation. This paper reports on experiences and future developments related to soft errors in the configuration memory of SRAM-based devices, which are of particular interest for reconfigurable systems.

A survey on SRAM-based FPGA development methods:

[JCST 2015]
Cinzia Bernardeschi, Luca Cassano, Andrea Domenici. SRAM-based FPGA Systems for Safety-Critical Applications: A Survey on Design Standards and Proposed Methodologies. Journal of computer science and technology vol. 30, no. 2, pp. 373-390, March 2014. [ bib |  DOI |  draft ]

abstract  As the ASIC design cost becomes affordable only for very large scale productions, the FPGA technology is currently becoming the leading technology for those applications that require a small scale production. FPGAs can be considered as a technology crossing between hardware and software. Only a small number of standards for the design of safety-critical systems give guidelines and recommendations that take the peculiarities of the FPGA technology into consideration. The main contribution of this paper is an overview of the existing design standards that regulate the design and verification of FPGA-based systems in safety-critical application fields. Moreover, the paper proposes a survey of significant published research proposals and existing industrial guidelines about the topic, and collects and reports about some lessons learned from industrial and research projects involving the use of FPGA devices.

Teaching material