Anthony J H Simons, MA PhD

Senior Lecturer in Computer Science

You are here: Simons Home / Research / Projects /
Department of Computer Science
Verification and Testing Research Group

Research Projects

Here is a summary of my major research projects, past and present. All apart from the most recent have received exernal funding. The sponsors, dates and amounts funded is given. Many projects have their own websites: click on the associated icon to visit.

Broker@Cloud:  Enabling continuous quality assurance and optimization 
    in future enterprise cloud service brokers

Broker@Cloud: EU FP7 (ICT-318392)

Project Title: Broker@Cloud: Enabling continuous quality assurance and optimization in future enterprise cloud service brokers. Sponsor: EU FP7 Period: 1 November 2012 - 31 October 2015 Value: €404,000 Investigators: Anthony Simons (PI), Mariam Kiran (RA) Partners: SINTEF Oslo (co-ordinator), SEERC Thessaloniki, CAS Software AG, SingularLogic, ICCS Athens, SAP Research.

Summary: This project aims to develop enabling technology to support future Cloud service brokers. A broker will link up service consumers with service providers, offering added value through mediation and quality control. Sheffield's role in this is to provide portable specifications and a testing methodlogy for certifying the behaviour of software services. Other partners will be investigating service monitoring and optimization, and failure prevention and recovery. The results will form part of a future European Open Standard that Cloud service providers and brokers may sign up to, in order to promote an open ecosystem of Cloud services.

ReMoDeL: Reusable Model Design Language

ReMoDeL: (Seeking funding)

Project Title: ReMoDeL: Reusable Model Design Language. Sponsor: seeking sponsorship Period: 1 January 2008 - current; Value: Nothing yet! Investigators: Anthony Simons (PI) Partners: Seeking partners.

Summary: This project brings together a number of different challenges in software engineering. Program-It-Yourself: PIY is the idea that, in future, business end-users should be able to specify the kinds of systems that they need, using domain-specific languages tailored to express their requirements directly. Scrap-Heap Challenge: SHC is the idea that, in future, software will be cannibalised from existing systems, but not at the code-level, rather at the model-level, from which new systems will be automatically generated. Self-Verification and Test: SVT is the idea that, in future, design models will be automatically checked for consistency and completeness and generated code will be automatically tested against specifications. This is an exciting new field!

JWalk: Lazy Systematic Unit Testing

JWalk: (Seeking funding)

Project Title: JWalk: Lazy Systematic Unit Testing by Introspection and Interaction. Sponsor: seeking sponsorship Period: 1 May 2006 - current; Value: Nothing yet! Investigators: Anthony Simons (PI), Chris Thomson (CI) Partners: Seeking partners.

Summary: The aim of this project is to provide the power of systematic specification-based testing for programmers who are too lazy to write specifications. JWalk is a toolset that performs bounded exhaustive unit tests on compiled Java classes. The tools discover the intended specification by a combination of run-time introspection, using the Java reflection API, and interaction with the programmer. JWalk can perform bounded exhaustive exploration of the test class's method protocols, algebraic structure and intended design state space. By a mixture of interaction and rule-based inference, the tool also builds up an incremental specification. Testing is progressively automated, up to the equivalent of full algebraic or state-space testing.

Z2SAL: A Translation-Based Model-Checker for Z

Z2SAL: (Seeking funding)

Project Title: Z2SAL: A Translation-Based Model-Checker for Z. Sponsor: seeking sponsorship Period: 1 October 2007 - current; Value: Nothing yet! Investigators: John Derrick (PI), Siobháhn North, Anthony Simons Partners: CZT: Community Z Tools.

Summary: This project aims to build a model-checker for the Z notation, by translating from Z into the input language for the Symbolic Analysis Laboratory (SAL) toolkit (from SRI, Stanford). The ultimate goal is to provide proofs of correct refinement from abstract to concrete Z formal specifications. Being able to automate proofs in Z brings added value to this formal specification language. Partners in this work include the Community Z Tools (CZT) community, who already share a number of Z tools. Eventually, this project will interface with the CZT abstract syntax tools for manipulating Z. To date, we have built a bespoke parser for the LaTeX encoding of Z, and can translate large parts of the Z mathematical toolkit into SAL. Model-checking validates LTL properties and, in the future will also validate CTL properties.

RefineMDA: Higher-order Refinement Techniques for Model Driven
    Architecture

Refine-MDA: EPSRC EP/G031711/1 and EP/GR03012X/1

Project Title: Higher-order Refinement Techniques for Model Driven Architecture. Sponsor: EPSRC Period: 13 July 2009 - current; Value: £324,340 (Sheffield), £315,590 (KCL) Investigators: John Derrick (PI), Anthony Simons (CI), Georg Struth (CI), Simon Thomson (RA) Partners:Iman Poernomo (PI), Kevin Lano (CI) at Kings College, London; ARTiSAN Tools; IBM UK Labs Ltd.

Summary: This twin-site project aims to provide the OMG's call for Model Driven Architecture with a proper formal underpinning. The main insight behind the project is that OMG's Meta-Object Facility (MOF) can be described in higher-order Constructive Type Theory (CTT). By constructing models in CTT of software specifications in UML, we aim to construct proofs of correct transformation from abstract to concrete UML models, using existing theorem provers, such as Coq or Agda. By exploiting the Curry-Howard isomorphism, whereby proofs correspond to programs, we expect to be able to define the notion of a correct transformation, obtaining the transformer-program as a by-product of constructing the proof of correctness. This will provide the OMG's notion of Query Value Transformation (QVT) with a much-needed formal underpinning.

MOTIVE: Object-Oriented Testing

MOTIVE: EPSRC GR/M56777

Project Title: MOTIVE: Method for Object Testing, Integration and Verification. Sponsor: Engineering and Physical Sciences Research Council: Information Technology and Computer Science Programme; Period: 1 October 1999 - 31 December 2002; Value: £221,238. Investigators: Anthony Simons (PI), Mike Holcombe (CI), Kirill Bogdanov (RA), Mike Stannett (RA); Partners: ObjecTime Ltd (later absorbed into Rational Inc. and IBM UK), Information Processing Ltd, Sun Microsystems UK.

Summary: This project set out to adapt the proven X-Machine testing method, developed here in Sheffield, for object-oriented software. A revised formal model, the Object X-Machine, was developed, together with a theory of behavioural refinement under inheritance. The X-Machine test generation method was adapted for unit testing object-oriented classes, and the tests generated by this method were compared against conventional regression testing methods. Conventional re-testing was found to admit hidden faults, whereas Motive-style testing produced repeatable guarantees of correctness for modified and extended classes.

The Discovery Method

The Discovery Method: AITO/ACM

Project Title: The Discovery Method for Developing Object-Oriented Systems. Sponsor: Association Internationale pour la Technologie des Objets / Association of Computing Machinery; and University of Sheffield International Strategy Group Period: March 1993 - present; Value: £3,800 so far. Investigators: Anthony Simons (PI), Dita Sardjono (PhD), Tom Baldwin (MRes), Michal Smialek (MSc), Carlos Fernandez (PhD); Partners: Xactium, Precise UML Group, OPEN Consortium, Wirfs-Brock Associates.

Summary: This project set out to develop a complete systems analysis and design method for object-oriented systems. The method exploits psychological reinforcement techniques (the so-called discovery procedures) to focus the developer's attention on relevant aspects of the system at each stage of development. The method has many techniques for capturing and refining requirements and many transformations for converting information into high-quality object-oriented designs, whose modules have high internal cohesion and loose external coupling. A semantically clarified UML profile is used as the notation, which has an underlying formal semantics. The Discovery Method has evolved through versions 1.0 and 2.0; a number of tutorials have been presented at the ECOOP and SPA (formerly OOPS) conferences. A major book is in preparation.

Fortest: Formal Methods and Testing Network

FORTEST: EPSRC GR/R43150/01

Project Title: FORTEST: Formal Methods and Testing Network. Sponsor: Engineering and Physical Sciences Research Council; Period: 1 November 2001 - 30 April 2005; Value: £63,158. Investigators: Robert Hierons (Brunel - PI), Mark Harman (Kings, London - CI), Jonathan Bowen (South Bank, London - CI) Mike Holcombe (CI), Anthony Simons (CI), Kirill Bogdanov (CI), Anthony Cowling (CI), Marian Gheorghe (CI) and others; Partners: DaimlerChrysler, Motorola, IBM , Philips, Praxis High-Integrity Systems, Teleogic, and DERA.

Summary: The aim of FORTEST was to establish a network on Formal Methods and Testing. This was successful and the network has continued as a subject group of two of the BCS Special Interest groups: FACS (Formal Aspects of Computing Science) and SIGIST (Special Interest Group in Software Testing). Network members investigated the relationship between formal and semi-formal methods and software testing; and sought to find ways to integrate static testing (viz verification, model checking of specifications) and dynamic testing (of software systems). A landscapes paper surveying the state of the art was produced by members of the network and will be published in ACM Computing Surveys.

The Poppy Object-Oriented Language

Poppy: (Seeking funding)

Project Title: Poppy: The Poppy Object-Oriented Language Sponsor: seeking sponsorship Period: 1 Jan 2003 - current; Value: Nothing yet! Investigators: Anthony Simons (PI), Chris Dabnor (student) Partners: Seeking partners.

Summary: The idea for this project grew out of my PhD thesis: A Language with Class: The Theory of Classification Exemplified in an Object-Oriented Language, University of Sheffield, 1996. It aims to design and implement a novel object-oriented programming language, whose treatment of class follows the theory of function-bounded polymorphism in the second-order (and higher-order) λ-calculus. However, the concrete syntax of Poppy will avoid the use of nested type parameters and will instead support systematic type substitution as a way of describing the evolution of closed recursive types under inheritance, and the specialisation of field-types that would normally be handled by parametric instantiation. One of the main challenges is to develop an incremental compiler, that is capable of making late binding optimisations.

The Theory of Classification

The Theory of Classification: AITO/ACM

Project Title: The Theory of Classification. Sponsor: Association Internationale pour la Technologie des Objets / Association of Computing Machinery Period: January 1991 - September 1995; January 2002 - September 2005 Value: £2,500 in travel grants. Investigators: Anthony Simons (PI); Partners: Kim Bruce (Williams College, MA), Richard Wiener and Bertrand Meyer (ETH Zurich), for the Journal of Object Technology (JOT).

Summary: This project grew out of my PhD thesis: A Language with Class: The Theory of Classification Exemplified in an Object-Oriented Language, University of Sheffield, 1996. It developed a mathematical theory of the notion of class in object-oriented programming languages, which formerly had been considered merely an implementation construct. The theory demonstrates that a class is not a type, but a second-order construction in the F-bounded λ-calculus. The theory distinguises simple subtyping from the second-order and higher-order inclusion that characterises inheritance relationships. The theory harmonises object-oriented notions of inhteritance-based polymorphism with traditional parametric notions of polymorphic types. A monograph in 20 parts was published in the Journal of Object Technology; and this popular series is frequently cited in courses on object-oriented theory.

The Simons Component Library

The Simons Component Library: RS/RAE

Project Title: The Simons Component Library Sponsor: The Royal Society / The Royal Academy of Engineers Period: October 1997 - December 1998; September 2005 - May 2006. Value: £1,000 in travel grants. Investigators: Anthony Simons (PI); Partners: Members of the OOPSLA Workshop on Library-Centric Software Design.

Summary: The Simons Component Library is a repository of general-purpose software components created in the C++ programming language. The aim is to offer a compact collection of components that work together, using common interfaces for similar components, in order to facilitate ease of understanding and usage. A uniformly object-oriented design philosophy is followed throughout; and programming idioms bear some similarity with Java. The SCL is designed with a greater emphasis on dynamic compatibility than the C++ Standard Template Library, to increase support for component serialisation, migration and run-time substitution. In many ways, the SCL takes precisely the opposite design decisions from the STL and serves as an interesting experiment in genuine dynamic code reuse (rather than code replication), minimal interfaces and shared algorithms.

SYLK: Syllable-Based Descriptions of Acoustic-Phonetic Events

SYLK: SERC/IED/IEATP GR/F36507

Project Title: SYLK: Syllable-Based Descriptions of Acoustic-Phonetic Events. Sponsor: Science and Engineering Research Council / Information Engineering Directorate: Information Engineering Advanced Technology Programme; Period: 1 October 1989 - 31 March 1993; Value: £255,000. Investigators: Phil Green (PI), Peter Roach (Leeds - CI), Anthony Simons (CI), Martin Cooke (CI), Nick Kew (RA), Luke Boucher (RA). Partners: John Holmes Consulting, UK Government Speech Research Unit.

Summary: This project developed a syllable-conditioned model of acoustic-phonetic segments for automatic speech recognition, capturing the differences in the way speech sounds are realised in the onset and coda portion of the syllable. This was more realistic than earlier segmental approaches. A mathematically sound scheme was developed to combine the results of different kinds of speech recognisers, such as knowlege-based recognisers, neural networks and hidden Markov models.

Speech Sketch: A Speech Recognition Strategy based on Making
    Acoustic Evidence and Phonetic Knowledge Explicit

Speech Sketch: SERC/Alvey

Project Title: Speech Sketch: A Speech Recognition Strategy based on Making Acoustic Evidence and Phonetic Knowledge Explicit. Sponsor: Science and Engineering Research Council / Alvey Programme; Period: 1 January 1986 - 31 March 1989; Value: £200,000. Investigators: Phil Green (PI), Anthony Simons (RA), Martin Cooke (RA). Partners: Centre for Speech Technology Research, Plessey, Marconi.

Summary: This project developed a representational approach to automatic speech recognition (ASR), analogous to David Marr's approach in computer vision, that raised the level of description of acoustic-phonetic events before applying recognition algorithms. The resulting Speech Sketch was a multi-scale cartoon of the acoustic spectrum, in which phonetic constraints could be applied to identify phonetic segments in a qualitative way. This improved on earlier segmental and threshold-based approaches that were non-robust and speaker-dependent. For difficult semivowel segments, the recogniser outperformed other UK approaches and achieved similar performance to the best MIT speech recogniser.

Regent Court, 211 Portobello Street, Sheffield S1 4DP, United Kingdom