Paolo Masci

Paolo Masci

Senior Research Scientist

Formal Methods Group

Tel: (757) 864-9978

Email: paolo.masci@nianet.org

Paolo Masci

Education

  • Ph.D, University of Pisa, 2008
  • MSc, University of Pisa, 2003

Work Experience

  • Senior Research Scientist, National Institute of Aerospace, USA, 2018-present
  • Senior Researcher, INESC-TEC and University of Minho, Portugal, 2016-2018
  • External Software Assessor for the Medicines and Healthcare products Regulatory Agency (MHRA), UK, 2015-2016
  • Post-Doctoral Researcher, Queen Mary University of London, UK, 2010-2015
  • Post-Doctoral Researcher, University of Pisa, Italy, 2009-2010
  • Post-Doctoral Researcher, Italian National Research Council (CNR), Italy, 2009
  • Research Assistant, University of Pisa, Italy, 2004-2009

Research Areas/Expertise

  • Formal Methods and Automated Reasoning
  • Application of Formal Methods to Human-Machine Interface Design
  • Design and Analysis of High-Confidence Software
  • Rapid Prototyping
  • Model-Based Development

Current Research

Rapid prototyping of interactive cockpit display systems using formal methods tools

Rapid prototyping is an analysis method for assessing the quality of a system early in the development process, before the actual system is built. It involves creating a representation of the final system (e.g., an interactive simulation) that can be used to demonstrate and test the behavior of the final system. Several prototyping tools exist, but none of them cannot be easily integrated with formal methods technologies necessary for design verification activities. My research contributes to the development of a novel prototyping toolkit for modeling and analysis of interactive cockpit displays using the PVS verification tool.

Development of next-generation theorem proving system tool

Theorem proving systems are advanced analysis tools for modeling and analysis of critical systems. Using theorem proving tools usually requires advanced mathematical knowledge and skills, resulting in steep learning curves for developers. My research aims to reduce this learning curve, by creating novel front-ends that automate typical modeling and analysis tasks carried out by developers. The specific theorem proving system I am working on is PVS, a state-of-the-art verification tool developed at SRI International and extensively used at NASA LaRC for verifying detect and avoid algorithms in aircraft systems.

Publications

Dr. Masci has published 70+ peer-reviewed articles on formal verification, software engineering, and healthcare informatics (see also Orcid profile: http://orcid.org/0000-0002-0667-7763, Scopus profile: https://www.scopus.com/authid/detail.uri?authorId=55633702700  )


Journals

M. Palmieri, C. Bernardeschi, P. Masci, “A framework for FMI-based co-simulation of human-machine interfaces”, Software and Systems Modeling, Springer, 2019, https://doi.org/10.1007/s10270-019-00754-9

C. Bernardeschi, A. Domenici, P. Masci, “Logic-based formalization of system requirements for integrated clinical environments”, Automated Reasoning for System Biology and Medicine, Computational Biology, vol 30, Springer, 2019,https://doi.org/10.1007/978-3-030-17297-8_8

Y. Zhang, P. Masci, P. Jones, H. Thimbleby, “User interface software errors in medical devices: a study of US device recall data”, AAMI Biomedical Instrumentation & Technology, 53(3), 2019, https://www.aami-bit.org/doi/10.2345/0899-8205-53.3.182


M.D. Harrison, L. Freitas, M. Drinnan, J.C. Campos, P. Masci, C. di Maria, M. Whitaker: “Formal techniques in the safety analysis of software components of a new dialysis machine”, Science of Computer Programming, vol 175, 2019, https://doi.org/10.1016/j.scico.2019.02.003

M.D. Harrison, P. Masci, J.C. Campos: “Verification templates for the analysis of user interface software design”, IEEE Transactions on Software Engineering, 2018, http://doi.org/10.1109/TSE.2018.2804939

C. Bernardeschi, A. Domenici, P. Masci: “A PVS-Simulink Integrated Environment for Model-Based Analysis of Cyber-Physical Systems”, IEEE Transactions on Software Engineering, 44(6), 2017, http://doi.org/10.1109/TSE.2017.2694423

M.D. Harrison, P. Masci, J.C. Campos, P. Curzon: “Verification of User Interface Software: The Example of Use-Related Safety Requirements and Programmable Medical Devices”, IEEE Transactions on Human-Machine Systems, 47(6), 2017, https://doi.org/10.1109/THMS.2017.2717910

P. Masci, R. Rukšėnas, P. Oladimeji, A. Cauchi, A. Gimblett, Y. Li, P. Curzon, H. Thimbleby: 
“The benefits of formalising design guidelines: A case study on the predictability of drug infusion pumps” Innovations in Systems and Software Engineering, Springer, 11(2), 2015, http://dx.doi.org/10.1007/s11334-013-0200-4

P. Masci, P. Curzon, D. Furniss, A. Blandford: “Using PVS to support the analysis of distributed cognition systems” Innovations in Systems and Software Engineering, Springer, 11(2), 2015, http://dx.doi.org/10.1007/s11334-013-0202-2

M.D. Harrison, J. Campos, P. Masci: “Reusing models and properties in the analysis of similar interactive devices” Innovations in Systems and Software Engineering, Springer, 11(2), 2015, http://dx.doi.org/10.1007/s11334-013-0201-3

F. Di Giandomenico, M.L. Itria, P. Masci, N. Nostro: “Automated synthesis of dependable mediators for heterogeneous interoperable systems” Reliability Engineering & System Safety, vol 132, pp 220–232, ISSN:0951-8320, 2014, http://dx.doi.org/10.1016/j.ress.2014.08.001

D. Furniss, P. Masci,P. Curzon, A. Mayer, A. Blandford: “Exploring medical device design and use through layers of Distributed Cognition: How a glucometer is coupled with its context” Journal of Biomedical Informatics, ISSN: 1532-0464, 2014, http://dx.doi.org/10.1016/j.jbi.2014.12.006

M. Avvenuti, C. Bernardeschi, N. De Francesco, P. Masci: “JCSI: A Tool for Checking Secure Information Flow in Java Card Applications” Elsevier Journal of Systems and Software, May 2012, http://dx.doi.org/10.1016/j.jss.2012.05.061

C. Bernardeschi, L. Cassano, A. Domenici, P. Masci: “Simulation and Test-Case Generation for PVS Specifications of Control Logics” International Journal On Advances in Software, vol 4, ISSN: 1942-2628, 2011, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.675.8285

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, http://dx.doi.org/10.1145/1452044.1452047

M. Avvenuti, P. Corsini, P. Masci, A. Vecchio: “An application adaptation layer for wireless sensor networks” Pervasive and Mobile Computing, vol. 3(4), pp. 413–438, ISSN: 1574-1192, 2007, http://dx.doi.org/10.1016/j.pmcj.2007.04.001

M. Avvenuti, P. Corsini, P. Masci, A. Vecchio: “Energy efficient reception of large preambles in MAC protocols for wireless sensor networks” Electronic Letters, vol 43(5), 2007, https://doi.org/10.1049/el:20073919

C. Bernardeschi, G. Lettieri, L. Martini, P. Masci: “Using postdominators to reduce space requirements in dataflow analysis” Information Processing Letters, vol 98(1), 2006, https://doi.org/10.1016/j.ipl.2005.11.017

C. Bernardeschi, G. Lettieri, L. Martini, P. Masci: “Using control dependencies for space-aware bytecode verification” The Computer Journal, vol 49(2) 2006, https://doi.org/10.1093/comjnl/bxh161


Book Chapters

M.D. Harrison, P. Masci, J.C. Campos, P. Curzon: “The Specification and Analysis of Use Properties of a Nuclear Control System.” In Handbook of Formal Methods in Human-Computer Interaction, 2017, https://doi.org/10.1007/978-3-319-51838-1_21

R. Rukšėnas, P. Masci, P. Curzon: “ Developing and Verifying User Interface Requirements for Infusion Pumps: A Refinement Approach. From Action Systems to Distributed Systems: The Refinement Approach.” From Actions Systems to Distributed Systems: the Refinement Approach, Chapter 15, 2016, http://dx.doi.org/10.1201/b20053-21


International Conferences and Workshops with Peer Review

P. Masci, C. Munoz: “An Integrated Development Environment for the Prototype Verification System”, in F-IDE 2019, 5thWorkshop on Integrated Development Environments, Electronic Proceedings in Theoretical Computer Science (EPTCS), vol 310, 2019, http://doi.org/10.4204/EPTCS.310.5

M.D. Harrison, P. Masci, J.C. Campos: “Formal modelling as a component of user centred design.” in FMIS2018, 7th International Workshop on Formal Methods for Interactive Systems, Lecture Notes in Computer Science (LNCS), vol 11176, Springer, 2018 https://doi.org/10.1007/978-3-030-04771-9_21

M. Palmieri, C. Bernardeschi, P. Masci: “A Flexible Framework for FMI-based Co-Simulation of Human-Centred Cyber-Physical Systems., in CoSim-CPS-18, 2nd Workshop on Formal Co-Simulation of Cyber-Physical Systems, Lecture Notes in Computer Science (LNCS), vol 11176, Springer, 2018, https://doi.org/10.1007/978-3-030-04771-9_2

N. Watson, S. Reeves, P. Masci: “Integrating user design and formal models within PVSio-Web.” in F-IDE-18, 4thWorkshop on Formal Integrated Development Environment, Electronic Proceedings in Theoretical Computer Science (EPTCS), vol 284, 2018 http://doi.org/10.4204/EPTCS.284.8

C. Silva, P. Masci, Y. Zhang, P. Jones, J.C. Campos: “A Use Error Taxonomy for Improving Human-Machine Interface Design in Medical Devices”, in M-CPS-18, Medical Cyber-Physical Systems Workshop 2018, ACM SIGBED Review newsletter, 2018 (to apper)

C. Bernardeschi, P. Masci, D. Caramella, R. 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.”, in M-CPS-18, Medical Cyber Physical Systems Workshop 2018, ACM SIGBED Review newsletter, 2018 (to appear)

C. Bernardeschi, P. Masci, A. Santone: “Data Leakage in Java applets with Exception Mechanism.” in ITASEC18, Italian Conference on Cyber-Security, CEUR Workshop Proceedings, vol 2058, 2018 http://ceur-ws.org/Vol-2058/

M. Palmieri, C. Bernardeschi, P. Masci: “Co-simulation of semi-autonomous systems: the Line Follower Robot case study” In CoSim-CPS, 1st Workshop on Formal Co-Simulation of Cyber-Physical Systems, Lecture Notes in Computer Science (LNCS), vol 10729, Springer, 2018, https://doi.org/10.1007/978-3-319-74781-1_29

P. Masci, Y. Zhang, P. Jones and J.C. Campos: “A Hazard Analysis Method for Systematic Identification of Safety Requirements for User Interface Software in Medical Devices.” In SEFM17, 15th International Conference on Software Engineering and Formal Methods, Lecture Notes in Computer Science (LNCS), vol 10469, 2017, https://doi.org/10.1007/978-3-319-66197-1_18

M.D. Harrison, M. Drinnan, J.C. Campos, P. Masci, L. Freitas, C. Di Maria, M. Whitaker: “Safety analysis of software components of a dialysis machine using model checking.” In FACS, 14th International Conference on Formal Aspects of Component Software. Springer Lecture Notes in Computer Science (LNCS) vol. 10487, 2017, https://doi.org/10.1007/978-3-319-68034-7_8

C. Fayollas, C. Martinie, P. Palanque, P. Masci, M.D. Harrison, J.C. Campos, S.R. e Silva: “Evaluation of Formal IDEs for Human-Machine Interface Design and Analysis: The Case of CIRCUS and PVSio-web” In F-IDE16, Third Workshop on Formal Integrated Development Environment, EPTCS 240, 2017, https://doi.org/10.4204/EPTCS.240.1

P. Masci, P. Oladimeji, P. Curzon, H. Thimbleby “Using PVSio-web to demonstrate software issues in medical user interfaces” In FHIES2014, 4th International Symposium on Foundations of Health Information Engineering and Systems, Lecture Notes in Computer Science (LNCS), vol 9062, 2017, https://doi.org/10.1007/978-3-319-63194-3_14

M.D. Harrison, P. Masci, J.C. Campos, P. Curzon “Demonstrating that medical devices satisfy user-related safety requirements” accepted at FHIES2014, 4th International Symposium on Foundations of Health Information Engineering and Systems, Lecture Notes in Computer Science (LNCS), vol 9062, 2017, https://doi.org/10.1007/978-3-319-63194-3_8

P. Masci, P. Oladimeji, Y. Zhang, P. Jones, P. Curzon, H. Thimbleby “PVSio-web 2.0: Joining PVS to Human-Computer-Interaction.” In CAV 2015, 27th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, vol 9206, 2015. California, USA, 2015. https://doi.org/10.1007/978-3-319-21690-4_30

P. Masci, P. Mallozzi, F.L. DeAngelis, GDM Serugendo, P. Curzon: “Using PVSio-web and SAPERE for rapid prototyping of user interfaces in Integrated Clinical Environments.” In Verisure 2015, Workshop on Verification and Assurance, co-located with CAV2015, 2015, http://fm.csl.sri.com/VeriSure2015

P. Masci, P. Oladimeji, P. Mallozzi, P. Curzon, H. Thimbleby: “PVSio-web: mathematically based tool support for the design of interactive and interoperable medical systems” MOBIHEALTH’15, 5th EAI International Conference on Wireless Mobile Communication and Healthcare, EAI Endorsed Transactions on Collaborative Computing, ACM, 16(7), 2015, http://dx.doi.org/10.4108/eai.14-10-2015.2261720

P. Masci, P. Curzon, H. Thimbleby: “Early identification of software causes of use-related hazards in medical devices” MOBIHEALTH’15, 5th EAI International Conference on Wireless Mobile Communication and Healthcare, EAI Endorsed Transactions on Collaborative Computing, ACM, 16(7), 2016, http://dx.doi.org/10.4108/eai.14-10-2015.2261720

P. Masci, L.D. Couto, P.G. Larsen, P. Curzon “Integrating the PVSio-web modelling and prototyping environment with Overture.” In Overture 2015, 2015, 13th Overture Workshop, co-located with FM2015, Oslo, Norway, 2015.

P. Masci, Y. Zhang, P. Jones, H. Thimbleby, P. Curzon “A generic user interface architecture for analyzing use hazards in infusion pump software.” In MedCPS, Medical Cyber Physical Systems Workshop 2014, OpenAccess Series in Informatics (OASIcs), Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, https://doi.org/10.4230/OASIcs.MCPS.2014.1

P. Masci, Y. Zhang, P. Jones, P. Oladimeji, E. D’Urso, C. Bernardeschi, P. Curzon, H. Thimbleby “Combining PVSio with Stateflow” In NASAFM2014, 6th NASA Formal Methods Symposium, Lecture Notes in Computer Science book series (LNCS, volume 8430), 2014, https://doi.org/10.1007/978-3-319-06200-6_16

P. Masci, Y. Zhang, P. Jones, P. Curzon, H. Thimbleby “Formal verification of medical devices using PVS” In FASE2014, 17th International Conference on Fundamental Approaches to Software Engineering, Lecture Notes in Computer Science (LNCS), vol 8411, 2014,https://doi.org/10.1007/978-3-642-54804-8_14

P. Masci, A. Ayoub, P. Curzon, I. Lee, O. Sokolsky, H. Thimbleby “Model-based development of the Generic PCA infusion pump user interface prototype in PVS.” In Safecomp2013, 32nd International Conference on Computer Safety, Reliability and Security, Lecture Notes in Computer Science, vol 8153, 2013, https://doi.org/10.1007/978-3-642-40793-2_21

P. Masci, A. Ayoub, P. Curzon, M.D. Harrison, I. Lee, H. Thimbleby “Verification of interactive software for medical devices: PCA infusion pumps and FDA regulation as an example.” In EICS2013, 5th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, ACM, 2013 https://doi.org/10.1145/2494603.2480302

P. Oladimeji, P. Masci, P. Curzon, H. Thimbleby “PVSio-web: a tool for rapid prototyping device user interfaces in PVS.” In FMIS2013, 5th Intl. Workshop on Formal Methods for Interactive Systems, Electronic Communications of the EASST, 2013, http://dx.doi.org/10.14279/tuj.eceasst.69.963

M.D. Harrison, P. Masci, J.C. Campos, P. Curzon “Automated theorem proving for the systematic analysis of interactive system.” In FMIS2013, 5th Intl. Workshop on Formal Methods for Interactive Systems, Electronic Communications of the EASST, 2013, http://dx.doi.org/10.14279/tuj.eceasst.69.962

R. Rukšėnas, P. Masci, M.D. Harrison, P. Curzon “Developing and Verifying User Interface Requirements for Infusion Pumps: A Refinement Approach.” In FMIS2013, 5th Intl. Workshop on Formal Methods for Interactive Systems, Electronic Communications of the EASST, 2013, http://dx.doi.org/10.14279/tuj.eceasst.69.964

H. Thimbleby, A. Cauchi, A, Gimblett, P. Masci, P. Curzon “Evaluating safer 5-key number entry user interface designs.” In BCS-HCI 2012, British Computer Society Conference on Human‐Computer Interaction, Birmingham, British Computer Society, 2012, http://dl.acm.org/citation.cfm?id=2377916.2377921

P. Masci, D. Furniss, P. Curzon, M.D. Harrison, A. Blandford “Supporting field investigators with PVS: a case study in the healthcare domain.”, In SERENE2012, 4th International Workshop on Software Engineering for Resilient Systems, Lecture Notes in Computer Science (LNCS), vol 7527, 2012, https://doi.org/10.1007/978-3-642-33176-3_11

P. Masci, H. Huang, P. Curzon, M.D. Harrison: “Using PVS to investigate incidents through the lens of distributedcognition.” In NASAFM2012, 4th NASA Formal Methods Symposium, Lecture Notes in Computer Science (LNCS), vol 7226, 2012, https://doi.org/10.1007/978-3-642-28891-3_27

P. Masci, P. Curzon: “Checking user-centred design principles in distributed cognition models: a case study in the healthcare domain.” In USAB2011, 7th Conference of the Austrian Computer Society on Information Quality in eHealth, Lecture Notes in Computer Science (LNCS), vol 7058, 2011, https://doi.org/10.1007/978-3-642-25364-5_10

P. Masci, R. Rukšėnas, P. Oladimeji, A. Cauchi, A. Gimblett, Y. Li, P. Curzon, H. Thimbleby: “On formalising interactive number entry on infusion pumps” In FMIS2011, 4th International Workshop on Formal Methods for Interactive Systems, Electronic Communications of the EASST, 2011, http://dx.doi.org/10.14279/tuj.eceasst.45.654

P. Masci, P. Curzon, A. Blandford, D. Furniss: “Modelling Distributed Cognition Systems in PVS” In FMIS2011, 4th International Workshop on Formal Methods for Interactive Systems, Electronic Communications of the EASST, 2011, http://dx.doi.org/10.14279/tuj.eceasst.45.653

P. Masci, P. Curzon, A. Blandford, D. Furniss, H. Huang, A. Rajkomar, R. Rukšėnas: “Towards a Formal Framework for Reasoning about the Resilience of Dynamic Interactive Systems” In EWDC2011, the 13th European Workshop on Dependable Computing, ACM, 2011, https://doi.org/10.1145/1978582.1978606

A. Cauchi, P. Curzon, P. Eslambolchilar, A. Gimblett, H. Huang, P. Lee, Y. Li, P. Masci, P. Oladimeji, R. Rukšėnas, H. Thimbleby: “Towards Dependable Number Entry for Medical Devices”, In Eics4Med, the 1st International Workshop on Engineering Interactive Computing Systems for Medicine and Health Care, CEUR Workshop Proceedings, vol 727, 2011, http://ceur-ws.org/Vol-727

A. Blandford, A. Cauchi, P. Curzon, P. Eslambolchilar, D. Furniss, A. Gimblett, H. Huang, P. Lee, Y. Li, P. Masci, P. Oladimeji, A. Rajkomar, R. Rukšėnas, H. Thimbleby: “Comparing Actual Practice and User Manuals: A Case Study Based on Programmable Infusion Pumps” In Eics4Med, the 1st International Workshop on Engineering Interactive Computing Systems for Medicine and Health Care, CEUR Workshop Proceedings, vol 727, 2011, http://ceur-ws.org/Vol-727

C. Bernardeschi, L. Cassano, A. Domenici, P. Masci: “A Tool for Signal Probability Analysis of FPGA-Based Systems” In ComputationTools2011, 2nd International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking, ISBN: 978-1-61208-159-5, 2011 https://www.thinkmind.org/download.php?articleid=computation_tools_2011_1_30_80007

P. Masci, N. Nostro, F. Di Giandomenico: “On enabling dependability assurance in heterogeneous networks through automated model-based analysis” In Serene2011, 3rd International Workshop on Software Engineering for Resilient Systems, Lecture Notes in Computer Science (LNCS), Springer, 2011, https://doi.org/10.1007/978-3-642-24124-6_7

P. Masci, M. Martinucci, F. Di Giandomenico: “Towards automated dependability analysis of dynamically connected systems” In ISADS2011, IEEE International Symposium On Autonomous Decentralised Systems, 2011 https://doi.org/10.1109/ISADS.2011.23

A. Bertolino, A. Calabró, F. Di Giandomenico, M. Martinucci, P. Masci: “Automated refinement of dependability analysis through monitoring in dynamically connected systems” In ISADS2011, IEEE International Symposium On Autonomous Decentralised Systems, 2011, https://doi.org/10.1109/ISADS.2011.46

P. Masci, F. Di Giandomenico, S. Chiaradonna: “Dependability Analysis of Diffusion Protocols in Wireless Networks with Heterogeneous Node Capabilities” In EDCC2010, IEEE European Dependable Computing Conference, 2010, https://doi.org/10.1109/EDCC.2010.26

C. Bernardeschi, L. Cassano, A. Domenici, P. Masci: “Debugging PVS Specifications of Control Logics via Event-driven Simulation” In ComputationTools2010, 1st International Conference. on Computational Logics, Algebras, Programming, Tools, and Benchmarking, 2010.

F. Di Giandomenico, M. Kwiatkowska, M. Martinucci, P. Masci, H. Qu: “Dependability Analysis and Verification for CONNECTed systems” In ISOLA2010, 4th Interntional Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Lecture Notes in Computer Science (LNCS), vol 6416, Springer, 2010, https://doi.org/10.1007/978-3-642-16561-0_27

C. Bernardeschi, P. Masci, H. Pfeifer: “Analysis of Wireless Sensor Network Protocols in Dynamic Scenarios” In SSS09, 11th International Symposium on Stabilization, Safety, and Security of Distributed Systems, Lecture Notes in Computer Science, vol 5873, Springer, 2009, https://doi.org/10.1007/978-3-642-05118-0_8

P. Masci, A. Tedeschi: “Modelling and Evaluation of a Game-Theory approach for Airborne Conflict Resolution in Omnet++” In DEPEND09, IEEE International Conference on Dependability, 2009, https://doi.org/10.1109/DEPEND.2009.31

C. Bernardeschi, P. Masci, H. Pfeifer: “Early prototyping of wireless sensor network algorithms in PVS” In SAFECOMP08, 27th International Conference on Computer Safety, Reliability and Security, Lecture Notes in Computer Science, vol 5219, Springer, 2008, https://doi.org/10.1007/978-3-540-87698-4_29

P. Corsini, P. Masci, A. Vecchio: “Configuration and Tuning of Sensor Network Applications through Virtual Sensors” In PerSens06, IEEE International Conference on Pervasive Computing and Communications, 2006, https://doi.org/10.1109/PERCOMW.2006.32

P. Corsini, P. Masci, A. Vecchio: “VirtuS: a Configurable Layer for Post-deployment Adaptation of Sensor Networks” In ICWMC06, IEEE International Conference on Wireless and Mobile Communication, 2006, https://doi.org/10.1109/ICWMC.2006.93

P. Corsini, P. Masci, A. Vecchio: “Increasing the Efficiency of Preamble Sampling Protocols for Wireless Sensor Networks” In MCWC06, IEEE International Conference on Mobile Computing and Wireless Communications, 2006, https://doi.org/10.1109/MCWC.2006.4375207

C. Bernardeschi, L. Martini, P. Masci: “Java Bytecode Verification with Dynamic Structures”, In IASTED, International Conference on Software Engineering and Applications, 2004, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.59.6729

A. Bertolino, F. Di Giandomenico, A. Di Marco, V. Issarny, F. Martinelli, P. Masci, I. Matteucci, R. Saadi, A. Sabetta: “Dependability in dynamic, evolving and heterogeneous systems: the CONNECT approach”, In SERENE2010, the 2nd International Workshop on Software Engineering for Resilient Systems, HAL archive-ouverte, 2010, https://hal.inria.fr/inria-00465229

M. Avvenuti, C. Bernardeschi, N. De Francesco, P. Masci: “A tool for checking secure interaction in Java Cards” In EWDC09, the 12th European Workshop on Dependable Computing, HAL archives-ouvertes.fr, 2009, https://hal.archives-ouvertes.fr/hal-00380664

P. Masci, H. Moniz, A. Tedeschi: “Services for fault-tolerant conflict resolution in air traffic management” In SERENE08, International Workshop on Software Engineering for Resilient Systems, Newcastle upon Tyne, UK, 2008, https://doi.org/10.1145/1479772.1479796

M. Avvenuti, P. Corsini, P. Masci, A. Vecchio: “Opportunistic Computing for Wireless Sensor Networks” In SensorFusion07, The 2nd Intl. Workshop on Information Fusion and Dissemination in Wireless Sensor Networks, IEEE, 2007, https://doi.org/10.1109/MOBHOC.2007.4428751

P. Corsini, P. Masci, A. Vecchio: “Experiences with the TinyOS Communication Library” In ICEIS06, 5th International Workshop on Wireless Information Systems, 2006, https://www.scitepress.org/papers/2006/24807/pdf/index.html

C. Bernardeschi, G. Lettieri, L. Martini, P. Masci: “A Space-Aware Bytecode Verifier for Java Cards” In BYTECODE05, the 1st Workshop on Bytecode Semantics, Verification, Analysis and Transformation, Electronic Notes in Theoretical Computer Science (ENTCS), vol 141(1): 237-254, 2005, https://doi.org/10.1016/j.entcs.2005.02.027


Invited Papers

P. Masci: “Experiences on Streamlining Formal Methods Tools,” 2nd Workshop on Practical Formal Verification for Software Dependability (AFFORD), Formal Methods World Congress Workshop post-proceedings, Lecture Notes in Computer Science, Springer, 2019 (to appear)

P. Masci: “Data-driven analysis of user interface software in medical devices” Invited Keynote talk at DATAMOD-18, 7th International Symposium on Data and Models June 2018, Toulouse, France.

P. Masci, Y. Zhang, P. Jones, J.C. Campos: “Extending STPA to Improve the Analysis of User Interface Software in Medical Devices”, invited paper at MIT STAMP Workshop, 2018

S. Anzivino, G. Quaini, V. Pisetta, P. Masci, A. Bertoldi, G. Nollo: “Implementation of a multi-specialized electronic health record for managing cardiological rehabilitation paths”, invited paper at ForItALL, Italian Forum of Ambient Assisted Living, 2018.

P. Masci, R. Rukšėnas, H. Huang, P. Curzon, M. Harrison: “Formal verification and the prevention of systematic user error” Invited paper at FormalH, Workshop on Formal Methods in Human-Machine Interaction sponsored by the IFIP Working Group 13.5 on Human Error, Safety, and System Development, May 2012, Imperial College, London, UK.

P. Curzon, M. Harrison, P. Masci, R. Rukšėnas: “Safety assurance cases, proof and the prevention of user error” Invited paper at the Workshop on Theorem Proving in Certification, December 2011, Cambridge, UK.


Public Engagement Publications

P. Masci: “Artists in disguise” in Electronic Engineering for Fun (EE4FN), vol. 1, 2012, available online at http://www.cs4fn.org/ee4fn/magazine/

P. Masci: “Lift me up!” in Computer Science for Fun (CS4FN), 2012, available online at http://www.cs4fn.org/humanerror/liftmeup.php

 


PhD and MSc Thesis

 

P. Masci: “Software Solutions for Battery-Aware Reconfiguration of Wireless Sensor Networks” 
PhD Thesis, University of Pisa, 2008.

P. Masci: “Design and Implementation of an Efficient Java Bytecode Verifier”
MSc Thesis, University of Pisa, 2003.