Dr Son Hoang

Lecturer in Cyber-Physical Systems

Programme Leader for Aerospace Electronic Engeering

Dr Son Hoang is a Lecturer in the Cyber-Physical Systems Group (a part of School of Electronics and Computer Science). He was awarded a first class honours degree in Computer Engineering from the University of New South Wales (UNSW), Sydney, Australia in 2001. Subsequently, he studied for a PhD (also at UNSW) and was awarded his PhD in 2006 for his thesis on "The Development of a Probabilistic B-Method and a Supporting Toolkit".

Research

Research interests

Dr Son Hoang is interested in Formal System Development, including developing methods, tools and their application to industrial systems.

Research Projects

Teaching

Dr Son Hoang lectures on programming, software engineering and system development. He supervises a number of Undergraduate and MSc projects, and is an Admissions Tutor for the undergraduate Aerospace Electronic Engineering (AEE) degree programme.

Publications

Hoang, Thai Son, Snook, Colin, Ladenberger, Lukas and Butler, Michael (2016) Validating the requirements and design of a hemodialysis machine using iUML-B, BMotion Studio, and co-simulation. Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings. pp. 360-375 . (doi:10.1007/978-3-319-33600-8_31).

Fürst, Andreas, Hoang, Thai Son, Basin, David, Sato, Naoto and Miyazaki, Kunihiko (2016) Large-scale system development using abstract data types and refinement. Science of Computer Programming, 131, 59-75. (doi:10.1016/j.scico.2016.04.010).

Hoang, Thai Son, Schneider, Steve, Treharne, Helen and Williams, David (2016) Foundations for using linear temporal logic in Event-B refinement. Formal Aspects of Computing, 28 (6), 909-935. (doi:10.1007/s00165-016-0376-0).

Hoang, Thai Son, Snook, Colin, Ladenberger, Lukas and Butler, Michael (2016) Formal specification of a Haemodialysis Machine (HD Machine) using Event-B. University of Southampton [Dataset]

Snook, Colin, Hoang, Thai Son and Butler, Michael (2016) iUML-B model of VLAN system. University of Southampton doi:10.5258/SOTON/403533 [Dataset]

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.

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 .

Snook, Colin, Hoang, Thai Son and Butler, Michael (2017) Analysing security protocols using refinement in iUML-B. In, Barrett, Clark, Davies, Misty and Kahsai, Temesghen (eds.) NASA Formal Methods: 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings. (Lecture Notes in Computer Science, 10227) 9th NASA Formal Methods Symposium (15/05/17 - 18/05/17) Springer, pp. 84-98. (doi:10.1007/978-3-319-57288-8_6).

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]

Bogdiukiewicz, Chris, Butler, Michael, Hoang, Thai Son, Paxton, Martin, Snook, James, Harvey, Waldron, Xanthippe and Wilkinson, Toby (2017) Formal development of policing functions for intelligent systems. In 2017 IEEE 28th International Symposium on Software Reliability Engineering (ISSRE). IEEE. 11 pp . (doi:10.1109/ISSRE.2017.40).

Snook, Colin, Dghaym, Dana, Hoang, Thai Son, Butler, Michael, Reichl, Klaus, Fischer, Tomas and Tummeltshammer, Peter (2017) Railground RSSRail models - iUML-B/Event-B. University of Southampton doi:10.5258/SOTON/D0184 [Dataset]

Hudon, Simon, Hoang, Thai Son and Ostroff, Jonathan S. (2016) The Unit-B method: refinement guided by progress concerns. Software and Systems Modeling, 15 (4), 1091-1116. (doi:10.1007/s10270-015-0456-2).

Bogdiukiewicz, Chris, Butler, Michael, Hoang, Thai Son, Paxton, Martin, Snook, James, Harvey, Waldron, Xanthippe and Wilkinson, Toby (2017) Route Validation in Event-B. University of Southampton doi:10.5258/SOTON/D0217 [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).

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]

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).

Fischer, Tomas, Snook, Colin and Hoang, Thai Son (2018) Formal model validation through acceptance tests University of Southampton 14pp.

Hoang, Thai Son, Sato, Naoto, Myosin, Tomoyuki, Butler, Michael, Nakagawa, Yuichiroh and Ogawa, Hideto (2018) Policing functions for machine learning systems. Workshop on Verification and Validation of Autonomous Systems: Satellite Workshop of Floc 2018, University of Oxford, Oxford, United Kingdom. 18 - 19 Jul 2018. 10 pp . (In Press)

Hoang, Thai Son, Butler, Michael and Reichl, Klaus (2018) The hybrid ERTMS/ETCS level 3 case study. In Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Proceedings. vol. 10817 LNCS, Springer Verlag. pp. 251-261 . (doi:10.1007/978-3-319-91271-4_17).

Hoang, Thai Son and Butler, Michael (2018) Rodin Developments for Formal Policing Functions based on Metamorphic Relations. University of Southampton doi:10.5258/SOTON/D0528 [Dataset]

Snook, James, Harvey, Butler, Michael and Hoang, Thai Son (2018) Developing a new language to construct algebraic hierarchies for Event-B. In Dependable Software Engineering. Theories, Tools, and Applications: SETTA 2018. vol. 10998, Springer. pp. 135-141 . (doi:10.1007/978-3-319-99933-3_9).

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]

Snook, Colin, Morris, Karla and Hoang, Thai Son (2018) Rodin Prototype Plug-ins and Development of the SecBot Case Study. University of Southampton doi:10.5258/SOTON/D0693 [Dataset]

Morris, Karla, Snook, Colin, Hoang, Thai Son, Armstrong, Robert and Butler, Michael (2018) Refinement of statecharts with run-to-completion semantics. The Sixth International Workshop on Formal Techniques for Safety-Critical Systems, , Gold Coast, Australia. 16 Nov 2018.

Butler, Michael, Raschke, Alexander, Hoang, Thai Son and Reichl, Klaus (2018) Preface. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 10817, III-VI.

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).

Sato, Naoto, Kuruma, Hironobu, Kaneko, Masanori, Nakagawa, Yuichiroh, Ogawa, Hideto, Hoang, Thai Son and Butler, Michael (2018) DeepSaucer: Unified environment for verifying Deep Neural Networks. arXiv.

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, 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, 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).

Butler, Michael, Hoang, Thai Son, Raschke, Alexander and Reichl, Klaus (2020) Introduction to special section on the ABZ 2018 case study: Hybrid ERTMS/ETCS Level 3. International Journal on Software Tools for Technology Transfer, 22 (3), 249-255. (doi:10.1007/s10009-020-00562-3).

Fischer, Tomas, Reichl, Klaus, Tummeltshammer, Peter, Hoang, Thai Son and Butler, Michael (2020) Validation of railway control systems. In, Leitner, A., Watzenig, D. and Ibanez-Guzman, J. (eds.) Validation and Verification of Automated Systems. (HASH(0xd25dda8)) Cham. Springer International Publishing, pp. 221-229. (doi:10.1007/978-3-030-14628-3_17).

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, Voisin, Laurent and Butler, Michael (2020) Domain-specific developments using Rodin theories. In, Ait-Ameur, Yamine, Nakajima, Shin and Méry, Dominique (eds.) Implicit and Explicit Semantics Integration in Proof Based Developments of Discrete Systems: Communications of NII Shonan Meetings. Springer Nature.

Morris, Karla, Snook, Colin, Hoang, Thai Son, Hulette, G., Armstrong, Robert and Butler, Michael (2020) Formal verification of run-to-completion style statecharts using Event-B. Muccini, Henry, Avgeriou, Paris, Buhnova, Barbora, Camara, Javier, Caporuscio, Mauro, Franzago, Mirco, Koziolek, Anne, Scandurra, Patrizia, Trubiani, Catia, Weyns, Danny and Zdun, Uwe (eds.) In Software Architecture. ECSA 2020.: Communications in Computer and Information Science. vol. 1269, Springer, Cham. pp. 311-325 . (doi:10.1007/978-3-030-59155-7_24).

Snook, Colin, Hoang, Thai Son and Morris, Karla (2020) Dataset for "Formal verification of run-to-completion style statecharts using Event-B". University of Southampton doi:10.5258/SOTON/D1475 [Dataset]

Sritharan, Sanjeevan and Hoang, Thai Son (2020) Towards generating SPARK from Event-B models. In Proceedings of the 16th International Conference on integrated Formal Methods. 18 pp .

Turnock, Stephen, Hoang, Thai Son, Ossont, Steven J, Downes, Jon, Lam, Joseph and Pritchard, Ben (2020) Challenges of mission planning for collaborative maritime autonomy. In Autonomous Ships: 17th-18th June 2020, London, UK. Royal Institution of Naval Architects..

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]

Sritharan, Sanjeevan and Hoang, Thai Son (2021) Dataset for "Towards Generating SPARK from Event-B Models". University of Southampton doi:10.5258/SOTON/D1554 [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)

Zhu, Chenyang, Butler, Michael, Cirstea, Corina and Hoang, Thai Son (2021) Reasoning About Real-Time Systems in Event-B Models with Fairness Assumptions. In Proceedings of TASE2021 Conference. (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 .

Salehi Fathabadi, Asieh, Aï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.

Contact

Telephone: +44 (0) 23 8059 7084

Email: T.S.Hoang@soton.ac.uk

Share this profile Facebook Twitter Weibo