Professor Hong Zhu

Cyberspace in increasingly important to people in their everyday lives for purchasing goods on the Internet, to energy supply increasingly managed remotely using Internet protocols. Unfortunately, this dependence makes us susceptible to attacks from nation states, terrorists, criminals and hactivists. Therefore, we need a better understanding of cyberspace, for which patterns, which are predictable regularities, may help to detect, understand and respond to incidents better. The inspiration for the workshop came from the existing work on formalising design patterns applied to cybersecurity, but we also need to understand the many other types of patterns that arise in cyberspace. Includes extended and updated papers from the First International Workshop on Cyberpatterns.

A pattern represents a discernible regularity in the world or in manmade designs. In the prescriptive point of view, a pattern is a template from which instances can be created; while in the descriptive point of view, the elements of a pattern that repeat in a predictable manner can be observed and recognised. Similar to theories in sciences, patterns explain and predict regularities in a subject domain. In a complicated subject domain like cyberspace, there are usually a large number of patterns that each describes and predicts a subset of recurring phenomena, yet these patterns can interact with each other and be interrelated and composed with each other. The pattern-oriented research method studies a subject domain by identifying the patterns, classifying and categorising them, organising them into pattern languages, investigating the interactions between them, devising mechanisms and operations for detecting and predicting their occurrences, and facilitating their instantiations. This chapter illustrates this research methodology through a review of the research on software design patterns as an example of successful application of the methodology. It then discusses its possible applications to the research on cyberpatterns, i.e. patterns in cyberspace. It defines the scope of research, reviews the current state of art and identifies the key research questions.

HASARD stands for Hazard Analysis of Software ARchitectural Designs. It is a model-based method for the analysis of software quality as entailed in software architectural designs. In this method, quality hazards are systematically explored and their causes and effects are identified. The results of hazard analysis are then transformed into a graphical quality model of the system under assessment. Queries about quality related properties of the system can be answered automatically through a set of algorithms with the quality model as the input. Such queries include: (1) the relationships between various quality attributes as manifested in the particular design, (2) the design decisions critical to a given quality concern, (3) the impacts of a given design decision to quality attributes, (4) trade-off points in the design that balancing conflict quality

concerns, etc. The chapter will present a prototype tool called SQUARE to support the whole process of HASARD analysis. It will also report a case study with a real software system to demonstrate the feasibility and usability of the HASARD method.

of software design patterns (DP) has been identified, catalogued and formalised in

the past decades. Tools have been developed to support the application and recognition

of patterns. However, although the notions of pattern in different subject domains

carry a great deal of similarity, we are in lack of a general pattern representation

approach that applies to all types of design patterns. Based on our previous

work on formalisation of OO DPs and an algebra of pattern compositions, this paper

proposes a generalisation of the approach so that it can be applied to other types

of DPs. In particular, a pattern is defined as a set of points in a design space that

satisfy certain conditions. Each condition specifies a property of the instances of the

pattern in a certain view of the design space. The patterns can then be composed

and instantiated through applications of operators defined on patterns. The paper

demonstrates the feasibility of the proposed approach by examples of patterns of

enterprise security architecture.

development of cyber systems from a new angle. They can help us move from an

improvised craft to an engineering discipline because they help to transfer knowledge

about proven solutions in an understandable and reusable format. They allow

innovative applications in cloud, cyber-physical and mobile systems, and novel

methods of use with data patterns for observation and analysis of ‘big data’ problems.

The ultimate aim of research on cyberpatterns is an overall framework for

cyberpatterns integrating all the cyber domains to help develop a betterunderstood

and effective cyberspace. However, there are many research questions

in cyberpatterns that remain unanswered regarding both their conceptual foundation

and practical use. This chapter concludes the book by exploring some of the

most critical and important problems needing to be addressed.

This paper presents a method of component testing based on algebraic specifications. An algorithm for generating checkable test cases is proposed. A proto-type testing tool called CASCAT for testing Java En-terprise Beans is developed. It has the advantages of high degree of automation, which include test case generation, test harness construction and test result checking. It achieves scalability by allowing incre-mental integration. It also allows testing to focus on a subset of used functions and key properties, thus suit-able for component testing. The paper also reports an experimental evaluation of the method and the tool.

This paper proposes a scenario-based functional testing approach for enhancing the performance of machine learning (ML) applica- tions. The proposed method is an iterative process that starts with testing the ML model on various scenarios to identify areas of weakness. It follows by a further testing on the suspected weak scenarios and statistically evaluate the model’s performance on the scenarios to confirm the diagnosis. Once the diagnosis of weak scenarios is confirmed by test results, the treatment of the model is performed by retraining the model using a transfer learning technique with the original model as the base and applying a set of training data specifically targeting the treated scenarios plus a subset of training data selected at random from the original train dataset to prevent the so-call catastrophic forgetting effect. Finally, after the treatment, the model is assessed and evaluated again by testing on the treated scenarios as well as other scenarios to check if the treatment is effective and no side-effect caused. The paper reports a case study with a real ML deep neural network (DNN) model, which is the perception system of an autonomous racing car. It is demonstrated that the method is effective in the sense that DNN model’s performance can be improved. It provides an efficient method of enhancing ML model’s performance with much less human and compute resource than retrain from scratch.

Metrics play a crucial role in evaluating the performance of machine learning (ML) models. Metrics for quantifying the extent of errors, in particular, have been intensively studied and widely used but only so far for regression models. This paper focuses instead on classifier models. A new approach is proposed in which datamorphic exploratory testing is used to discover the boundary values between classes and the distance of misclassified instances from that boundary is used to quantify the errors that the model makes. Empirical experiments and case studies are reported that validate and evaluate the proposed metrics.

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.

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.

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.

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.

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.

NoSQL cloud database systems are new types of databases that are built across thousands of cloud nodes and are capable of storing and processing Big Data. NoSQL systems have

increasingly been used in large scale applications that need high availability and efficiency but with weaker consistency. Consequently, such systems lack support for standard transactions which provide stronger consistency. This paper proposes a new multi-key transactional model which provides NoSQL systems with standard transaction support and stronger level of data consistency. The strategy is to supplement current NoSQL architecture with an extra layer that manages transactions. The proposed model is configurable where consistency, availability and efficiency can be adjusted based on application requirements. The proposed model is validated through a prototype system using MongoDB. Preliminary experiments show that it ensures stronger consistency and maintains good performance.

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. 

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. 

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.

Tenant level checkpointing is a novel fault-tolerance technique proposed in our previous work for largescale software-as-a-service applications. This paper evaluates the technique by a theoretical analysis of the technique and an empirical study using workload benchmarks of real largescale cluster systems. We propose the notion of accumulated delay as a measurement of the performance of checkpointing techniques. It reflects the effect of checkpointing on system

performance as experienced by the end users. Both theoretical analysis and empirical study show that tenant level checkpointing significantly outperforms traditional bulk checkpointing as

measured by the amount of accumulated delays.

Automated test framework plays a significant role in test driven software development methodologies. The XUnit family of testing tools has been widely used in the industry. However, they are weak in supporting test case generation and test result checking. In this paper we propose a new kind of test automation framework by integrating data mutation testing and metamorphic testing methods. A tool for unit testing of Java class called JFuzz is presented. Its uses are illustrated by examples.

With the advent of embedded and mobile computing techniques, software systems are increasingly operated in open and dynamic environments. Such systems desire self-adaptive capabilities. This paper proposes an agent-oriented approach to the modeling and simulation of distributed adaptive systems. The approach enables to construct structural and behavioral models at a high abstraction level, and to validate the models at design stage through model simulation. The modeling language facilitates devising decentralized adaption logic at both component and system levels. Simulation demonstrates how a

system dynamically re-organizes in response to the changes in the operating context. Case studies show that our approach can support various self-adaptation mechanisms with which a multi-agent system adjusts to internal failures, unexpected environment, or user's changing requirements.

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.

Traditional checkpointing techniques are facing a grave challenge when applied to multi-tenancy software-as-a-service (SaaS) systems due to the huge scale of the system state and the diversity of users' requirements on the quality of services. This paper proposes the notion of tenant level checkpointing and an algorithm that exploits Big Data techniques to checkpoint tenant's meta-data, which are widely used in configuring SaaS for tenant-specific features. The paper presents a prototype implementation of the proposed technique using NoSQL database Couchbase and reports the experiments that compare it with traditional implementation of checkpointing using file systems. Experiments show that the Big Data approach has a significantly lower latency in comparison with the traditional approach.

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.

The research on software design in the past decades has made some breakthroughs that may lead to a revolutionary new type of software design tools so that software developers can benefit from creative computing. These research results combined with the general theory of design methodologies may make creativity in software design benefit from automation. The following briefly examine such theories and research results in the light of creative computing.

The author presents a theorem that states that the correctness of a software system can be validated by testing on a finite number of test cases provided that the program and specification are in a learnable set of functions. Moreover, such testing can be performed without writing down a formal specification. This lays a foundation of the current practice of software testing where formal specifications are not available. This theorem implies that what current testing practice lacks is an analysis of the "complexity" of the program to determine a learnable set within which the program and the specification vary.

This paper presents an algebraic specification language for the formal specification of the semantics of web services. A set of rules for transforming WSDL into algebraic structures is proposed. Its practical usability is also demonstrated by an example.

A long lasting myth of formal methods is that they are difficult to learn and expensive to apply. This paper reports a controlled experiment to test if this myth is true or false in the context of writing algebraic formal specifications. The experiment shows that writing algebraic specifications for software components can be learnt by ordinary university students. It does not heavily depend on mathematical knowledge and skills. Moreover, it is not time consuming to write algebraic specifications for software components.

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.

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.

Scenario analysis has been widely perceived to be able to play two important roles in requirement engineering. Firstly, it is a vehicle of separating concerns in the elicitation of users' requirements. Secondly, it is a means of validating specified requirements. However, there are a number of key activities in scenario analysis that demand automated tool support to make the method practically applicable. Such activities include: (a) the analysis of consistency and completeness among various scenarios, (b) the analysis of the consistency and completeness of a set of scenarios with respect to

requirements models, (c) the synthesis of requirements models from a set of scenarios, and (d) the generation of scenarios from requirements models for requirements validation. In this paper, we present an automatic toolkit that supports these activities. We discuss how the idea of scenario analysis can be adapted to a structured analysis method, how to describe scenarios and how to support scenario

analysis activities through automated tools. We also report some case studies with the toolkit.