Phone: 023 80593123 (w)

email: cfs(at)ecs.soton.ac.uk

 
Colin F. Snook

                                                                    

Go To U2B Downloads                                                                                      Other Downloads

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

Projects:

Rodin

This project will start June 2004.

Pussee

http://www.keesda.com/pussee/

During the Pussee project we developed UML-B and U2B to support UML based modelling of event B systems.

Snook, C., Butler, M. and Oliver, I. (2003) Towards a UML profile for UML-B. Technical Report DSSE-TR-2003-3, Electronics and Computer Science, University of Southampton.

Snook, C. and Sandstrom, K. (2003) Using UML-B and U2B for formal refinement of digital components. In Proceedings of Forum on specification & design languages , Frankfurt.

Matisse

http://www.matisse.qinetiq.com/

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 RCS’02 – 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 RCS’03 – International workshop on refinement of critical systems: methods, tools and experience, Turku, Finland, 2003.

PhD:

Survey

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 Interview.
Information and Software Technology March 2001
(earlier version: Proceedings of EASE 2000: Papers from The Conference on Empirical Assessment In Software Engineering)
Abstract: html

Experiment

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 in Java.
Information and Software Technology – to be published
(earlier version: Proceedings of EASE 2001: Papers from The Conference on Empirical Assessment In Software Engineering
Abstract: html

U2B:   UML to B

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)

C.Snook and M.Butler: Using a Graphical Design Tool for Formal Specification. Proceedings of the 13th Annual Workshop of the Psychology of Programming Interest Group (PPIG)
Abstract: html

Butler, M. and Snook, C. (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 .

Snook, C. and Butler, M. J. (2001) Using UML Class Diagrams for Constructing B Specifications.

Other Work

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 paper:
M.Satpathy, C.Snook, R.Harrison, M.Butler: A Comparative Study of Formal and Informal Specifications through an Industrial Case Study
Abstract: html

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.
Abstract: html

Background

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.