Unified Modelling Language (UML) has been conferred as the de facto standard in modeling by majority in the software system development community. Among the various types of diagrams that exist under the umbrella of UML is Sequence Diagram. Sequence Diagrams are capable of modeling interactional behaviours as well as dynamic happenings in a system, and as such are generally used in the modeling of complex software systems. However in this paper, Sequence Diagrams are used in the modeling of the IEEE 802.11 Carrier Sense Multiple Access with Collision Avoidance (CSMA/CA) protocol. The Sequence Diagram representing this protocol will then be used for formal, mathematical analysis by first transforming the Sequence Diagram through the MDA model transformation tool called SD2PN, and performing analysis such as liveness analysis, boundedness analysis and reachability analysis of the resulting Petri Net.

Machine learning-based malware detection systems have been widely suggested and used as a replacement for signature-based detection methods. Such systems have shown that they can provide a high detection rate when recognising non-previously seen malware samples. However, when classifying malware based on their behavioural features, some new malware can go undetected, resulting in a misclassification. Our aim is to gain more understanding of the underlying causes of malware misclassification; this will help to develop more robust malware detection systems. Towards this objective, several questions have been addressed in this paper: Does misclassification increase over a period of time? Do changes that affect classification occur in malware at the level of families, where all instances that belong to certain families are hard to detect? Alternatively, can such changes be traced back to certain malware variants instead of families? Also, does misclassification increase when removing distinct API functions that have been used only by malware? As this technique could be used by malware writers to evade the detection. Our experiments showed that changes in malware behaviour are mostly due to behavioural changes at the level of variants across malware families, where variants did not behave as expected. It also showed that machine learning-based systems could maintain a high detection rate even in the case of trying to evade the detection by not using distinct API functions, which are uniquely used by malware.

Recent technical advances in utility computing have allowed small and medium sized businesses to move their applications to the cloud, to benefit from features such as auto-scaling and pay-as-you-go facilities. Before clouds are widely adopted, there is a need to address privacy concerns of customer data outsourced to these platforms. In this paper, we present a practical approach for protecting the confidentiality and integrity of client data and computation from insider attacks such as cloud clients as well as from the Infrastructure-as-a-Service (IaaS) based cloud system administrator himself. We demonstrate a scenario of how the origin integrity and authenticity of health-care multimedia content processed on the cloud can be verified using digital watermarking in an isolated environment without revealing the watermark details to the cloud administrator. Finally to verify that our protocol does not compromise confidentiality and integrity of the client data and computation or degrade performance, we have tested a prototype system using two different approaches. Formal verification using ProVerif tool shows that cryptographic operations and protocol communication cannot be compromised using a realistic attacker model. Performance analysis of our implementation demonstrates that it adds negligible overhead.

Clinical guidelines specify sequences of steps (care pathways) to treat patients with single conditions. Increasingly, many patients exhibit “multimorbidity,” several chronic conditions needing concurrent treatment. However, applying multiple guidelines in parallel can lead to conflicts, eg, between prescribed drugs, lifestyle intervention recommendations, or treatment schedules. In computer science, process languages used to design and reason about software development and business process management are similar to clinical pathways. Using formal model transformation, composition and analysis methods, models can be combined and conflicts detected and resolved. We propose BPMN+V, a data‐driven formal model for clinical care pathways, as an extension of Business Process Model and Notation. We describe a method for conflict detection using a transformation of BPMN+V to Coloured Petri Nets and a state‐space method for detection of conflict in composed models. We present results from a case study, showing that common conflicts are successfully detected, and propose extension to a complete framework for efficiently recommending resolutions to medical conflicts in composed care pathway models.

Energy management has become an important concern in virtualized environments; Cloud providers are developing and using techniques to minimize the energy consumption of their data centres. Providers rely immediately on elastic computing to scale-up or -down infrastructure resources based on incoming workloads and user settings. However, elasticity comes at a price, as adding resources may significantly increase energy usages and costs. We believe that, before scaling-up, it is possible to cope with different workloads and energy expenditure by automatically reconfiguring the software architecture of the Cloud. This paper presents a self-adaptive architecture and a set of techniques that use information about energy consumption to enforce policies to reduce cost and energy. We experiment our approach by reconfiguring different HTTP servers and web applications of the back-end servers based on the workload and energy consumption without interrupting current running services. Our approach proves more efficient when compared to elasticity methods under the same workloads.

A number of machine learning based malware detection systems have been suggested to replace signature based detection methods. These systems have shown that they can provide a high detection rate when recognising non-previously seen malware samples. However, in systems based on behavioural features, some new malware can go undetected as a result of changes in behaviour compared to the training data. In this paper we analysed misclassified malware instances and investigated whether there were recognisable patterns across these misclassifications. Several questions needed to be understood: Can we claim that malware changes over time directly affect the detection rate? Do changes that affect classification occur in malware at the level of families, where all instances that belong to certain families are hard to detect? Alternatively, can such changes be traced back to certain malware variants instead of families? Our experiments showed that these changes are mostly due to behavioural changes at the level of variants across malware families where variants did not behave as expected. This can be due to the adoption of anti-virtualisation techniques, the fact that these variants were looking for a specific argument to be activated or it can be due to the fact that these variants were actually corrupted.

SUMMARY Clinical guidelines specify sequences of steps (care pathways) to treat patients with single conditions. Increasingly many patients exhibit ‘multimorbidity’, several chronic conditions needing concurrent treatment. However, applying multiple guidelines in parallel can lead to conflicts, e.g. between prescribed drugs, lifestyle intervention recommendations, or treatment schedules. In computer science, process languages used to design and reason about software development and business process management are similar to clinical pathways. Using formal model transformation, composition and analysis methods, models can be combined and conflicts detected and resolved. We propose BPMN+V, a data-driven formal model for clinical care pathways, as an extension of BPMN. We describe a method for conflict detection using a transformation of BPMN+V to Coloured Petri Nets, and a state-space method for detection of conflict in composed models. We present results from a case study, showing that common conflicts are successfully detected, and propose extension to a complete framework for efficiently recommending resolutions to medical conflicts in composed care pathway models. Copyright c (cid:13) 2017 John Wiley & Sons, Ltd.

Delivering cloud services with better quality-of- service demands infrastructures which are autonomic and self- manageable. In particular, there is a clear scope for developing automated methods for enforcing suitable management policies that would run such infrastructures. An example of a management policy is the one that governs the triggering of migration of virtual machines to manage energy consumption. Although there is extensive research on developing novel methods of implementing such policies in an autonomic manner, the identification of suitable policies in terms of cost reduction has received less attention. This requires an analysis of two given sets of policies to identify which one is more suitable. This paper presents a method involving Coloured Petri Nets for an offline modelling and analysis of an autonomic cloud platform which executes sets of policies. We use traces of execution in Petri Nets for calculating minimum cost associated to each set of policies. Petri Net models can generate infinite traces because of the appearance of loops. However, as migration of virtual machines entails cost, many of the infinite traces will not result in the identification of the minimal cost. This paper presents an analytical method using Integer Programming to find the minimum cost of energy consumption for a given policy. We evaluated our approach with the help of an energy management case study.

Large system models usually consist of several simpler models that can be understood more easily. Making changes to the behaviour of a component will likely affect several models and could introduce accidental errors. Aspects address this by modelling new functionality required in several places as an advice, which can be integrated with the original base models by specifying a pointcut. Before checking that the overall outcome is correct, we need to weave the cross-cutting advice into the base models, and obtain new augmented models. Although considerable research has been done to weave models, many such approaches are not fully automated. This paper looks at aspect weaving of scenario-based models, where aspects are given a true-concurrent semantics based on event structures. Our contribution is a novel formal automated technique for weaving aspects using the Z3-SMT solver. We compare the performance of Alloy and Z3 to justify our choice.

This paper presents a new technique for failure diagnosis in partially observable discrete event systems modelled as Petri nets. In this new technique we adopt Integer Fourier-Motzkin Elimination (IFME) method. We start with a Petri net and produce the state equations. The state equations are a set of integer valued inequalities in variables that represent number of firing of transitions. Occurrences of failure can also be expressed by inequalities. Then we extend the set of inequalities obtained from the state equations to two new sets. The first is created from adding the inequality for failure. The second is created from adding the negation of the inequality for failure. Applying the IFME method to the two resulting sets of inequalities, the variables corresponding to unobservable transitions will be eliminated. Then we prove that for acyclic Petri nets, the reduced set of inequalities after the elimination can be used to diagnose failures.

Rule-based systems process event streams and trigger actions according to pre-defined rule-sets. Over the last three decades, such systems have been widely used in businesses, governments and organisations. However, with today's need to process larger event streams such as events produced in Internet of Things (IoT), current rule-based systems face serious challenges in terms of speed, scalability and fault tolerance. Spark Streaming is emerging as a novel solution to address these challenges. This paper presents an approach for adapting rule-based systems to work with Spark Streaming. We focus on Rete algorithm which is behind many of the current rule engines. We present DRESS (Distributed Rule Engine on Spark Streaming), an infrastructure for executing Rete algorithm on Spark Streaming. In addition, we present an automated method of transforming rules written in Drools' style to be executed on DRESS. The performance of our system was evaluated with the help of a case study.

As modern systems become more complex, design approaches model different aspects of the system separately. When considering (intra and inter) system interactions, it is usual to model individual scenarios using UML’s sequence diagrams. Given a set of scenarios we then need to check whether these are consistent and can be combined for a better understanding of the overall behaviour. This paper addresses this by presenting a novel formal technique for composing behavioural models at the metamodel level through exact metamodel restriction (EMR). In our approach a sequence diagram can be completely described by a set of logical constraints at the metamodel level. When composing sequence diagrams we take the union of the sets of logical constraints for each diagram and additional behavioural constraints that describe the matching composition glue. A formal semantics for composition in accordance with the glue guides our model transformation to Alloy. Alloy’s fully automated constraint solver gives us the solution. Our technique has been implemented as an Eclipse plugin SD2Alloy.

The design of large systems often involves the creation of models that describe partial specifications. Model composition is the process of combining partial models to create a single coherent model. This paper presents an automatic composition technique for creating a sequence diagram from partial specifications captured in multiple sequence diagrams with the help of Alloy. Our contribution is twofold: a novel true-concurrent semantics for sequence diagram composition, and a model-driven transformation of sequence diagrams to Alloy that preserves the semantics of composition defined. We have created a tool SD2Alloy that implements the technique as follows: two given sequence diagrams are transformed into two Alloy models, and merged according to a set of syntactic logical constraints describing how their elements should be matched. These constraints are in accordance to our compositional semantics. The technique can also be used to detect problems and inconsistencies in the composition of diagrams.

Forensic Virtual Machines are a new technology that replaces signature-based malware detection for the cloud. Forensic Virtual Machines are mini-VMs which are used to identify symptoms of malicious behaviour on customer VMs. Scanning using these mini-VMs consumes less resources than a full scan would and their small size reduces the possibility of the FVMs themselves containing vulnerabilities. A mobility algorithm embedded in every FVM specifies how it chooses which customer VM to scan. Although multiple scanning strategies have been introduced, there is no work which provides a comparison of these strategies. In this paper, we develop a probabilistic approach which tells us which strategy is best for a given cloud environment and particular family of malware. Our framework uses Bayesian probability in addition to a malware knowledge base in order to simulate the scanning process of a number of FVMs.

Although the deployment of TLS has been of great importance to its users in preventing eavesdroppers from reading personal data, it also prevents intrusion detection systems (IDSs) from completing their own tasks, as they are, in essence, eavesdroppers themselves. Cloud providers specifically are at risk because of the pure mass of data they accrue over the many applications they serve, so they have a responsibility to protect both themselves and their users. Without the keys, however, they can't provide the service they require. A method to acquire these keys is to use virtual machine introspection (VMI), a technique that allows an application to read the internal state of a virtual machine. Current methods are expensive and require the application to read the entire virtual machine's memory. The authors present an efficient approach to acquire RSA keys, commonly used on the Internet, using the forensic virtual machine (FVM) framework. This framework provides the ability, from another virtual machine to use VMI to find, analyze, and act on these findings.

To benefit from the advantages that Cloud Computing brings to the IT industry, management policies must be implemented as a part of the operation of the Cloud.Among others, for example, the specification of policies can be used for the management of energy to reduce the cost of running the IT system or also for security policies while handling privacy issues of users.As cloud platforms are large, manual enforcement of policies is not scalable.Hence, autonomic approaches for management policies have recently received a considerable attention.These approaches allow specification of rules that are executed via rule-engines.The process of rules creation starts by the interpretation of the policies drafted by high-rank managers.Then, technical IT staff translate such policies to operational activities to implement them.Such process can start from a textual declarative description and after numerous steps terminates in a set of rules to be executed on a rule engine.To simplify the steps and to bridge the considerable gap between the declarative policies and executable rules, we propose a domain-specific language called CloudMPL.We also design a method of automated transformation of the rules captured in CloudMPL to the popular rule-engine Drools.As the policies are changed over time, code generation will reduce the time required for the implementation of the policies.In addition, using a declarative language for writing the specifications is expected to make the authoring of rules easier.We demonstrate the use of the CloudMPL language into a running example extracted from a management energy consumption case study.

Cloud providers must detect malicious traffic in and out of their network, virtual or otherwise. The use of Intrusion Detection Systems (IDS) has been hampered by the encryption of network communication. The result is that current signatures cannot match potentially malicious requests. A method to acquire the encryption keys is Virtual Machine Introspection (VMI). VMI is a technique to view the internal, and yet raw, representation of a Virtual Machine (VM). Current methods to find keys are expensive and use sliding windows or entropy. This inevitably requires reading the memory space of the entire process, or worse the OS, in a live environment where performance is paramount. This paper describes a structured walk of memory to find keys, particularly RSA, using as fewer reads from the VM as possible. In doing this we create a scalable mechanism to populate an IDS with keys to analyse traffic.

The automated execution of model transformation plays a key role within Model Driven Development. The software that executes a transformation, commonly known as a transformation engine, receives the meta-models of the source and destination, and a set of transformation rules as input. Then the engine can be used to convert instances of the source meta-model to produce a destination model. Transformation engines are often seen as black boxes. In order to be sure of the correct execution, it is crucial to understand how a transformation engine executes a given transformation. This paper presents a method of capturing and analysing the activities carried out within the transformation engine by elaborating on existing tracing mechanisms used by existing engines. We compare the tracing mechanisms involved in four popular, rule-based transformation frameworks and highlight their shortcomings. A new trace meta-model is presented to deal with some of these shortcomings. These processes can be applied to all existing frameworks; as a proof of concept we have extended an existing traceability framework, based on our earlier work, to implement these mechanisms.

Design of large systems often involves the creation of models that describe partial specifications. Model composition is the process of combining partial models to create a single coherent model. This paper presents an automatic composition technique for creating a sequence diagram from partial specifications captured in multiple sequence diagrams with the help of Alloy. Our contribution is twofold: a novel true-concurrent semantics for sequence diagram composition, and a model-driven transformation of sequence diagrams onto Alloy that preserves the semantics of composition defined. We have created a tool called SD2Alloy that implements the automated technique and works as follows: two given sequence diagrams are transformed in two Alloy models, and then combined according to a set of logical constraints, determined by our compositional semantics, into a final composed Alloy model. The technique can also be used to detect problems and inconsistencies in the composition of diagrams.