Asieh Salehi Fathabadi is a senior research fellow in the cyber-physical systems group at the University of Southampton, UK. Her main research area is formal methods for software engineering. She has spent the past 10 years working on several research projects to propose and facilitate use of formal methods for design and verification of safe and secure software-based systems.
My main research interest is model-based formal methods, in particular a formal method called Event-B, for software engineering. Formal methods are mathematically rigorous techniques for the specification, development and verification of software and hardware systems and hence can contribute to the reliability and robustness of a design. My research work includes application, tools and methodology for formal methods.
I am also interested in Public Engagement (PE) activities to engage children with my ongoing research. A video of my PE activities is available here.
Research Projects:
Salehi Fathabadi, Asieh and Butler, Michael (2010) Applying Event-B Atomicity Decomposition to a Multi Media Protocol. FMCO Formal Methods for Components and Objects. pp. 89-104 . (doi:10.1007/978-3-642-17071-3_5).
Salehi Fathabadi, Asieh, Rezazadeh, Abdolbaghi and Butler, Michael (2011) Applying Atomicity and Model Decomposition to a Space Craft System in Event-B. THIRD NASA FORMAL METHODS SYMPOSIUM, Pasadena, California. 17 - 19 Apr 2011.
Butler, Michael, Salehi Fathabadi, Asieh and Silva, Renato (2012) Event-B and Rodin. In, Boulanger, Jean-Louis (ed.) Industrial Use of Formal Methods: Formal Verification. Chichester, GB. ISTE; Wiley, pp. 215-245.
Salehi Fathabadi, Asieh, Butler, Michael and Rezazadeh, Abdolbaghi (2012) A systematic approach to atomicity decomposition in Event-B. [in special issue: Software Engineering and Formal Methods. 10th International Conference, SEFM 2012, Thessaloniki, Greece, October 1-5, 2012. Proceedings] Lecture Notes in Computer Science, 7504, 78-93. (doi:10.1007/978-3-642-33826-7_6).
Salehi Fathabadi, Asieh (2012) An approach to atomicity decomposition in the Event-B formal method. University of Southampton, Electronics and Computer Science, Doctoral Thesis, 276pp.
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).
Alkhammash, Eman, Salehi Fathabadi, Asieh, Butler, Michael and Cirstea, Corina (2013) Building Traceable Event-B Models from Requirements. Automated Verification of Critical Systems (AVoCS 2013).
Pereverzeva, Inna, Butler, Michael and Salehi Fathabadi, Asieh et al. (2014) Formal derivation of distributed MapReduce. 4th International ABZ 2014 Conference, , Toulouse, France. 01 - 05 Jun 2014. 17 pp .
Salehi Fathabadi, Asieh, Snook, Colin and Butler, Michael (2014) Applying an integrated modelling process to run-time management of many-core systems. 11th International Conference on Integrated Formal Methods (iFM), Bertinoro, Italy. 08 - 10 Sep 2014.
Salehi Fathabadi, Asieh, Butler, Michael and Rezazadeh, Abdolbaghi (2015) Language and tool support for event refinement structures in Event-B. Formal Aspects of Computing, 27 (3), 499-523. (doi:10.1007/s00165-014-0311-1).
Alkhammash, Eman, Butler, Michael, Fathabadi, Asieh Salehi and Cîrstea, Corina (2015) Building traceable Event-B models from requirements. Science of Computer Programming, 1- 21. (doi:10.1016/j.scico.2015.06.002).
Salehi Fathabadi, Asieh, Maeda-Nunez, Luis Alfonso, Butler, Michael, Al-Hashimi, Bashir and Merrett, Geoff (2015) Towards automatic code generation of run-time power management for embedded systems using formal methods. 9th International Symposium on Embedded Multicore/Many-core Systems-on-Chip (MCSoC-15), Turin, Italy. 22 - 24 Sep 2015. 8 pp .
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).
Akeel, Fatmah, Salehi Fathabadi, Asieh, Paci, Federica, Gravell, Andy and Wills, Gary (2016) Formal modelling of data integration systems security policies. Data Science and Engineering, 1 (3), 139-148. (doi:10.1007/s41019-016-0016-y).
Salehi Fathabadi, Asieh, Butler, Michael and Snook, Colin (2016) Extending Code Generation to Support Platform-Independent Event-B Models. Rodin Developer Workshop, 2016. p. 21 .
Hoang, Son, Voisin, Laurent, Salehi Fathabadi, Asieh, Butler, Michael, Wilkinson, Toby and Beauger, Nicolas (2017) Theory plug-in for Rodin 3.x. arXiv, abs/1701.08625, 1-9.
Dghaym, Dana, Salehi Fathabadi, Asieh and Snook, Colin (2016) Using Rodin and BMotionStudio for public engagement. Rodin Developer Workshop 2016, Linz, Austria.
Hoang, Thai Son, Salehi Fathabadi, Asieh, Butler, Michael and Voisin, Laurent (2016) Theory plug-in for Rodin 3.x. 6th Rodin User and Developer Workshop, Linz, Austria. 22 May 2016. 2 pp .
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, Snook, Colin, Salehi Fathabadi, Asieh, Butler, Michael and Ladenberger, Lukas (2017) Validating and verifying the requirements and design of a haemodialysis machine using the rodin toolset. Science of Computer Programming. (doi:10.1016/j.scico.2017.11.002).
Salehi Fathabadi, Asieh, Butler, Michael J., Yang, Sheng, Maeda-Nunez, Luis, Bantock, James, Al-Hashimi, Bashir M. and Merrett, Geoff V. (2018) A model-based framework for software portability and verification in embedded power management systems. Journal of Systems Architecture, 82, 12-23. (doi:10.1016/j.sysarc.2017.12.001).
Dalvandi, Mohammad Sadegh, Butler, Michael, Rezazadeh, Abdolbaghi and Salehi Fathabadi, Asieh (2018) Verifiable code generation from scheduled event-B models. In Abstract State Machines, Alloy, B, TLA, VDM, and Z: ABZ 2018. vol. 10817, Springer. pp. 1-15 . (doi:10.1007/978-3-319-91271-4_16).
Dalvandi, Mohammad Sadegh, Salehi Fathabadi, Asieh and Butler, Michael (2018) Using formal methods for automatic platform-independent code generation of run-time management. University Booth at DATE 2018, Maritim Hotel & Internationales Congress Center, Dresden, Germany. 19 - 22 Mar 2018.
Dalvandi, Mohammad Sadegh, Salehi Fathabadi, Asieh and Butler, Michael (2018) A report on PRiME code generation activities. 7th Rodin Workshop, , Southampton, United Kingdom. 04 Jun 2018.
Salehi Fathabadi, Asieh, Dalvandi, Mohammad Sadegh and Butler, Michael (2019) Developing portable embedded software for multicore systems through formal abstraction and refinement. In, Al-Hashimi, Bashir M. and Merrett, Geoff V. (eds.) Many-Core Computing: Hardware and Software. Institute of Engineering and Technology, IET.
Dalvandi, Mohammad Sadegh, Butler, Michael and Salehi Fathabadi, Asieh (2019) SEB-CG: Code generation tool with algorithmic refinement support for Event-B. Practical Formal Verification for Software Dependability: co-located with the Formal Methods 2019 (FM'19), , Porto, Portugal. 07 Oct 2019.
Salehi Fathabadi, Asieh, Dalvandi, Mohammadsadegh, Butler, Michael and Al-Hashimi, Bashir M. (2019) Verifying cross-layer interactions through formal model-based assertion generation. IEEE Embedded Systems Letters. (doi:10.1109/LES.2019.2955316).
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].
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 .
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 .
Salehi Fathabadi, Asieh, Aït Ameur, Yamine, Hoang, Thai Son and Snook, Colin (2021) Proceedings of the 9th Rodin User and Developer Workshop, 2021 ,
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.
Email: asf1g08@soton.ac.uk