Recent and Selected Publications

Journals

• Cinzia Bernardeschi, Gianluca Dini, Murizio Palmieri, Francesco Racciatti. A framework for formal analysis and simulative evaluation of security attacks in wireless sensor networks. J. Comput. Virol. Hacking Tech., 2021. https://doi.org/10.1007/s11416-021-00392-02021
  
  
• Luca Frosini, Pasquale Pagano, Leonardo Candela, Manuele Simi, Cinzia Bernardeschi. ReLock: a resilient two-phase locking RESTful transaction model. Serv. Oriented Comput. Appl. 15(1): 75-92, 2021
  
  
• 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.
  
  
• Cinzia Bernardeschi, Andrea Domenici, Maurizio Palmieri. Formalization and co-simulation of attacks on cyber-physical systems. J. Comput. Virol. Hacking Tech. 16(1): 63-77, 2020.
  
  
• Maurizio Palmieri, Cinzia Bernardeschi, Paolo Masci. A framework for FMI-based co-simulation of human-machine interfaces. Softw. Syst. Model. 19(3): 601-623, 2020.
  
  
• Cinzia Bernardeschi, Andrea Domenici, Sergio Saponara. Formal Verification in the Loop to Enhance Verification of Safety-Critical Cyber-physical Systems. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 77, 2019
  
  
• Cinzia Bernardeschi, Paolo Masci, Davide Caramella, Ruggero Dell'Osso. The benefits of using interactive device simulations as training material for clinicians: an experience report with a contrast media injector used in CT. SIGBED Rev. 16(2): 41-45, 2019
  
  
• Dario Cozzi, Sebastian Korf, Luca Cassano, Jens Hagemeyer, Andrea Domenici, Cinzia Bernardeschi, Luca Sterpone, Mario Porrmann. OLT(RE)2: An On-Line On-Demand Testing Approach for Permanent Radiation Effects in Reconfigurable Systems. IEEE Trans. Emerging Topics Comput. 6(4): 511-523, 2018
  
  
• Cinzia Bernardeschi, Marco Di Natale, Gianluca Dini, Maurizio Palmieri.Verifying data secure flow in AUTOSAR models. J. Comput. Virol. Hacking Tech. 14(4): 269-289, 2018
  
  
• Cinzia Bernardeschi, Andrea Domenici, Paolo Masci. A PVS-Simulink Integrated Environment for Model-Based Analysis of Cyber-Physical Systems. IEEE Trans. Software Eng. 44(6): 512-533, 2018
  
  
• Cinzia Bernardeschi, Andrea Domenici. Verifying safety properties of a nonlinear control by interactive theorem proving with the Prototype Verification System. Inf. Process. Lett. 116(6): 409-415, 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, 55: 85-97, 2016
  
  
• Marco Avvenuti, Cinzia Bernardeschi, Luca Cassano, Alessio Vecchio. Adapting the duty cycle to traffic load in a preamble sampling MAC for WSNs, Ad Hoc & Sensor Wireless Networks 31(1-4): 101-129, 2016
  
  
• 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, 30(2): 373-390, DOI 10.1007/s11390-015-1530-5, 2015
  
  
• Cinzia Bernardeschi, Luca Cassano, Andrea Domenici, Luca Sterpone. ASSESS: A Simulator of Soft Errors in the Configuration Memory of SRAM-Based FPGAs. IEEE Trans. on CAD of Integrated Circuits and Systems 33(9): 1342-1355, 2014
  
  
• Federico Baronti, Cinzia Bernardeschi, Luca Cassano, Andrea Domenici, Roberto Roncella, Roberto Saletti. Design and Safety Verification of a Distributed Charge Equalizer for Modular Li-Ion Batteries. IEEE Trans. Industrial Informatics 10(2): 1003-1011, 2014
  
  
• Cinzia Bernardeschi, Luca Cassano, Mario G. C. A. Cimino, Andrea Domenici: GABES: A genetic algorithm based environment for SEU testing in SRAM-FPGAs. Journal of Systems Architecture - Embedded Systems Design 59(10-D): 1243-1254, 2013
  
  
• Avvenuti M, Bernardeschi C, De Francesco N, Masci P. JCSI: A Tool for Checking Secure Information Flow in Java Card Applications . The Journal of Systems and Software, vol. 85, p. 2479-2493, ISSN: 0164-1212, 2012
  
  
• Cinzia Bernardeschi, Luca Cassano, Andrea Domenici, Paolo Masci. Simulation and Test-Case Generation for PVS Specifications of Control Logics. International Journal on Advances in Software, vol. 4, p. 327-341, ISSN: 1942-2628, 2011
  
  
• C. Bernardeschi, N. De Francesco, G. Lettieri, L. Martini, P. Masci. Decomposing bytecode verification by abstract interpretation. ACM Transactions on Programming Languages and Systems, vol. 31/1; pp. 1-63, ISSN: 0164-0925, 2008
  
  
• C. Bernardeschi, G. Lettieri, L. Martini, P. Masci, Using Control Dependencies for Space-Aware Bytecode Verification, COMPUTER JOURNAL, vol. 49, num. 2, pp 234-248, 2006
  
  
• C. Bernardeschi, G. Lettieri, L. Martini, P. Masci, Using postdomination to reduce space requirements of data flow analysis, Information Processing letters,vol. 98,num. 1, pp 11-18, 2006
  
  
• C. Bernardeschi, N. De Francesco, G. Lettieri, Concrete and Abstract Semantics to Check Secure Information Flow in Concurrent Programs, Fundamenta Informaticae, num. 1-4, vol. 60, pp. 81-98, 2004
  
  
• C. Bernardeschi, N. De Francesco, G. Lettieri, L. Martini, Checking secure information flow in Java bytecode by code transformation and standard bytecode verification, Software-Practice & Experience, num. 13, vol. 34, pp. 1225-1255, 2004
  
  
• R. Barbuti, C. Bernardeschi, N. De Francesco, Analyzing Information Flow Properties in Assembly Code by Abstract Interpretation, Computer Journal, num. 1, vol. 47, pp. 25-45, 2004
  
  
• M. Avvenuti, C. Bernardeschi, N. De Francesco, Java bytecode verification for secure information flow, ACM Sigplan Notices, num. 12, vol. 38, pp. 20-27, 2003
  
  
• R. Barbuti, C. Bernardeschi, N. De Francesco, Abstract interpretation of operational semantics for secure information flow, Information Processing Letters, num. 2, vol. 83, pp. 101-108, 2002
  
  
• C. Bernardeschi, N. De Francesco, G. Lettieri, An Abstract Semantics Tool for Secure Information Flow of Stack-based Assembly Programs, Microprocessors and Microsystems, num. 8, vol. 26, pp. 391-398, 2002
  
  
• C. Bernardeschi, A. Fantechi, S. Gnesi, Model checking fault tolerant systems, Software Testing, Verification and Reliability, num. 4, vol. 12, pp. 251-275, 2002
  
  
• C. Bernardeschi, A. Fantechi, S. Gnesi,Formal Validation of Fault -tolerance Mechanisms inside GUARDS, Reliability Engineering and System Safety, num. 71,pp 261-270, 2001
  
  
• C. Bernardeschi, N. De Francesco, G. Vaglini. An approach to system design based on P/T net simulation, Information and Software Technology, vol. 43, num. 10,pp 591,tot.pag 15, 2001
  
  
• C. Bernardeschi, A. Fantechi, L. Simoncini. Formally Verifying Fault Tolerant System Designs, The Computer Journal, Oxford University Press, Vol. 43, n. 3, pp. 191-205, 2000
  
  

Conferences

• Andrea Domenici, Cinzia Bernardeschi. A Logic Theory Pattern for Linearized Control Systems. Proceedings F-IDE 2021. Electronic Proceedings in Theoretical Computer Science vol. 338, ISSN 2075-2180, Open Publishing Association, 46–52, 2021.
  
  
• Cinzia Bernardeschi, Andrea Domenici, Maurizio Palmieri, Sergio Saponara, Tanguy Sassolas, Arief Wicaksana, Lilia Zaourar. Cross-level Co-simulation and Verification of an Automatic Transmission Control on Embedded Processor. Software Engineering and Formal Methods. SEFM 2020 Collocated Workshops, Revised Selected Papers. Editors: Cleophas, Loek, Massink, Mieke (Eds.) , LNCS 12524: 263-279, 2021.
  
  
• Cinzia Bernardeschi, Andrea Domenici, Maurizio Palmieri, Adriano Fagiolini. Co-simulation of bio-inspired multi-agent algorithms. Proceedings of the 2020 Summer Simulation Conference, SummerSim '20, 1–12, ACM Digital Library, 2020.
  
  
• Cinzia Bernardeschi, Andrea Domenici, Francesco Mercaldo, Antonella Santone. Identify Potential Attacks from Simulated Log Analysis. IJCNN 2020: 1-6, 2020.
  
  
• Cinzia Bernardeschi, Gianluca Dini, Maurizio Palmieri, Francesco Racciatti. Analysis of Security Attacks in Wireless Sensor Networks: From UPPAAL to Castalia. ICISSP 2020: 815-824, 2020.
  
  
• Cinzia Bernardeschi, Pierpaolo Dini, Andrea Domenici, Sergio Saponara, Co-simulation and verification of a non-linear control system for cogging torque reduction in brushless motors. Workshop on Formal Co-Simulation of Cyber-Physical Systems, SEFM Workshops, 2019
  
  
• Cinzia Bernardeschi, Andrea Domenici. Application of Model Checking to Fault Tolerance Analysis. In: ter Beek M., Fantechi A., Semini L. (eds) From Software Engineering to Formal Methods and Tools, and Back. Lecture Notes in Computer Science, vol 11865, Springer, Cham, 531-547, 2019.
  
  
• Cinzia Bernardeschi, Andrea Domenici, Maurizio Palmieri. Modeling and Simulation of Attacks on Cyber-physical Systems. 3rd International Workshop on FORmal methods for Security Engineering (ICISSP Workshop), 2019: 700-708
  
  
• Cinzia Bernardeschi, Francesco Mercaldo, Vittoria Nardone, Antonella Santone. Exploiting Model Checking for Mobile Botnet Detection. Procedia Computer Science, Special issue on Knowledge-Based and Intelligent Information & Engineering Systems International Conference (KES2019), Volume 159: 963-972, Elsevier, 2019.
  
  
• Cinzia Bernardeschi, Paolo Masci, Antonella Santone. Data Leakage in Java Applets with Exception Mechanism. ITASEC 2018, 2018
  
  
• Cinzia Bernardeschi, Adriano Fagiolini, Maurizio Palmieri, Giulio Scrima, Fabio Sofia. ROS/Gazebo Based Simulation of Co-operative UAVs. MESAS 2018: 321-334, 2018
  
  
• Ludovica Bozzoli, Corrado De Sio, Luca Sterpone, Cinzia Bernardeschi. PyXEL: An Integrated Environment for the Analysis of Fault Effects in SRAM-Based FPGA Routing. RSP 2018: 70-75, 2018
  
  
• Maurizio Palmieri, Cinzia Bernardeschi, Paolo Masci. A Flexible Framework for FMI-Based Co-Simulation of Human-Centred Cyber-Physical Systems. STAF Workshops 2018: 21-33, 2018
  
  
• Cinzia Bernardeschi, Andrea Domenici, Maurizio Palmieri.Towards Stochastic FMI Co-Simulations: Implementation of an FMU for a Stochastic Activity Networks Simulator. STAF Workshops 2018: 34-44, 2018
  
  
• Maurizio Palmieri, Cinzia Bernardeschi, Andrea Domenici, Adriano Fagiolini. Demo: Co-simulation of UAVs with INTO-CPS and PVSio-web. STAF Workshops 2018: 52-57, 2018
  
  
• Maurizio Palmieri, Cinzia Bernardeschi, Paolo Masci. Co-simulation of Semi-autonomous Systems: The Line Follower Robot Case Study. Workshop on Formal Co-Simulation of Cyber-Physical Systems, SEFM Workshops 2017: 423-437, 2017
  
  
• Cinzia Bernardeschi, Marco Di Natale, Gianluca Dini, Maurizio Palmieri, Verifying Data Secure Flow in AUTOSAR Models by Static Analysis. ICISSP 2017: 704-713
  
  
• Cinzia Bernardeschi, Marco Di Natale, Gianluca Dini, Dario Varano, Modeling and generation of secure component communications in AUTOSAR. SAC 2017: 1473-1480
  
  
• Cinzia Bernardeschi, Gabriele Del Vigna, Marco Di Natale, Gianluca Dini, Dario Varano. Using AUTOSAR High-Level Specifications for the Synthesis of Security Components in Automotive Systems. MESAS 2016, LNCS 9991: 101-117, 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
  
  
• 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
  
  
• Cinzia Bernardeschi, Mario G. C. A. Cimino, Andrea Domenici, Gigliola Vaglini. Using smartwatch sensors to support the acquisition of sleep quality data for supervised machine learning, In 6th EAI International Conference on Wireless Mobile Communication and Healthcare (MOBIHEALTH 2016), Milano, Italy, November 14-16, 2016.
  
  
• Marco Avvenuti, Cinzia Bernardeschi, Mario G. C. A. Cimino, Guglielmo Cola, Andrea Domenici, Gigliola Vaglini. Detecting elderly behavior shift via smart devices and stigmergic receptive fields, In 6th EAI International Conference on Wireless Mobile Communication and Healthcare (MOBIHEALTH 2016), Milano, Italy, November 14-16, 2016
  
  
• Cinzia Bernardeschi, Andrea Domenici, Paolo Masci. Towards a Formalization of System Requirements for an Integrated Clinical Environment. In 5th EAI International Conference on Wireless Mobile Communication and Healthcare (MOBIHEALTH 2015) London, 2015
  
  
• Domenico Sorrenti, Dario Cozzi, Sebastian Korf, Luca Cassano, Jens Hagemeyer, Mario Porrmann and Cinzia Bernardeschi. Exploiting Dynamic Partial Reconfiguration for On-Line On-Demand Testing of Permanent Faults in Reconfigurable Systems. International Symposium on Defect and Fault Tolerance in VLSI and Nanotechnology Systems, October 1-3, 2014
  
  
• Luca Cassano, Dario Cozzi, Dirk Jungewelter, Sebastian Korf, Jens Hagemeyer, Mario Porrmann, Cinzia Bernardeschi. An inter-processor communication interface for data-flow centric heterogeneous embedded multiprocessor systems. DTIS 2014: 1-6, 2014.
  
  
• Paolo Masci, Yi Zhang, Paul L. Jones, Patrick Oladimeji, Enrico D'Urso, Cinzia Bernardeschi, Paul Curzon, Harold Thimbleby. Combining PVSio with Stateflow. NASA Formal Methods 2014: 209-214, 2014
  
  
• Cinzia Bernardeschi, Luca Cassano, Andrea Domenici. Formal approaches to SEU testing in FPGAs. AHS 2013: 209-216, 2013
  
  
• Federico Baronti, Cinzia Bernardeschi, Luca Cassano, Andrea Domenici, Roberto Roncella, Roberto Saletti. Mitigation of Single Event Upsets in the Control Logic of a Charge Equalizer for Li-ion Batteries. In IECON 2013 the 39th Annual Conference of the IEEE Industrial Electronics Society, Vienna, Austria, November 10-13, 2013
  
  
• Cinzia Bernardeschi, Luca Cassano, Andrea Domenici, Luca Sterpone. Unexcitability analysis of SEus affecting the routing structure of SRAM-based FPGAs. ACM Great Lakes Symposium on VLSI 2013: 7-12, 2013
  
  
• Bernardeschi C, Cassano L, Domenici A, Sterpone L (2012). Accurate Simulation of SEUs in the Configuration Memory of SRAM-based FPGAs. In: IEEE International Symposium on Defect and Fault Tolerance in VLSI and Nanotechnology Systems (DFT), 2012. p. 115-120, IEEE, ISBN: 9781467330435, Austin, Texas, U.S.A., Oct. 3-5.
  
  
• Bernardeschi C, Cassano L, Cimino M, Domenici A (2012). Application of a Genetic Algorithm for Testing SEUs in SRAM-FPGA Systems. In: 6th HiPEAC Workshop on Reconfigurable Computing. p. 1-10, Parigi, Jan. 24.
  
  
• Bernardeschi C, Cassano L., Domenici A. (2012). SEU-X: a SEu Un-eXcitability prover for SRAM-FPGAs. In: Proceedings of The 18th IEEE International On-Line Testing Symposium. p. 25-30, ISBN: 9781467320832, Sitges, Spagna, June 27.
  
  
• Bernardeschi C, Cassano L, Domenici A, Masci P (2011). A Tool for Signal Probability Analysis of FPGA-Based Systems. In: (a cura di): Kenneth Scerri, Pascal Lorenz, International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking. p. 13-18, IARIA, ISBN: 9781612081595, Rome, Italy, Sept. 25.
  
  
• Bernardeschi C, Cassano L, Domenici A, Gennaro G, Pasquariello M (2011). Simulated Injection of Radiation-Induced Logic Faults in FPGAs. In Third International Conference on Advances in System Testing and Validation Lifecycle. p. 84-89, IARIA, ISBN: 9781612081687, Barcelona, Oct. 23- 29.
  
  
• Bernardeschi C, Cassano L, Domenici A (2011). Failure Probability and Fault Observability of SRAM-FPGA Systems. In: Peter Athanas, Dionisios Pnevmatikatos, Nicolas Sklavos, Eds, International Conference on. Field Programmable Logic and Applications (FPL) p. 385-388, IEEE, ISBN: 9781457714849, Chania, Greece, Sept. 5-7.
  
  
• Bernardeschi C, Cassano L, Domenici A (2011). Failure Probability of SRAM-FPGA Systems with Stochastic Activity Networks. In: IEEE 14th International Symposium on Design and Diagnostics of Electronic Circuits and Systems (DDECS),p. 293-296, IEEE, ISBN: 9781424497553, Cottbus, Germany, April 13-15.
  
  
• Bernardeschi C., Cassano L. M., Domenici A., Masci P. M. (2010), Debugging PVS specifications of control logics via event-driven simulation, COMPUTATION TOOLS 2010, Lisbon, Portugal.
  
  
• Avvenuti M, Bernardeschi C., De Francesco N, Masci P (2009). A tool for checking secure interaction in Java Cards. In: Proceedings of the 12th European Workshop on Dependable Computing (EWDC-09). Toulouse, France.
  
  
• Bernardeschi C., Masci P, Pfeifer H (2009). Analysis of wireless sensor network protocols in dynamic scenarios. In: Proceedings of the 11th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS09). France, vol. LNCS 5873, p. 105-119
  
  
• Domenici A, Bernardeschi C. (2009). Extended matchmaking with availability metrics in the WLCG/EGEE production Grid. In: Proceedings of the IASTED International Conference on Parallel and Distributed Computing and Networks (PDCN 2009). Innsbruck, Austria, p. 83-90
  
  
• Bernardeschi C., Masci P, Pfeifer H (2008). Early prototyping of wireless sensor network algorithms in PVS. In: Proceedings of the 27th International Conference on Computer Safety, Reliability and Security (SAFECOMP08). Newcastle, vol. LNCS 5219, p. 346-359
  
  
• C. Bernardeschi, G. Lettieri, L. Martini, P. Masci, A Space-Aware Bytecode Verifier for Java Cards, First Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode 2005), vol. ENTCS 141, Issue 1, pp 237-254, vol. 141, 2005 Bernardeschi C., Dini G, Domenici A (2005). FACT: a Tool for Code Generation from Communicating Automata. In: Proceedings of the 23rd IASTED International Conference on Software Engineering. Innsbruck, Austria, vol. 1, p. 313-318
  
  
• C. Bernardeschi, L. Martini, P. Masci, Java bytecode verification with dynamic structures, IASTED International Conference on Software Engineering and Applications, Acta Press, pp. 559-564, MIT, Cambridge, USA, 2004
  
  
• C. Bernardeschi, L. Martini, Enforcement of Applet Boundaries in Java Card Systems, IASTED International Conference on Software Engineering and Applications (SEA 2004), Acta Press, pp. 96-101, MIT, Cambridge, USA, 2004
  
  
• C. Bernardeschi, N. De Francesco, G. Lettieri, Concrete and Abstract Semantics to check Information Flow in Concurrent programs, Concurrency Specification and Programming CS&P'2003, vol. 1, pp. 79-91, Czarna (Polonia) 2003
  
  
• C. Bernardeschi, N. De Francesco, L. Martini, Efficient Bytecode Verification using Immediate Postdominators in Control Flow Graphs, Workshop on Java Technologies for Real Time and Embedded Systems, LNCS 2889, pp. 425-436, Catania 2003
  
  
• R. Barbuti, C. Bernardeschi, N. De Francesco, Checking Security of Java Bytecode by Abstract Interpretation, Proceedings of the 2002 ACM Symposium on Applied Computing, SAC2002, pp. 229-236, Madrid 2002.
  
  
• R. Barbuti, L. Tesei, C. Bernardeschi, N. De Francesco, Fixing the Java Bytecode Verifier by a Suitable Type Domain, SEKE'02, vol. 1, pp. 377-382, Ischia 2002
  
  
• C. Bernardecshi, N. De Francesco, Combining Abstract Interpretation and Model Checking for Analysing Security Properties of Java Bytecode, Proceedings of Third International Workshop on Verification, Model Checking, and Abstract Interpretation, VMCAI 2002, LNCS 2294, pp. 1-15, Venezia 2002
  
  
• C. Bernardeschi, N. De Francesco, G. Lettieri, Using Standard Verifier to Check Secure Information Flow in Java Bytecode, COMPSAC'02, vol. 1, pp. 850-855, Oxford 2002
  
  

Book chapters

• Cinzia Bernardeschi, Andrea Domenici, Paolo Masci. Logic-Based Formalization of System Requirements for Integrated Clinical Environments. In: Liò, Pietro, Zuliani, Paolo (Eds.) Automated Reasoning for Systems Biology and Medicine, Springer, 215-242, 2019.
  
  
• C. Bernardeschi, A. Fantechi, S. Gnesi. Chapter 10 - Formal Verification, A generic fault-tolerant architecture for real-time dependable systems, (Powell D. editor), Kluwer Academic Publishers, 2001.