The University of Southampton

Dr Colin F Snook

Research Staff

Dr Colin Snook is a senior research fellow in the Electronic and Software Systems research group of the Electronics and Computer Science department at the University of Southampton. He is currently working on the EU FPR7 Advance project developing tools for formal modelling of cyberphysical systems and on the EPSRC Prime project modelling power and reliability management of many-core computers. Dr Snook is best known for the development of the UML-B modelling notation, facilitating the use of formal methods in industry and empirical assessment of formal modelling notations. Dr Snook gained his PhD at the University of Southampton in 2001. Before that he worked for Hawker Siddeley Dynamics Engineering (now AT Engine Controls Ltd.) developing real time embedded control systems in various application domains including avionic engine controls. He also spent several years as a software quality manager.


Research interests

I am interested in tools and techniques to make formal methods more approachable to industry. One way to do this is to integrate formal methods with the tools and methods that are more commonly used in industry. 

I am also interested in methods for developing extensible integrated modelling tools.




PhD Exploring the Barriers to Formal Specification, University of Southampton, 2001 

Professional activities

Ongoing work with AT Engine Controls Ltd.


ESS Lab Manager


Gondal, Ali, Poppleton, Michael and Snook, Colin (2009) Feature composition - towards product lines of event-B models At 1st International Workshop on Model-Driven Product Line Engineering. 24 Jun 2009.

Satpathy, Manoranjan, Harrison, Rachel, Snook, Colin and Butler, Michael, (2001) A Generic Model for Assessing Process Quality Dumke, None and Abran, None (eds.) At International Workshop on Software Measurement (IWSM2000).

Snook, Colin and Butler, Michael (2000) Verifying Dynamic Properties of UML Models by Translation to the B Language and Toolkit At UML 2000 Workshop, Dynamic Behaviour in UML Models: Semantic Questions.

Snook, C. and Butler, M. J. (2001) Using a Graphical Design Tool for Formal Specification At Proceedings 13th Annual Workshop of the Psychology of Programming Interest Group.

Satpathy, Manoranjan, Harrison, Rachel, Snook, Colin and Butler, Michael (2001) A Comparative Study of Formal and Informal Specifications through an Industrial Case Study At IEEE/ IFIP Workshop on Formal Specification of Computer Based Systems (FSCBS'01).

Snook, Colin and Harrison, Rachel (2001) Practitioners' views on the use of formal methods: an industrial survey by structured interview Information and Software Technology, 43, (4), pp. 275-283.

Snook, Colin and Sandstrom, Kim (2003) Using UML-B and U2B for formal refinement of digital components At Forum on specification & design languages. 23 - 26 Sep 2003.

Snook, Colin, Butler, Michael and Oliver, Ian (2004) The UML-B Profile for formal systems modelling in UML In, Mermet, J. (eds.) UML-B Specification for Proven Embedded Systems Design. Springer

Snook, Colin and Butler, Michael (2006) UML-B: Formal modelling and design aided by UML ACM Transactions on Software Engineering and Methodology, 15, (1), pp. 92-122.

Lo Presti, Stephane, Butler, Michael, Leuschel, Michael, Snook, Colin and Turner, Phillip (2004) Formal Modelling and Verification of Trust in a Pervasive Application s.n.

Snook, Colin, Butler, Michael, Edmunds, Andy and Johnson, Ian, (2004) Rigorous development of reusable, domain-specific components, for complex applications Jurgens, Jan and France, Robert (eds.) At 3rd International Workshop on Critical Systems Development with UML. , pp. 115-129.

Butler, Michael, Leuschel, Michael and Snook, Colin (2005) Tools for system validation with B abstract machines At ASM 2005: 12th International Workshop on Abstract State Machines.

Snook, Colin and Butler, Michael (2004) U2B - A tool for translating UML-B models into B In, Mermet, J. (eds.) UML-B Specification for Proven Embedded Systems Design. Springer

Snook, Colin, Poppleton, Michael and Johnson, Ian, (2005) Towards a methodology for rigorous development of generic requirements patterns Butler, M, Jones, C, Romanovsky, A and Troubitsyna, E (eds.) At Workshop on Rigorous Engineering of Fault Tolerant Systems, United Kingdom. , pp. 17-27.

Snook, Colin, Poppleton, Michael and Johnson, Ian, (2005) The engineering of generic requirements for failure management Kamsties, Erik, Gervasi, Vincenzo and Sawyer, Pete (eds.) At Eleventh International Workshop on Requirements Engineering: Foundation for Software Quality. 13 - 14 Jun 2005. , pp. 145-160.

Razali, R, Snook, C. F., Poppleton, M. R., Garratt, P. W. and Walters, R. J., (2007) Experimental Comparison of the Comprehensibility of a UML-based Formal Specification versus a Textual One Kitchenham, B, Brereton, P and Turner, M (eds.) At 11th International Conference on Evaluation and Assessment in Software Engineering (EASE'07), United Kingdom. 02 - 03 Apr 2007. , pp. 1-11.

Razali, R, Snook, C, Poppleton, M and Garratt, P (2007) Comprehensibility of UML-B - A Series of Controlled Experiments s.n.

Snook, Colin and Butler, Michael (2008) UML-B and Event-B: an integration of languages and tools At The IASTED International Conference on Software Engineering - SE2008, Austria. 12 - 14 Feb 2008.

Razali, R, Snook, C. F. and Poppleton, M. R. (2007) Comprehensibility of UML-based Formal Model – A Series of Controlled Experiments At 1st ACM International Workshop on Empirical Assessment of Software Engineering Languages and Technologies (WEASELTech) 2007, Georgia. , pp. 25-30.

Razali, Rozilawati, Snook, Colin, Poppleton, Michael and Garratt, Paul (2008) Usability Assessment of a UML-based Formal Modelling Method Using Cognitive Dimensions Framework Human Technology: An Interdisciplinary Journal on Humans in ICT Environments

Snook, Colin, Poppleton, Michael and Johnson, Ian (2008) Rigorous engineering of product-line requirements: a case study in failure management [in special issue: Section 1: Most-cited software engineering articles in 2001. Section 2: Requirement engineering: Foundation for software quality] Information and Software Technology, 50, (1-2), pp. 112-129. (doi:10.1016/j.infsof.2007.10.010).

Snook, Colin and Butler, Michael (2008) UML-B: A plug-in for the Event-B tool set At Abstract State Machines, B and Z, First International Conference ABZ 2008. , p. 347.

Poppleton, M., Fischer, B., Franklin, C., Gondal, A., Snook, C. and Sorge, J. (2008) Towards Reuse with "Feature-Oriented Event-B" At McGPLE: Workshop on Modularization, Composition, and Generative Techniques for Product Line Engineering. , pp. 1-6.

Said, Mar Yah, Butler, Michael and Snook, Colin (2009) Class and State Machine Re?nement in UML-B At Integration of Model-based Formal Methods and Tools (workshop at iFM 2009).

Gondal, Ali, Poppleton, Mike and Snook, Colin (2009) Feature composition - towards product lines of Event-B models At 1st International Workshop on Model-Driven Product Line Engineering (MDPLE'09), Netherlands.

Savicks, Vitaly, Snook, Colin and Butler, Michael (2009) Animation of UML-B State-machines s.n.

Said, Mar Yah, Butler, Michael and Snook, Colin, (2009) Language and tool support for class and state machine refinement in UML-B Cavalcanti, A. and Dams, D. (eds.) In FM 2009: Formal Methods. Springer. 17 pp, pp. 579-595. (doi:10.1007/978-3-642-05089-3_37).

Snook, Colin, Fritz, Fabian and Illisaov, Alexei (2010) An EMF Framework for Event-B At Workshop on Tool Building in Formal Methods - ABZ Conference, Canada.

Joochim, Tossaporn, Snook, Colin, Poppleton, Mike and Gravell, Andrew (2010) Timing diagrams requirements modeling using Event-B formal methods At IASTED International Conference on Software Engineering (SE2010), Austria. 16 - 18 Feb 2010.

Gondal, Ali, Poppleton, Mike, Butler, Michael and Snook, Colin (2010) Feature-Oriented Modelling Using Event-B At International Conference on Software Engineering Theory and Practice (SETP-10), United States. 12 - 14 Jul 2010.

Snook, Colin (2011) Modelling Control Process and Control Mode with Synchronising Orthogonal State Machines At B2011.

Snook, Colin, Savicks, Vitaly and Butler, Michael (2011) Verification of UML models by translation to UML-B Lecture Notes in Computer Science, 6957, p. 251.

Hallerstede, Stefan and Snook, Colin (2011) Refining Nodes and Edges of State Machines At ICFEM 2011: 13th International Conference on Formal Engineering Methods, United Kingdom. 26 - 28 Oct 2011.

Snook, Colin, Satpathy, Manoranjan and Arora, Silky (2012) Power window case study models - UML-B/Event-B/Simulink University of Southampton [Dataset]

Satpathy, Manoranjan, Snook, Colin, Arora, Silky, Ramesh, S and Butler, Michael (2013) Systematic Development of Control Designs via Formal Refinement At International Conference on Model-Driven Engineering and Software Development.

Butler, Michael, Colley, John, Edmunds, Andrew, Snook, Colin, Evans, Neil, Grant, Neil and Marshall, Helen (2013) Modelling and Refinement in CODA At Refine. , pp. 36-51.

Satpathy, M., Ramesh, S., Snook, Colin, Singh, N.K. and Butler, Michael (2013) A Mixed Approach to Rigorous Development of Control Designs At IEEE Multi-Conference on Systems and Control (MSC 2013).

Bicknell, Brett, Reis, Jose, Butler, Michael, Colley, John and Snook, Colin (2012) A Practical Approach for Closed Systems Formal Verification Using Event-B At 10th International Conference on Software Engineering and Formal Methods (SEFM 2012). , pp. 323-332.

Said, Mar Yah, Butler, Michael and Snook, Colin (2015) A Method of Refinement in UML-B Software and Systems Modeling, 14, (4)

Salehi Fathabadi, Asieh, Snook, Colin and Butler, Michael (2014) Applying an integrated modelling process to run-time management of many-core systems At 11th International Conference on Integrated Formal Methods (iFM), Italy. 09 - 11 Sep 2014.

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

Edmunds, Andrew, Olszewska, Marta and Walden, Marina (2016) Using the Event-B formal method for disciplined agile delivery of safety-critical systems At The Second International Conference on Advances and Trends in Software Engineering: SOFTENG 2016, Portugal. 21 - 25 Feb 2016. 9 pp.

Edmunds, Andrew, Snook, Colin and Walden, Marina (2016) On component-based reuse for Event-B At ABZ 2016: 5th International ABZ Conference ASM, Alloy, B, TLA, VDM, Z, Austria. 23 - 27 May 2016. 14 pp.

Snook, Colin and Kazmierski, Tomasz (2016) Using Event-B and Modelica to evaluate thermal management strategies in many core systems At Forum on specification & Design Languages (FDL 2016), Germany. 14 - 16 Sep 2016. 5 pp.

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]

Al-Brashdi, Ahmed, Butler, Michael, Rezazadeh, Abdolbaghi and Snook, Colin (2016) Tool support for model-based database design with Event-B At Workshop on Formal and Model-Driven Techniques for Developing Trustworthy Systemsc at ICFEM 2016, Japan. 14 - 16 Nov 2016. 7 pp.

Salehi Fathabadi, Asieh, Butler, Michael and Snook, Colin (2016) Extending Code Generation to Support Platform-Independent Event-B Models At Rodin Developer Workshop, 2016. , p. 21.

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

Dghaym, Dana, Salehi Fathabadi, Asieh and Snook, Colin (2016) Using Rodin and BMotionStudio for public engagement At Rodin Developer Workshop 2016, Austria.

Snook, Colin, Hoang, Thai Son and Butler, Michael (2017) Analysing security protocols using refinement in iUML-B At 9th NASA Formal Methods Symposium, Moffett Field, CA, United States. 16 - 18 May 2017. 15 pp, pp. 84-98.

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. 18 pp. (Submitted). (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 At International Conference on Reliability, Safety and Security of Railway Systems: Modelling, Analysis, Verification and Certification, Pistoia, Italy. 14 - 16 Nov 2017. (Submitted).

Hoang, Thai, Snook, Colin, Dghaym, Dana and Butler, Michael (2017) RailGround using Theory plug-in University of Southampton [Dataset]

Snook, Colin, Dghaym, Dana, Hoang, Thai, 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]

Hoang, Thai Son, Dghaym, Dana, Snook, Colin and Butler, Michael (2017) A composition mechanism for refinement-based methods At 22nd International Conference on Engineering of Complex Computer Systems, Fukuoka, Japan. 05 - 08 Nov 2017. 10 pp.

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]


Telephone: +442380599052


Fax: +44 23 8059 4506

Share this profile FacebookGoogle+TwitterWeibo

We use cookies to ensure that we give you the best experience on our website. If you continue without changing your settings, we will assume that you are happy to receive cookies on the University of Southampton website.