last updated 07/05/04
I am a Research Fellow in the Declarative Systems and Software Engineering (DSSE) group of the ECS Department. (3rd floor lab of New Zeppler building). This position follows on from my PhD research, which I started in October 98 after about 20 years in industry. My research areas are integration of semi-formal and formal notations (particularly UML and B) and the empirical assessment of formal specifications.
UML-B is a graphical formal notation that borrows from UML and from B. UML-B is a profile of the UML that is precise and semantically well defined via an equivalence to B. UML-B consists of:
D a subset of the UML - including packages, class diagrams and state charts
D specialisations of these features via stereotypes and tagged values,
D structuring mechanisms (systems, components and modules) based on specialisations of UML packages
D UML-B clauses a set of textual tagged values to define extra modelling features for UML entities,
D uB an integrated action and constraint language based on B,
D Well-formedness rules
U2B is a translator that converts a UML-B model into its equivalent B specification.
We are keen for people to try UML-B and the U2B translation and give feedback. You can download the U2B translator, an example and a description here: U2B Downloads
This project will start June 2004.
During the Pussee project we developed UML-B and U2B to support UML based modelling of event B systems.
(2003) Towards a
UML profile for UML-B. Technical Report DSSE-TR-2003-3, Electronics and Computer Science,
UML-B and U2B for formal refinement of digital components.
In Proceedings of Forum on specification
& design languages ,
During the Matisse project we developed UML-B and U2B to support UML based modelling of B-action systems. B-action systems are a representation, using B, of the action systems formalism. This work was carried out with Marina Walden of Abo Akademi.
C. Snook and M.Walden: Use of U2B for specifying B action systems. In Proceedings of RCS02 International workshop on refinement of critical systems: methods, tools and experience, Grenoble, France, Jan 2002.
A description of the case study developed during and following the Matisse project is given in.
C. Snook, L.Tsiopoulos and M.Walden: A case study on control system development in UML and B. In Proceedings of RCS03 International workshop on refinement of critical systems: methods, tools and experience, Turku, Finland, 2003.
The first part of this work consisted of surveying practitioners opinions to gain an understanding of the issues that are of most concern to industry. (This work was conducted under the supervision of Rachel Harrison).
C. Snook and R.Harrison: Practitioners
Views on the Use of Formal Methods: An Industrial Survey by Structured
Information and Software Technology March 2001
(earlier version: Proceedings of EASE 2000: Papers from The Conference on Empirical Assessment In Software Engineering)
The survey indicated that comprehension of formal specifications is not a significant problem. I conducted an experiment to compare the comprehensibility of a Z specification with its implementation in Java. Since it is difficult to find valid measures for external attributes such as comprehensibility, this comparison is useful because pratitioners have a good feel for the attribute with respect to code. (Also conducted under the supervision of Rachel Harrison).
C. Snook and R.Harrison: Experimental
Comparison of the Comprehensibility of a Z Specification and its Implementation
Information and Software Technology to be published
(earlier version: Proceedings of EASE 2001: Papers from The Conference on Empirical Assessment In Software Engineering
The survey indicated that creation of good formal specifications is difficult. I am therefore interested in whether design exploration and visualisation tools such as are used for program design would be of similar benefit in creating formal specifications. More specifically I am investigating automated translations between UML class diagrams and B as a technique to aid in producing B specifications. (This work is being conducted under the supervision of Michael Butler)
(2000) Verifying Dynamic Properties of UML Models by Translation to the B Language and Toolkit. In Proceedings of UML 2000 Workshop, Dynamic Behaviour in UML Models: Semantic Questions .
(2001) Using UML Class Diagrams for Constructing B Specifications.
I also worked on the EPSRC
project called 'Empirical Assessment of Formal Methods (EMPAF) in collaboration
with Reading University and Philips Research laboratories culminating in our
M.Satpathy, C.Snook, R.Harrison, M.Butler: A Comparative Study of Formal and Informal Specifications through an Industrial Case Study
I also contributed to Manu's work on Quality Models and
appear as a co-author on the paper:
M.Satpathy, R.Harrison, C.Snook, M.Butler: A Generic Model for Assessing Process Quality.
In Proceedings of IWSM2000 - Dumke/Abran: New Approaches in Software Measurement, LNCS 2006, Springer Publ., 2001.
Prior to starting my PhD I worked as a software engineer on various embedded control and monitoring systems; most recently for Vosper Thorneycroft Controls Ltd on safety critical engine control systems. I also spent some years in quality assurance where I was responsible for obtaining ISO 9001 TickIt certification.