Staff Profiles

Modules taught

• Advanced Software Engineering: how can we make sure that software is built correctly? In this module, you will learn a language called B for specifying exactly what software should do, built on the concepts of sets, relations, functions and logic. You will then learn a technique for deriving correct programs based solely on a specification in logic. 
• Secure Programming: you will learn about the fiendish tricks that hackers use to hijack software and gain control of computer systems and then make sure that all the software you work on is free from vulnerabilites. This is an exciting fast evolving field in which there are revelations about new exploits every month. You will learn about many subtleties within C/C++ and the security aspects of, for example, web programming, cryptography, networks, and operating systems including concurrency and access control. 
• Paradigms of Programming: you will end up writing five programs in five different languages. This is the module where you get to analyse and make up your own mind (with reasons!) about the programming languages you will be using in your everyday working life. You will also learn about the functional and logic paradigms, both of which will almost certainly have a profound effect on the way you think about programming. 

Research group membership

• Applied Formal Methods group

Research projects

• software design patterns are widely used in industry to pass on expertise about object-orientation, but can we recognise design patterns in legacy systems and when we compose them together to make larger systems, can we be sure that we have done it correctly?
• can we apply the concepts of design patterns to other areas such as security design patterns, which are the practices passed on by security experts to keep computer systems secure? 
• microservices are a lightweight container technology commonly used to provide SaaS (software-as-a-service). It seems plausible that agent-orientation, in which we supply behavioural rules to react to changes in the environment, may be a better fit to microservices than object-orientation. Inspired by this, we have devised a programming language for programming microservices. 
• algebraic specification of web services enables us to do automated testing using equations instantiated with random inputs instead of having to supply (input, output) pairs as usually required. However, since the testing is done shortly before use by a client that doesn't even own the service, it is not possible to "reset" the service to a prior state as sometimes is needed when testing such equations. How do we solve this problem and still successfully test web services?

Journal articles

• Zhu H, Bayley I , 'Discovering Boundary Values of Feature-based Machine Learning Classifiers through Exploratory Datamorphic Testing'
  Journal of Systems and Software 187 (2022)
  ISSN: 0164-1212
  Abstract

  Testing has been widely recognised as difficult for AI applications. This paper proposes a set of testing strategies for testing machine learning applications in the framework of the data- morphism testing methodology. In these strategies, testing aims at exploring the data space of a classification or clustering application to discover the boundaries between classes that the machine learning application defines. This enables the tester to understand precisely the be- haviour and function of the software under test. In the paper, three variants of exploratory strategies are presented with the algorithms implemented in the automated datamorphic test- ing tool Morphy. The correctness of these algorithms are formally proved. Their capability and cost of discovering borders between classes are evaluated via a set of controlled experiments with manually designed subjects and a set of case studies with real machine learning models.

  Website 
• Zhu H, Bayley I, 'Discovering and Investigating Cyberpatterns: The Road Map to Link Data Analytics with Reusable Knowledge'
  IEEE Systems, Man, and Cybernetics Magazine 4 (3) (2018) pp.14-22
  ISSN: 2380-1298 eISSN: 2333-942X
  Abstract One of the most compelling challenges for data analytics is to obtain reusable, verifiable and transferable knowledge from data. One solution to this is the pattern-oriented approach to knowledge representation proposed by this paper. The foundation of the approach is a formal theory of patterns, including a formal language for defining them, and an algebra of operations for composing patterns and instantiating them. This paper outlines a roadmap for the study of so-called cyberpatterns: the patterns of cyberspace. It explores the scope of research, views the current state of the art and identifies the key research questions.Website 
• Brown D, Aldea A, Harrison R, Martin C, Bayley I, 'Temporal case-based reasoning for type 1 diabetes mellitus bolus insulin decision support'
  Artificial Intelligence in Medicine 85 (April 2018) (2018) pp.28-42
  ISSN: 0933-3657 eISSN: 1873-2860
  Abstract Individuals with type 1 diabetes have to monitor their blood glucose levels, determine the quantity of insulin required to achieve optimal glycaemic control and administer it themselves subcutaneously, multiple times per day. To help with this process bolus calculators have been developed that suggest the appropriate dose. However these calculators do not automatically adapt to the specific circumstances of an individual and require fine-tuning of parameters, a process that often requires the input of an expert.
  To overcome the limitations of the traditional methods this paper proposes the use of an artificial intelligence technique, case-based reasoning, to personalise the bolus calculation. A novel aspect of our approach is the use of temporal sequences to take into account preceding events when recommending the bolus insulin doses rather than looking at events in isolation.
  The in silico results described in this paper show that given the initial conditions of the patient, the temporal retrieval algorithm identifies the most suitable case for reuse. Additionally through insulin-on-board adaptation and postprandial revision, the approach is able to learn and improve bolus predictions, reducing the blood glucose risk index by up to 27% after three revisions of a bolus solution.Website 
• Zhu H, Liu D, Bayley I, Aldea A, Yang Y, Chen Y, 'Quality Model and Metrics of Ontology for Semantic Descriptions of Web Services'
  Tsinghua Science and Technology 22 (3) (2017) pp.254-272
  ISSN: 1007-0214
  Abstract An ontology is a conceptualisation of domain knowledge. It is employed in semantic web services technologies to describe the meanings of services so that they can be dynamically searched for and composed according to their meanings. It is essential for dynamic service discovery, composition and invocation. Whether an ontology is well constructed has a tremendous impact on the accuracy of the semantic description of a web service, the complexity of the semantic definitions, the efficiency of processing messages passed between services, and the precision and recall rates of service retrieval from service registrations. However, measuring the quality of an ontology remains an open problem. Work on the evaluation of ontologies do exist, but they are not in the context of semantic web services. This paper addresses this problem by proposing a quality model of ontology and defining a set of metrics that enables the quality of an ontology to be measured objectively and quantitatively in the context of semantic descriptions of web services. These metrics cover the contents, presentation and usage aspects of ontologies. The paper also presents a tool that implements these metrics and reports a case study on five real-life examples of web services.Website 
• Zhu H, Bayley I, 'On the Composability of Design Patterns'
  IEEE Transactions on Software Engineering 41 (11) (2015) pp.1138-1152
  ISSN: 0098-5589
  Abstract
  In real applications, design patterns are almost always to be found composed with each other. It is crucial that these compositions be validated. This paper examines the notion of validity, and develops a formal method for proving or disproving it, in a context where composition is performed with formally defined operators on formally specified patterns. In particular, for validity, we require that pattern compositions preserve the features, semantics and soundness of the composed patterns. The application of the theory is demonstrated by a formal analysis of overlap-based pattern compositions and a case study of a real pattern-oriented software design. 
   
  Website 
• Liu D, Zhu H, Bayley I, 'Transformation of Algebraic Specifications into Ontological Semantic Descriptions of Web Services'
  International Journal of Services Computing 2 (1) (2014) pp.58-71
  ISSN: 2330-4464 eISSN: 2330-4472
  Abstract

  The accurate description of service semantics  plays a crucial role in service discovery, composition and  interaction. Most  work in this area has been focused on ontological descriptions, which are searchable and machineunderstandable.

  However, they do not define service functionality in a verifiable and testable manner In contrast, formal specification techniques, having evolved over the past 30 years, can define semantics in such a manner, but they have not yet been widely applied to service computing because the specifications produced are not searchable. There is a huge gap between these two methods of semantics description. This paper bridges the gap by advancing a transformation technique. It specifies services formally in an algebraic specification language, and then, extracts an ontological description of domain knowledge and service semantics as profiles in an ontology description language such as OWL-S. This brings the desired  searchability benefits. The paper presents a prototype tool for performing this transformation and reports a case study  to demonstrate the feasibility of our approach.        

• Zhu H, Bayley I, 'An algebra of design patterns'
  ACM Transactions on Software Engineering and Methodology 22 (3) (2013)
  ISSN: 1049-331X
  Abstract

  In a pattern-oriented software design process, design decisions are made by selecting and instantiating appropriate patterns, and composing them together. In our previous work, we enabled these decisions to be formalized by defining a set of operators on patterns with which instantiations and compositions can be represented. In this article, we investigate the algebraic properties of these operators. We provide and prove a complete set of algebraic laws so that equivalence between pattern expressions can be proven. Furthermore, we define an always-terminating normalization of pattern expression to a canonical form which is unique modulo equivalence in first-order logic.

   

  By a case study, the pattern-oriented design of an extensible request-handling framework, we demonstrate two practical applications of the algebraic framework. First, we can prove the correctness of a finished design with respect to the design decisions made and the formal specification of the patterns. Second, we can even derive the design from these components.

  Website 
• Bayley I, Zhu H, 'A formal language for the expression of pattern compositions'
  International Journal on Advances in Software 4 (3&4) (2011) pp.354-366
  ISSN: 1942-2628
  Website 
• Bayley I, Zhu H, 'Formal specification of the variants and behavioural features of design patterns'
  Journal of Systems and Software 83 (2) (2010) pp.209-221
  ISSN: 0164-1212
  Abstract

  The formal specification of design patterns is widely recognized as being vital to their effective and correct use in software development. It can clarify the concepts underlying patterns, eliminate ambiguity and thereby lay a solid foundation for tool support. This paper further advances a formal meta-modelling approach that uses first order predicate logic to specify design patterns. In particular, it specifies both structural and behavioural features of design patterns and systematically captures the variants in a well-structured format. The paper reports a case study involving the formal specification of all 23 patterns in the Gang of Four catalog. It demonstrates that the approach improves the accuracy of pattern specifications by covering variations and clarifying the ambiguous parts of informal descriptions.

  Website 
• Bayley I, Zhu H, 'On the Composition of Design Patterns'
  Quality Software Proceeedings on quality software 2008 (QSIC) , 12-13 (2008) pp.27-36
  ISSN: 1550-6002
  Abstract Design patterns are usually applied in a composed form with each other. It is crucial to be able to formally reason about how patterns can be composed and to prove the properties of composed patterns. Based on our previous work on formal specification of design patterns and formal reasoning about their properties, this paper focuses on the composition of design patterns. A notion of composition of patterns with respect to overlaps is formally defined based on two operations on design patterns, which are the specialisation of a pattern with constraints and the lifting of a pattern with a subset of components as the key. The composition of design patterns is illustrated by the composition of Composite, Strategy and Observer patterns. A case study of the formalisation of the relationship between patterns as suggested by GoF is also reported.Website 
• Bayley I, Zhu H, 'Specifying behavioural features of design patterns in first order logic'
  IEEE International Computer Software and Applications (COMPSAC 2008), Proceedings. (2008) pp.203-210
  ISSN: 0730-3157
  Abstract The formal specification of design patterns is widely recognised as being vital to their effective and correct use in software development. It can clarify the concepts underlying patterns, eliminate ambiguity and thereby lay a solid foundation for tool support. This paper further advances an approach that uses first order predicate logic to specify design patterns by capturing the dynamic behaviour represented in sequence diagrams. A case study of all 23 patterns in the Gang of Four catalogue demonstrates that it can not only capture dynamic features but also simplify the specification of structural properties.Website 
• Martin C, Bayley I, 'Disciplined, Efficient, Generalised Folds for Nested Datatypes'
  Formal Aspects of Computing 16 (2005) pp.19-35
  ISSN: 0934-5043 eISSN: 1433-299X
  Abstract Nested (or non-uniform, or non-regular) datatypes have recursive definitions in which the type parameter changes. Their folds are restricted in power due to type constraints. Bird and Paterson introduced generalised folds for extra power, but at the cost of a loss of efficiency: folds may take more than linear time to evaluate. Hinze introduced efficient generalised folds to counter this inefficiency, but did so in a pragmatic way, at the cost of a loss of reasoning power: without categorical or equivalent underpinnings, there are no universal properties for manipulating folds. We combine the efficiency of Hinze's construction with the powerful reasoning tools of Bird and Paterson's.Website 

Book chapters

• Zhu H, Shan L, Bayley I, Amphlett R, 'A formal descriptive semantics of UML and its applications' in UML 2 Semantics and Applications, John Wiley & Sons (2009)
  ISBN: 9780470409084
  Abstract Summary This chapter contains sections titled: Introduction Definition of Descriptive Semantics in FOPL The LAMBDES Tool Applications Using Model and Metamodel Analysis Conclusions ReferencesWebsite 

Conference papers

• Zhu H, Bayley I, Wang H, 'Continuous Debugging of Microservices'
  (2020) pp.736-745
  ISBN: 9781665414852
  Abstract

  Debugging is one of the most difficult tasks during the development of cloud-native applications for the microservices architecture. This paper proposes a continuous debugging facility to support the DevOps continuous development methodology. It has been implemented and integrated into the Integrated DevOps Environment CIDE for microservices written in the agent-oriented programming language CAOPLE.
  The paper also reports controlled experiments with the debug facility. Experiment data show that the overhead is less than 3% of the execution time on average.
  

  Website 
• Zheng X, Liu D, Zhu H, Bayley I, 'Pattern-based Approach to Modelling and Verifying System Security'
  (2020) pp.92-102
  Abstract

  Security is one of the most important problems in the engineering of online service-oriented systems. The current best practice in security design is a pattern-oriented approach. A large number of security design patterns have been identified, categorised and documented in the literature. The design of a security solution for a system starts with identification of security requirements and selection of appropriate security design patterns; these are then composed together. It is crucial to verify that the composition of security design patterns is valid in the sense that it preserves the features, semantics and soundness of the patterns and correct in the sense that the security requirements are met by the design. This paper proposes a methodology that employs the algebraic specification language SOFIA to specify security design patterns and their compositions. The specifications are then translated into the Alloy formalism and their validity and correctness are verified
  using the Alloy model checker. A tool that translates SOFIA into Alloy is presented. A case study with the method and the tool is also reported.

  Website 
• Zhu H, Bayley I, Liu D, Zheng X, 'Automation of Datamorphic Testing'
  (2020) pp.64-72
  Abstract

  This paper presents an automated tool called Morphy for datamorphic testing. It classifies software test artefacts into test entities and test morphisms, which are mappings on testing entities. In addition to datamorphisms, metamorphisms and seed test case makers, Morphy also employs a set of other test morphisms including test case metrics and filters, test set metrics and filters, test result analysers and test executers to realise test automation. In particular, basic testing activities can be automated by invoking test morphisms. Test strategies can be realised as complex combinations of test morphisms. Test processes can be automated by recording, editing and playing test scripts that invoke test morphisms and strategies. Three types of test strategies have been implemented in Morphy: datamorphism combination strategies, cluster border exploration strategies and strategies for test set optimisation via genetic algorithms. This paper focuses on the datamorphism combination strategies by giving their definitions and implementation algorithms. The paper also illustrates their uses for testing both traditional software and AI applications with three case studies.

  Website 
• Zhu H, Bayley I, 'Exploratory Datamorphic Testing of Classification Applications'
  (2020) pp.51-60
  Abstract

  Testing has been widely recognised as difficult for AI applications. This paper proposes a set of testing strategies for testing machine learning applications in the framework of the datamorphism testing methodology. In these strategies, testing aims at exploring the data space of a classification or clustering application to discover the boundaries between classes that the machine learning application defines. This enables the tester to understand precisely the behaviour and function of the software under test. In the paper, three variants of exploratory strategies are presented with the algorithms as implemented in the automated datamorphic testing tool Morphy. The correctness of these algorithms are formally proved. The paper also reports the results of some controlled experiments with Morphy that study the factors that affect the test effectiveness of the strategies.
  

  Website 
• Zhu H, Liu D, Bayley I, Harrison R, Cuzzolin F, 'Datamorphic Testing: A Method for Testing Intelligent Applications'
  (2019) pp.149-156
  ISBN: 9781728104935 eISBN: 9781728104928
  Abstract

  Adequate testing of AI applications is essential to ensure their quality. However, it is often prohibitively difficult to generate realistic test cases or to check software correctness. This paper proposes a new method called datamorphic testing, which consists of three components: a set of seed test cases, a set of datamorphisms for transforming test cases, and a set of metamorphisms for checking test results. With an example of face recognition application, the paper demonstrates how to develop datamorphic test frameworks, and illustrates how to perform testing in various strategies, and validates the approach using an experiment with four real industrial applications of face recognition.

  Website 
• Zhu H, Wang H, Bayley I, 'Formal Analysis of Load Balancing in Microservices with Scenario Calculus'
  (2018)
  eISSN: 2159-6190
  Abstract Load balancing plays a crucial role in realising the benefits of microservices, especially to achieve elastic scalability and performance optimisation. However, it is different from load balancing for virtual machines, because workloads on microservices are harder to predict and the number of services in the systems is large. In this paper, we formalise load balance as an emergent property of the microservices ecosystem, and employ scenario calculus to formally analyse the impact of scheduling on service capability and scalability. We discovered that elastic round robin scheduling is highly scalable but the service capability is limited by the slowest microservice instance. In contrast, shortest waiting queue scheduling is less scalable, but the service capability is higher.Website 
• Zhu H, Bayley I, 'If Docker Is The Answer, What Is The Question? A Case for Software Engineering Paradigm Shift Towards Service Agent Orientation'
  (2018)
  Abstract The recent rise of cloud computing poses serious challenges for software engineering because it adds complexity not only to the platform and infrastructure, but to the software too. The demands on system scalability, performance and reliability are ever increasing. Industry solutions with
  widespread adoption include the microservices architecture, the container technology and the DevOps methodology. These approaches have changed software engineering practice in
  such a profound way that we argue that it is becoming a paradigm shift. In this paper, we examine the current support of programming languages for the key concepts behind the change in software engineering practice and argue that a novel programming language is required to support the new paradigm. We report a new programming language CAOPLE
  and its associated Integrated DevOps Environment CIDE and demonstrate the utility of both.
• Liu D, Zhu H, Xu C, Bayley I, Lightfoot D, Green M, Marshall P, 'CIDE: An Integrated Development Environment for Microservices'
  (2016) pp.808-812-
  ISBN: 978-1-5090-2628-9/16
  Abstract Microservices is a flexible architectural style that has many advantages over the alternative monolithic style. These include better performance and scalability. It is particularly suitable, and widely adopted, for cloud-based applications, because in this architecture a software system consisting of a large suite of services of fine granularity, each running its own process and communicating with the others. However, programming such systems is more complex. In this paper we report on CIDE, an integrated software development environment that helps with this. CIDE supports programming in a novel agent-oriented language called CAOPLE and tests their execution in a cluster environment. We present the architecture of CIDE, discuss its design based on the principles of the DevOps software development methodology, and describe facilities that support continuous testing and seamless integration, two other advantages of Microservices. Website 
• Xu C, Zhu H, Bayley I, Lightfoot D, Green M, Marshall P, 'CAOPLE: A Programming Language for Microservices SaaS'
  (2016) pp.42-52
  ISBN: 978-1-5090-2253-3
  Abstract

  The microservices architecture is widely regarded as a promising approach to service-oriented systems. However, developing applications in the microservices architecture presents three main challenges: (a) how to program systems that consists of a large number of services running in paral- lel and distributed over a cluster of computers; (b) how to reduce the communication overhead caused by executing a large number of small services; (c) how to support the flexi- ble deployment of services to a network to achieve system load balance. This paper presents a programming language called CAOPLE and reports the implementation of the lan- guage on a virtual machine called CAVM-2. The paper demonstrates how this approach meets these challenges. 

  Website 
• Liu D, Wu X, Zhang X, Zhu H, Bayley I, 'Monic Testing of Web Services Based on Algebraic Specifications'
  (16022376) (2016) pp.24-33
  ISBN: 978-1-5090-2253-3
  Abstract Web services are designed to be discovered and composed dynamically, which implies that testing must also be done dynamically. This involves both the generation of test cases and the checking of test results. This paper presents algorithms for both of these using the technique of algebraic specification. It focuses in particular on the problem that web services, when they are third-party, have poor controllability and observability, and introduces a solution known as monic floating checkable test cases. A prototype tool has implemented the proposed testing technique and it is applied to a case study with a real industry application GoGrid, demonstrating that the technique is both applicable and feasible. Website 
• Liu D, Yang Y, Chen Y, Zhu H, Bayley I, Aldea A, 'Evaluating the Ontological Semantic Description of Web Services Generated from Algebraic Specifications'
  (16022405) (2016) pp.211-220
  ISBN: 978-1-5090-2253-3
  Abstract
  The semantics of web services can be described using ontology or formally specified in mathematical notations. The former is comprehensible and searchable, while the latter is testable and verifiable. To take advantage of both, we proposed, in our previous work, a transformation that takes an algebraic specification of a web service to generate a domain ontology and a semantic description of the service on that ontology.
   
  This paper investigates the quality of these two outputs by proposing a general framework of ontology evaluation that assesses them on 4 aspects of quality, which are decomposed into 8 factors and then measured by a set of 37 metrics. It reports a case study on 3 real-life examples of web services. The results show that the ontologies and semantic descriptions generated from formal specifications are of satisfactory quality. 
   
  Website 
• Zhu H, Bayley I, Younas M, Lightfoot D, Yousef B, Liu D, 'Big SaaS: The Next Step Beyond Big Data'
  (2015) pp.775-784
  ISBN: 978-1-4673-7277-0
  Abstract
  Software-as-a-Service (SaaS) is a model of cloud computing in which software functions are delivered to the users as services. The past few years have witnessed its global flourishing. In the foreseeable future, SaaS applications will integrate with the Internet of Things, Mobile Computing, Big Data, Wireless Sensor Networks, and many other computing and communication technologies to deliver customizable intelligent services to a vast population. This will give rise to an era of what we call Big SaaS systems of unprecedented complexity and scale. They will have huge numbers of tenants/users interrelated in complex ways. The code will be complex too and require Big Data but provide great value to the customer. With these benefits come great societal risks, however, and there are other drawbacks and challenges. For example, it is difficult to ensure the quality of data and metadata obtained from crowdsourcing and to maintain the integrity of conceptual model. Big SaaS applications will also need to evolve continuously. This paper will discuss how to address these challenges at all stages of the software lifecycle.
  Website 
• Liu D, Liu Y, Zhang X, Zhu H, Bayley I, 'Automated Testing of Web Services Based on Algebraic Specification'
  15252318 (2015) pp.143-152
  ISBN: 978-1-4799-8355-1
  Abstract The testing of web services must be done in a com- pletely automated manner when it takes place on-the-fly due to third-party services are dynamically composed to. We present an approach that uses algebraic specification to make this possible. Test data is generated from a formal specification and then used to construct and submit service requests. Test results are then extracted and checked against the specification. All these are done automatically, as required. We present ASSAT (Algebraic Specification-Based Service Automated Testing), a prototype that performs these tasks and demonstrate its utility by applying it to Amazon Web Services, a real-life industrial example. Website 
• Liu D, Zhu H, Bayley I, 'SOFIA: An Algebraic Specification Language for Developing Services'
  (2014) pp.70-75
  Abstract

  Describing the semantics of services accurately plays a crucial role in service discovery, execution, composition and interaction. Formal specification techniques, having evolved over the past 30 years, can define the semantics of software systems in a verifiable and testable manner. This paper presents a new algebraic specification language called SOFIA for describing the semantics of services. It unifies the approaches using algebras and co-algebras for software specifications. A case study with a real industry example, the GoGrid cloud's resource management services, demonstrates that the semantics of services can be specified in SOFIA.

  Website 
• Liu DM, Zhu H, Bayley I, 'A Case Study on Algebraic Specification of Cloud Computing'
  (2013) pp.269-273
  Abstract
  A cloud often provides a RESTful interface with which to access its services. These are usually specified through an open but informal document in the IT industry. There is no agreed standard for the specification of RESTful web services. In this paper, we propose the application of an algebraic method to the formal specification of such services and report a case study with the GoGrid’s RESTful API, an industrial real system that provides Infrastructure-as-a-Service. The case study demonstrates that the algebraic approach can provide formal unambiguous specifications that are easy to read and write. It also demonstrates that formalisation can identify and eliminate ambiguity and inconsistency in informal documents.
  Website 
• Brown D, Bayley I, Harrison R, Martin C, 'Developing a Mobile Case-based Reasoning Application to Assist Type 1 Diabetes Management'
  (2013)
  ISBN: 978-1-4673-5800-2
  Abstract Effective management of diabetes is crucial for patient wellbeing and the prevention of low blood sugar levels (Hypoglycemia) and high blood sugar levels (Hyperglycemia) both of which can be potentially dangerous. Traditionally log books are maintained by patients to record information such as insulin usage and their meals. The ever increasing popularity of smart phones has resulted in various applications being developed to allow patients to log data and help manage their condition. However these applications are often developed simply for the logging of data and only occasionally provide basic calculations to suggest insulin doses following a meal. The goal of this research is to use case-based reasoning techniques to suggest an insulin dosage for the patient as opposed to using a one calculation fits all approach. This is to be achieved by building a knowledge base of the patient's history that is then used to obtain a solution which best fits the current circumstances. The proposed case-based reasoning system is described alongside the development of the system to date and discussion into further research and development. The final implementation will be tested and validated using a diabetic patient simulator to create a knowledge base and observe system behavior and accuracy.Website 
• Bayley I, Flood D, Harrison R, Martin C, 'Mobitest: A cross-platform tool for testing mobile applications'
  (2012)
  ISBN: 978-1-61208-230-1
  Abstract
  Testing is an essential part of the software  development lifecycle. However, it can cost a lot of time and  money to perform. For mobile applications, this problem is  further exacerbated by the need to develop apps in a short  time-span and for multiple platforms. This paper proposes MobiTest, a cross-platform automated testing tool for mobile  applications, which uses a domain-specific language for mobile  interfaces. With it, developers can define a single suite of tests  that can then be run for the same application on multiple  platforms simultaneously, with considerable savings in time  and money.
  Website 
• Brown D, Bayley I, Harrison R, Martin C, 'Formal specification of a mobile diabetes management application using the Rodin platform and Event-B'
  (2012) pp.43-44
  
• Zhu H, Bayley I, 'Laws of Pattern Composition'
  6447 (2010) pp.630-645
  ISBN: 9783642169007
  Abstract

  Design patterns are rarely used on their own. They are almost always to be found composed with each other in real applications. So it is crucial that we can reason about their compositions. In our previous work, we defined a set of operators on patterns so that pattern compositions can be represented as expressions on patterns. In this paper, we investigate the algebraic properties of these operators, prove a set of algebraic laws that they obey, and use the laws to show the equivalence of pattern compositions.

  Website 
• Bayley I, Zhu H, 'A formal language of pattern compositions'
  (2010) pp.1-6
  ISBN: 9781618396419
  Abstract In real applications, design patterns are almost always to be found composed with each other. Correct application of patterns therefore relies on precise definition of these compositions. In this paper, we propose a set of operators on patterns that can be used in such definitions. These operators are restriction of a pattern with respect to a constraint, superposition of two patterns, and a number of structural manipulations of the pattern's components. We also report a case study on the pattern compositions suggested informally in the Gang of Four book in order to demonstrate the expressiveness of the operators.
• Zhu H, Bayley I, Shan L, Amphlett R, 'Tool support for design pattern recognition at model level'
  (2009) pp.228-233
  ISBN: 9780769537269
  Abstract

  Given the rapid rise of model-driven software development methodologies, it is highly desirable that tools be developed to support the use of design patterns in this context. This paper presents such a tool, called LAMBDES-DP, with UML diagrams as the software design models. Its theoretical foundation is a descriptive semantics of UML in first order logic, and the design patterns are formally specified in the same language. The tool uses the LAMBDES system to translate the UML diagrams into their descriptive semantics and invokes the theorem prover SPASS to decide whether the design conforms to a pattern. Our experiments show that our tool has significantly lower rates of false positive and false negative errors compared with existing tools.

  Website 
• Bayley I, Zhu H, 'Formalising design patterns in predicate logic'
  (2007) pp.25 - 36
  ISBN: 9780769528847
  Abstract Design patterns are traditionally outlined in an informal manner. If they could be formalised, we could derive tools that automatically recognise design patterns and refactor designs and code. Our approach is to deploy predicate logic to specify conditions on the class diagrams that describe design patterns. The structure of class diagrams is itself described with a novel meta-notation that can be used for defining any graphical modelling language. As a result, the constraints, while based on UML, are highly readable and have much expressive power. This enables us not only to recognise design patterns in legacy code, but also to reason about them at the design stage, such as showing one pattern to be a special case of another. The paper discusses our specification of the original 23 design patterns and presents a representative sample of some of them.Website 

Areas of expertise

• software engineering:
  • design patterns
  • web services
• formal methods
  • model-based specification
  • algebraic specification
• programming languages
  • object-oriented programming
  • functional programming
  • agent-oriented programming

Conferences

• PC co-chair for COMPSAC SETA 2018

Other experience

• Lecturer at University of Bournemouth