Lecturer in Cyber-Physical Systems
Dr Dana Dghaym is a Lecturer in the Cyber-Physical Systems group in the School of Electronics and Computer Science (ECS). Her main research area is in formal methods where she contributed to Event-B structured refinement and composition methodologies. She also has experience of tool development and verification in railway and maritime autonomous systems. In 2017, Dana was awarded her PhD in Computer Science from the University of Southampton.
Dr Dana Dghaym is interested in the formal verification and validation of safe and secure cyber physical systems. Dana is also interested in making formal modelling more accessible to industry.
Research Projects
I currently teach:
Dghaym, Dana, Butler, Michael and Salehi Fathabadi, Asieh (2014) Evaluation of graphical control flow management approaches for Event-B modelling. Proceedings of the 13th International Workshop on Automated Verification of Critical Systems (AVocS 2013), Guildford, United Kingdom. 15 pp . (doi:10.14279/tuj.eceasst.66.891).
Dghaym, Dana, Trindade, Matheus Garay, Butler, Michael and Salehi Fathabadi, Asieh (2016) A graphical tool for event refinement structures in Event-B. Abstract State Machines, Alloy, B, TLA, VDM, and Z: Proceedings of the 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Linz, Austria. pp. 269-274 . (doi:10.1007/978-3-319-33600-8_20).
Dghaym, Dana, Salehi Fathabadi, Asieh and Snook, Colin (2016) Using Rodin and BMotionStudio for public engagement. Rodin Developer Workshop 2016, Linz, Austria.
Dghaym, Dana (2017) Extending the ERS approach for workflow modelling in Event-B. University of Southampton, Doctoral Thesis, 389pp.
Hoang, Thai Son, Snook, Colin, Dghaym, Dana and Butler, Michael (2017) Class diagrams for Abstract Data Types. Hung, D. and Kapur, D. (eds.) In Theoretical Aspects of Computing – ICTAC 2017. vol. 10580, Springer. pp. 100-117 . (doi:10.1007/978-3-319-67729-3_7).
Butler, Michael, Dghaym, Dana, Fischer, Tomas, Hoang, Thai Son, Reichl, Klaus, Snook, Colin and Tummeltshammer, Peter (2017) Formal modelling techniques for efficient development of railway control products. Fantechi, A., Lecomte, T. and Romanovsky, A. (eds.) In RSSRail 2017 : Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. vol. 10598, Springer.. (doi:10.1007/978-3-319-68499-4_5).
Hoang, Thai, Snook, Colin, Dghaym, Dana and Butler, Michael (2017) RailGround using Theory plug-in. University of Southampton doi:10.5258/SOTON/D0162 [Dataset]
Hoang, Thai Son, Dghaym, Dana, Snook, Colin and Butler, Michael (2018) A composition mechanism for refinement-based methods. In Proceedings 2017 22nd International Conference on Engineering of Complex Computer Systems: ICECCS 2017. IEEE. 10 pp . (doi:10.1109/ICECCS.2017.27).
Dghaym, Dana, Butler, Michael and Salehi Fathabadi, Asieh (2018) Extending ERS for modelling dynamic workflows in Event-B. 22nd International Conference on Engineering of Complex Computer Systems, The Kyushu University, Fukuoka, Japan. 05 - 08 Nov 2017. pp. 20-29 . (doi:10.1109/ICECCS.2017.29).
Hoang, Thai Son, Dghaym, Dana, Snook, Colin and Butler, Michael (2017) Development of a System Controlling Cars on a Bridge using Machine Inclusion. University of Southampton doi:10.5258/SOTON/D0237 [Dataset]
Dghaym, Dana, Poppleton, Michael and Snook, Colin (2018) ERTMS Hybrid Level 3 - model using iUML-B/Event-B. University of Southampton doi:10.5258/SOTON/D0403 [Dataset]
Dghaym, Dana, Poppleton, Michael and Snook, Colin (2018) Diagram-led formal modelling using iUMLB for Hybrid ERTMS Level 3. In Abstract State Machines, Alloy, B, TLA, VDM, and Z: ABZ 2018. vol. 10817, Springer. pp. 338-352 . (doi:10.1007/978-3-319-91271-4_23).
Snook, Colin, Hoang, Thai Son, Dghaym, Dana, Butler, Michael, Fischer, Tomas, Schlick, Rupert and Wang, Keming (2018) Behaviour-driven formal model development. Sun, J. and Sun, M. (eds.) In Formal Methods and Software Engineering: 20th International Conference on Formal Engineering Methods, ICFEM 2018, Gold Coast, QLD, Australia, November 12-16, 2018, Proceedings. Springer. pp. 21-36 . (doi:10.1007/978-3-030-02450-5_2).
Dghaym, Dana, Hoang, Thai Son and Snook, Colin (2018) Requirements document, scenarios, and Event-B models for lift examples. University of Southampton doi:10.5258/SOTON/D0604 [Dataset]
Dghaym, Dana, Snook, Colin, Hoang, Thai Son and Butler, Michael (2018) Reusing formal models via lifting. In Proceedings - 23rd International Conference on Engineering of Complex Computer Systems, ICECCS 2018. vol. 2018-December, Institute of Electrical and Electronics Engineers Inc. pp. 189-192 . (doi:10.1109/ICECCS2018.2018.00029).
Fischer, Tomas and Dghaym, Dana (2019) Formal model validation through acceptance tests. Collart-Dutilleul, S., Lecomte, T. and Romanovsky, A. (eds.) In Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification: RSSRail 2019. vol. 11495, Springer. pp. 159-169 . (doi:10.1007/978-3-030-18744-6_10).
Snook, Colin, Hoang, Thai Son, Dghaym, Dana and Butler, Michael (2019) Domain-specific scenarios for refinement-based methods. Attiogbe, C., Ferrarotti, F. and Maabout, S. (eds.) In DETECT 2019: moDeling, vErification and Testing of dEpendable CriTical systems. Springer. pp. 18-31 . (doi:10.1007/978-3-030-32213-7_2).
Dghaym, Dana and Snook, Colin (2019) Dataset for: Formalising the Hybrid ERTMS Level 3 specification in iUML-B and Event-B. University of Southampton doi:10.5258/SOTON/D0991 [Dataset]
Dghaym, Dana, Turnock, Stephen, Butler, Michael, Downes, Jonathan, Hoang, Thai Son and Pritchard, Ben (2019) Developing a framework for trustworthy autonomous maritime systems. Valdez Banda, Osiris Alejandro, Kujala, Pentti, Hirdaris, Spyros and Basnet, Sunil (eds.) In Proceedings of the International Seminar on Safety and Security of Autonomous Vessels (ISSAV) and European STAMP Workshop and Conference (ESWC) 2019: ISSAV 2019. Sciendo. pp. 73-82 . (doi:10.2478/9788395669606-007).
Butler, Michael, Dghaym, Dana, Hoang, Thai Son, Omitola, Temitope, Snook, Colin, Fellner, Andreas, Schlick, Rupert, Tarrach, Thorsten, Fischer, Tomas and Tummeltshammer, Peter (2019) Behaviour-driven formal model development of the ETCS hybrid level 3. In The 24th International Conference on Engineering Of Complex Computer Systems: ICECCS 2019. pp. 1-10 . (In Press)
Dghaym, Dana, Dalvandi, Mohammad Sadegh, Poppleton, Michael and Snook, Colin (2019) Formalising the hybrid ERTMS level 3 specification in iUML-B and Event-B. International Journal on Software Tools for Technology Transfer. (doi:10.1007/s10009-019-00548-w).
Dghaym, Dana, Fischer, Tomas, Hoang, Thai Son, Reichl, Klaus, Snook, Colin, Schlick, Rupert and Tummeltshammer, Peter (2019) Systematic verification and testing. In, Leitner, Andrea, Watzenig, Daniel and Ibanez-Guzman, Javier (eds.) Validation and Verification of Automated Systems : Results of the ENABLE-S3 Project. Springer Nature Switzerland AG 2020. Springer, Cham, pp. 89-104. (doi:10.1007/978-3-030-14628-3_9).
Snook, Colin, Hoang, Thai Son, Dghaym, Dana, Butler, Michael and Salehi Fathabadi, Asieh (2020) Dataset for: Domain-Specific Scenarios for Refinement-based Methods. University of Southampton doi:10.5258/SOTON/D1026 [Dataset]
Snook, Colin, Hoang, Thai Son, Dghaym, Dana, Salehi Fathabadi, Asieh and Butler, Michael (2021) Domain-specific scenarios for refinement-based methods. Journal of Systems Architecture, 112, [101833].
Dghaym, Dana, Hoang, Thai Son, Turnock, Stephen, Butler, Michael, Downes, Jon and Pritchard, Ben (2021) An STPA-based formal composition framework for trustworthy autonomous maritime systems. Safety Science, 136 (0925-7535), [105139].
Hoang, Thai Son and Dghaym, Dana (2021) Dataset for "An STPA-based formal composition framework for trustworthy autonomous maritime systems". University of Southampton doi:10.5258/SOTON/D1702 [Dataset]
Hoang, Thai Son, Snook, Colin, Dghaym, Dana, Salehi Fathabadi, Asieh and Butler, Michael (2021) The CamilleX Framework for the Rodin Platform. ABZ 2021- 8th International Conference on Rigorous State Based Methods: ABZ 2021, virtual. 07 - 11 Jun 2021. pp. 124-129 .
Salehi Fathabadi, Asieh, Snook, Colin, Hoang, Thai Son, Dghaym, Dana and Butler, Michael (2021) Extensible Record Structures in Event-B. ABZ 2021- 8th International Conference on Rigorous State Based Methods: ABZ 2021, virtual. 07 - 11 Jun 2021. pp. 130-136 .
Dghaym, Dana, Hoang, Thai Son, Butler, Michael, Hu, Runshan, Aniello, Leonardo and Sassone, Vladimiro (2021) Verifying System-level Security of a Smart Ballot Box. In ABZ 2021 – 8th International Conference on Rigorous State Based Methods: ABZ 2021. Springer Nature Switzerland AG. 16 pp . (In Press)
Salehi Fathabadi, Asieh, Snook, Colin, Hoang, Thai Son, Dghaym, Dana and Butler, Michael (2021) Refinable record structures in formal methods. The International Workshop DETECT 2021. pp. 3-15 .
Hoang, Thai Son, Snook, Colin, Salehi Fathabadi, Asieh, Dghaym, Dana and Butler, Michael (2021) Towards CamilleX 3.0. 9th Rodin User and Developer Workshop, virtual. 08 - 11 Jun 2021.
Snook, Colin, Hoang, Thai Son, Salehi Fathabadi, Asieh, Dghaym, Dana and Butler, Michael (2021) Scenario Checker: An Event-B tool for validating abstract models. 9th Rodin User and Developer Workshop, virtual. 08 - 11 Jun 2021.
Telephone: +44 (0) 23 8059 29052
Email: d.dghaym@soton.ac.uk