Dr Colin Snook PhD

Dr Colin Snook is a Senior Research Fellow in the cyber-physical systems group at the University of Southampton, UK. He was involved in the development of the Rodin modelling tools, especially UML-B which is a UML-like diagrammatic front-end for the Event-B formal modelling language. He has spent the past 20 years collaborating with industry in the Aerospace and Railway domains to facilitate industrial use of formal methods. This has included consultancy on modelling and verification of systems as well as developing formal modelling tools and training various industrial partners in their use. Before gaining his PhD in computer science at Southampton in 2001 he worked as a software engineer on safety-critical aircraft engine controls.

Research

Research interests

Useable Formal modelling methods and promoting their use in industry.

Publications

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

Satpathy, Manoranjan, Harrison, Rachel, Snook, Colin and Butler, Michael (2001) A Generic Model for Assessing Process Quality. Dumke, None and Abran, None (eds.) 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. 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. 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. 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), 275-283.

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

Snook, Colin, Butler, Michael and Oliver, Ian (2004) The UML-B Profile for formal systems modelling in UML. In, Mermet, J. (ed.) 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), 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.) 3rd International Workshop on Critical Systems Development with UML, Lisbon. pp. 115-129 .

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

Snook, Colin and Butler, Michael (2004) U2B - A tool for translating UML-B models into B. In, Mermet, J. (ed.) 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.) Workshop on Rigorous Engineering of Fault Tolerant Systems, Newcastle, 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.) Eleventh International Workshop on Requirements Engineering: Foundation for Software Quality, Oporto. 12 - 13 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.) 11th International Conference on Evaluation and Assessment in Software Engineering (EASE'07), Keele, Staffordshire, United Kingdom. 01 - 02 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. The IASTED International Conference on Software Engineering - SE2008, Innsbruck, 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. 1st ACM International Workshop on Empirical Assessment of Software Engineering Languages and Technologies (WEASELTech) 2007, Atlanta, US, 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. (In Press)

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), 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. 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". McGPLE: Workshop on Modularization, Composition, and Generative Techniques for Product Line Engineering, Nashville, TN. pp. 1-6 .

Said, Mar Yah, Butler, Michael and Snook, Colin (2009) Class and state machine refinement in UML-B. Integration of Model-based Formal Methods and Tools (workshop at iFM 2009).

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

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

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. pp. 579-595 . (doi:10.1007/978-3-642-05089-3_37).

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

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

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

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

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

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

Said, Mar Yah (2012) ATM Case study models - UML-B/Event-B. University of Southampton [Dataset]

Satpathy, Manoranjan, Snook, Colin, Arora, Silky, Ramesh, S and Butler, Michael (2013) Systematic Development of Control Designs via Formal Refinement. 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. 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. 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. 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), 1557–1580. (doi:10.1007/s10270-013-0391-z).

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.

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

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

Edmunds, Andrew, Snook, Colin and Walden, Marina (2016) On component-based reuse for Event-B. Butler, M, Schewe, K-D, Mashkoor, A and Biro, M (eds.) In Abstract State Machines, Alloy, B, TLA, VDM, and Z: 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings. Springer. pp. 151-168 . (doi:10.1007/978-3-319-33600-8_9).

Snook, Colin and Kazmierski, Tomasz (2016) Using Event-B and Modelica to evaluate thermal management strategies in many core systems. In, 2016 Forum on Specification and Design Languages (FDL). Forum on specification & Design Languages (FDL 2016) (13/09/16 - 15/09/16) IEEE. (doi:10.1109/FDL.2016.7880380).

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. Ogata, K, Lawford, M and Liu, S (eds.) In Formal Methods and Software Engineering: ICFEM 2016. vol. 10009, Springer. pp. 210-225 . (doi:10.1007/978-3-319-47846-3_14).

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 .

Snook, Colin, Hoang, Thai Son 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. Rodin Developer Workshop 2016, Linz, Austria.

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]

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]

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

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

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

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.

Schlick, Rupert, Felderer, Michael, Majzik, Istvan, Nardone, Roberto, Raschke, Alexander, Snook, Colin and Vittorini, Valeria (2018) A proposal of an example and experiments repository to foster industrial adoption of formal methods. In Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice - 8th International Symposium, ISoLA 2018, Proceedings. vol. 11247 LNCS, Springer Verlag. pp. 249-272 . (doi:10.1007/978-3-030-03427-6_20).

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

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]

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

Morris, K., Snook, Colin, Hoang, T.S., Hulette, G., Armstrong, R. and Butler, M. (2020) Refinement and verification of responsive control systems. Raschke, Alexander, Méry, Dominique and Houdek, Frank (eds.) In Rigorous State-Based Methods: 7th International Conference, ABZ 2020, Ulm, Germany, May 27–29, 2020, Proceedings. vol. 12071, Springer. 6 pp . (In Press)

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

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]

Abbas, Messaoud, Rioboo, Renaud, Ben-Yelles, Choukri-Bey and Snook, Colin (2020) Formal modeling and verification of UML Activity Diagrams (UAD) with FoCaLiZe. Journal of Systems Architecture, [101911]. (doi:10.1016/j.sysarc.2020.101911).

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, 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 9052

Email: cfs@soton.ac.uk

Share this profile Facebook Twitter Weibo