DSpace Collection:
http://hdl.handle.net/2381/385
Sun, 01 May 2016 08:08:31 GMT2016-05-01T08:08:31ZEfficient Embedded Software Migration towards Clusterized Distributed-Memory Architectures
http://hdl.handle.net/2381/37451
Title: Efficient Embedded Software Migration towards Clusterized Distributed-Memory Architectures
Authors: Garibotti, Rafael; Butko, Anastasiia; Ost, Luciano; Gamatie, Abdoulaye; Sassatelli, Gilles; Adeniyi-Jones, Chris
Abstract: A large portion of existing multithreaded embedded sofware has been programmed according to symmetric shared memory platforms where a monolithic memory block is shared by all cores. Such platforms accommodate popular parallel programming models such as POSIX threads and OpenMP. However with the growing number of cores in modern manycore embedded architectures, they present a bottleneck related to their centralized memory accesses. This paper proposes a solution tailored for an efficient execution of applications defined with shared-memory programming models onto on-chip distributed-memory multicore architectures. It shows how performance, area and energy consumption are significantly improved thanks to the scalability of these architectures. This is illustrated in an open-source realistic design framework, including tools from ASIC to microkernel.Tue, 26 Apr 2016 14:07:53 GMThttp://hdl.handle.net/2381/374512016-04-26T14:07:53ZFinitary Logics for Coalgebras with Branching
http://hdl.handle.net/2381/37190
Title: Finitary Logics for Coalgebras with Branching
Authors: Kissig, Christian
Abstract: The purpose of this dissertation is to further previous work on coalgebras as infinite statebased
transition systems and their logical characterisation with particular focus on infinite
regular behaviour and branching.
Finite trace semantics is well understood [DR95] for nondeterministic labelled transition
systems, and has recently [Jac04, HJS06] been generalised to a coalgebraic level
where monads act as branching types for instance, of nondeterministic choice. Finite
trace semantics then arises through an inductive construction in the Kleisli-category of
the monad. We provide a more comprehensive definition of finite trace semantics, allowing
for finitary branching types in Chapter 5. In Chapter 6 we carry over the ideas behind
our definition of finite trace semantics to define infinite trace semantics.
Coalgebraic logics [Mos99] provide one approach to characterising states in coalgebras
up to bisimilarity. Coalgebraic logics are Boolean logics with the modality r. We
define the Boolean dual of r in the negation-free fragment of finitary coalgebraic logics
in Chapter 7, showing that finitary coalgebraic logics are essentially negation free. Our
proof is largely based on the previously established completeness of finitary coalgebraic
logics [KKV08].
Finite trace semantics induces the notion of finite trace equivalence. In Chapter 8 we
define coalgebraic logics for many relevant branching and transition types characterising
states of coalgebras with branching up to finite trace equivalence. Under further assumptions
we show that these logics are expressive.
Coalgebra automata allow us to state finitary properties over infinite structures essentially
by a fix-point style construction. We use the dualisation of r from Chapter 7 to prove that coalgebra automata are closed under complementation in Chapter 10. This result
completes a Rabin style [Rab69] correspondence between finitary coalgebraic logics
and coalgebra automata for finitary transition types, begun in [Ven04, KV05].
The semantics of coalgebra automata is given in terms of parity graph games [GTW02].
In Chapter 9 we show how to structure parity graph games into rounds using the notion
of players power [vB02] and how to normalise the interaction pattern between the players
per round. From the latter we obtain the coinductive principle of game bisimulation.
Languages accepted by coalgebra automata are called regular. Regularity is commonly
[Sip96, HMU03] disproved using the pumping lemma for regular languages. We
define regular languages of coalgebras and prove a pumping lemma for these languages
in Chapter 11.Thu, 07 Apr 2016 11:33:58 GMThttp://hdl.handle.net/2381/371902016-04-07T11:33:58ZIntegrating user knowledge into design pattern detection
http://hdl.handle.net/2381/36232
Title: Integrating user knowledge into design pattern detection
Authors: Alshira'H, Mohammad H.
Abstract: Design pattern detection is useful for a range of software comprehension and maintenance
tasks. Tools that rely on static or dynamic analysis alone can produce
inaccurate results, especially for patterns that rely on the run-time information.
Some tools provide facilities for the developer to refine the results by adding their
own knowledge. Currently, however, the ability of tools to accommodate this knowledge
is very limited; it can only pertain to the detected patterns and cannot provide
additional knowledge about the source code, or about its behaviour. In this thesis,
we propose an approach to combine existing pattern detection techniques with
a structured feedback mechanism. This enables the developer to refine the detection
results by feeding-in additional knowledge about pattern implementations and
software behaviour. The motivation is that a limited amount of user input can complement
the automated detection process, to produce results that are more accurate.
To evaluate the approach we applied it to a selection of openly available software
systems. The evaluation was carried in two parts. First, an evaluation case study
was carried out to detect pattern instances in the selected systems with the help
of the user knowledge. Second, a user study of a broader range of expert users of
design patterns was conducted in order to investigate the impact of their knowledge
on the detection process, and to see whether it is realistic that the user can identify
useful knowledge for the detection process. The evaluation results indicate that
the proposed approach can yield a significant improvement in the accuracy whilst
requiring a relatively small degree of user input from the developer. Moreover, the
results show that expert users can supplement the design pattern detection process
with a useful feedback that can enhance the detection of design pattern instances in
the source code.Fri, 08 Jan 2016 16:11:49 GMThttp://hdl.handle.net/2381/362322016-01-08T16:11:49ZOptimal control of two distributed parameter systems.
http://hdl.handle.net/2381/34933
Title: Optimal control of two distributed parameter systems.
Authors: Williams, V (Vaughan)
Abstract: Part I. A heat conduction problem is outlined, where the state of the system under consideration is described by a linear parabolic partial differential equation in one space dimension, with bounded controlling boundary conditions. A cost functional is defined in terms of an integral involving some specified "target function". Integral expressions describing the evolution of the system under the influence of various initial and boundary conditions are given; Butkovskii's Maximum Principle is formally applied to modified forms of these expressions, to give equations determining the optimal control function. Pontryagin's Maximum Principle is applied to a discrete approximation to the distributed system, and a connection is demonstrated between the optimal control thus obtained and that for the distributed system. A further connection is demonstrated with the solution obtained after applying calculus of variations techniques to a notionally unconstrained version of the problem. Difficulties of numerical solution are discussed, and the need for further constraints is pointed out. Solutions to some numerical examples are given. PART II. Equations governing one-dimensional non-turbulent compressible fluid flow in a pipe are given, and the waterhammer problem is described. The method known as "valve stroking" is outlined for a linearized version of this problem. A necessary condition on the optimal solution to the linearized problem is demonstrated, and it is shown that valve stroking does not satisfy this condition, and produces neither a time-optimal nor a mass-flux-optimal solution. A calculus of variations method applied to the non-linear model is shown to produce a non-linear hyperbolic split boundary value problem. A numerical approach, based on iterative gradient methods, is described and some numerical results are presented. Computer programmes for the numerical methods described in parts I and II are included as Appendices.Thu, 19 Nov 2015 09:02:28 GMThttp://hdl.handle.net/2381/349332015-11-19T09:02:28ZMarkov processes in adaptive control.
http://hdl.handle.net/2381/34932
Title: Markov processes in adaptive control.
Authors: Longley, D.
Abstract: The self-adaptive control system continually seeks to improve the performance of the process by making certain parameter adjustments. This improvement is achieved by "hill-climbing" techniques which test the effect of parameter adjustments on the performance and then make computed adjustments towards optimum conditions. The application of these techniques is complicated by the effects of the process dynamics and "noise" in performance index measurements. This thesis is concerned with the study of "hill-climbing" strategies that will minimise the effect of performance index noise. Markov process techniques were applied to a sempled data, unidimensional search over a parabolic curve and the effects of process dynamics were ignored. The result of incorporating a dead-zone filter in an optimising loop was analysed for a stepped-rectangular noise probability density function with a stationary and drifting optimum. A strategy which estimated the gradient by measuring the performance index difference over two successive values of the parameter (instead of perturbation techniques) was analysed but no conclusive results were obtained. Finally a supervisory loop, to adjust the gain of the optimising loop, was postulated and analysed. Digital and analogue computer studies were performed to compare the above strategies and to obtain an insight into the practical problems associated with the implementation of the optimising loop.Thu, 19 Nov 2015 09:02:27 GMThttp://hdl.handle.net/2381/349322015-11-19T09:02:27ZThe structure of binary molten salt mixtures: A neutron diffraction study.
http://hdl.handle.net/2381/34931
Title: The structure of binary molten salt mixtures: A neutron diffraction study.
Authors: Badyal, Yaspal Singh.
Abstract: Structural modification in a series of polyvalent metal chloride - alkali chloride binary molten salt mixtures has been investigated using the pulsed neutron diffraction technique. Structure factors have been measured for NiCl2- KCl, NiCl2-LiCl and ZnCl2-LiCl samples spanning the entire composition range. The key finding was that the degree of structural modification is dependent on the relative size and polarising power of the two cation species. The mixtures of NiCl2, and ZnCl2, with LiCl largely appear to be admixtures of the two pure salt structures, whereas adding KCl to NiCl2 results in a better ordered, more regularly tetrahedral local structure around the metal cation and enhancement of the first sharp diffraction peak (FSDP). A simple model involving charge ordering of discrete tetrahedral units by alkali counter-ions is proposed as an explanation for the enhanced intermediate range order. In order to identify some of the partial structure factor contributions to the enhanced FSDP, the scattering was measured for three isotopically-enriched NiCl2+2KCl samples. A complementary isotopic substitution experiment was performed on three ZnCl2+2KCl samples. The results generally confirm the findings of the composition study, with a strong similarity between the two molten salt systems also being evident. In addition, RMC modelling supports the proposed model for intermediate range order in the mixtures. Structure factors were also measured for AlCl3-LiCl and AlCl3-NaCl samples covering the entire composition range. Several features consistent with strong charge ordering of discrete tetrahedral units by alkali counter-ions were identified. In addition, RMC modelling of the data for pure AICl3 strongly challenges the 'established' view of the structure and an alternative 'sparse network liquid' model is proposed which emphasises the similarity to ZnCl2.Thu, 19 Nov 2015 09:02:25 GMThttp://hdl.handle.net/2381/349312015-11-19T09:02:25ZGenetic variation in the response of mice to xenobiotics, in vitro.
http://hdl.handle.net/2381/34930
Title: Genetic variation in the response of mice to xenobiotics, in vitro.
Authors: Arranz, Maria J.
Abstract: Adverse reactions to drugs and environmental chemicals are a serious problem with up to 30% of hospital patients experiencing such problems (Venning, 1983; Ludwig and Axelsen, 1983). There is evidence that many adverse reactions arise as a result of genetically controlled sensitivity (Festing, 1987). Large genetically determined differences in response to chemicals have also been recorded in laboratory animals. However, most toxicological screening involves a single strain and fails to detect genetically determined sensitivity. Should some animals show an adverse reaction, this is usually attributed to "biological variation". As the pedigree of such animals is not normally known at the time of use there is no way of showing whether these adverse reactions were inherited (Festing, 1975, 1979). The initial aim of this project was to develop a technique for studying genetic variation in sensitivity to treatment with drugs using in vitro screening methods. The techniques should not require hazardous or expensive chemicals and equipment, should require a small number of animals and should be reliable and easy to perform. Several end-points were studied, and a protocol for detecting genetic differences which included four end-points and two cell types was developed. In the second part of the project, the aim was to study genetic variation in sensitivity to Aspirin, Ethanol and Coumarin as model compounds, using the previously developed techniques in conjunction with suitable genetically-defined strains of mice. Two cell types (macrophages and hepatocytes) were studied and several end-points were used including neutral red uptake, total protein concentration, rate of phagocytosis and LDH activity in cells and supernatant. The study involved nine strains of mice. Although statistically significant differences among inbred strains were detected, in no experiment did strain distribution pattern suggest single-locus Mendelian control. There was no evidence that response to coumarin depended on the coumarin hydroxylase (Cyp2b) locus nor that response to alcohol depended on the alcohol dehydrogenase locus. It is concluded that further development would be necessary to develop these methods as a way of identifying genes associated with their type of genetic variation.Thu, 19 Nov 2015 09:02:23 GMThttp://hdl.handle.net/2381/349302015-11-19T09:02:23ZFast Data Processing in Hyper-Scale Systems
http://hdl.handle.net/2381/33565
Title: Fast Data Processing in Hyper-Scale Systems
Authors: Tilly, Marcel
Abstract: The deluge of intelligent objects that are providing continuous access
to data and services on one hand and the demand of developers and
consumers to handle these data on the other hand require us to think
about new communication paradigms and middleware.
Based on requirements collected from scenarios from connected car,
social networks, and factory of the future this thesis is developing new
concepts for fast data processing for hyper-scale systems. In hyperscale
systems, such as in the Internet of Things, one emerging requirement
is to process, procure, and provide information with almost zero
latency. This thesis is introducing new concepts for a middleware to
enable fast communication by limiting information flow with filtering
concepts using event policy obligations and combining data processing
techniques adopted from complex event processing.
Fast data processing has to deal with continuous data streams of
events, providing a set of operators to manipulate, aggregate, and
correlate data. This processing logic needs to be distributed. Distribution
helps us to scale on one hand in terms of numbers of data
sources (e.g. phones, cars, sensors) and on the other hand to parallelise
processing in terms of grouping and partitions (e.g. regional).
In our solution, event policies are injected as close as possible to the
place where the data is born to optimise traffic. Filters, aggregations
and rules help to process the data accordingly. Finally, communication
paradigms or interaction patterns support mediation between
classical service based request-response interaction and event-based
data exchange.
This all together builds a middleware enabling fast data processing
for hyper-scale systems.Mon, 16 Nov 2015 15:53:25 GMThttp://hdl.handle.net/2381/335652015-11-16T15:53:25ZHybridLF: a system for reasoning in higher-order abstract syntax
http://hdl.handle.net/2381/33362
Title: HybridLF: a system for reasoning in higher-order abstract syntax
Authors: Furniss, Amy Elizabeth
Abstract: In this thesis we describe two new systems for reasoning about deductive
systems: HybridLF and Canonical HybridLF.
HybridLF brings together the Hybrid approach (due to Ambler, Crole
and Momigliano [15]) to higher-order abstract syntax (HOAS) in Isabelle/HOL
with the logical framework LF, a dependently-typed system for proving theorems
about logical systems. Hybrid provides a version of HOAS in the form of
the lambda calculus, in which Isabelle functions are automatically converted
to a nameless de Bruijn represenation. Hybrid allows untyped expressions to
be entered as human-readable functions, which are then translated into the
machine-friendly de Bruijn form. HybridLF uses and updates these techniques
for variable representation in the context of the dependent type theory
LF, providing a version of HOAS in the form of LF.
Canonical HybridLF unites the variable representation techniques of
Hybrid with Canonical LF, in which all terms are in canonical form and definitional
equality is reduced to syntactic equality. We extend the Hybrid approach
to HOAS to functions with multiple variables by introducing a family
of abstraction functions, and use the Isabelle option type to denote errors instead
of including an ERR element in the Canonical HybridLF expression
type.
In both systems we employ the meta-logic M2 to prove theorems about
deductive systems. M2 [28] is a first-order logic in which quantifiers range
over the objects and types generated by an LF signature (that encodes a
deductive system). As part of the implementation of M2 we explore higher-order
unification in LF, adapting existing approaches to work in our setting.Thu, 22 Oct 2015 15:25:23 GMThttp://hdl.handle.net/2381/333622015-10-22T15:25:23ZA Calculus of Mobility and Communication for Ubiquitous Computing
http://hdl.handle.net/2381/32898
Title: A Calculus of Mobility and Communication for Ubiquitous Computing
Authors: Gul, Nosheen
Abstract: Ubiquitous computing makes various computing devices available throughout the
physical setting. Ubiquitous computing devices are distributed and could be mobile,
and interactions among them are concurrent and often depend on the location of
the devices. Process calculi are formal models of concurrent and mobile systems.
The work in this thesis is inspired by the calculus of Mobile Ambients and other
process calculi such as Calculus of Communicating Systems which have proved to
be successful in the modelling of mobility, communication and structure of systems.
We start by developing operational semantics for the calculus of Mobile Ambients
and Push and Pull Ambient Calculus, and prove that the semantics are sound and
complete with respect to the corresponding underlying reduction semantics. This
thesis proposes a Calculus of Communication and Mobility, denoted by CMCPCA,
for the modelling of mobility, communication and context awareness in the setting
of ubiquitous computing. CMCPCA is an ambient calculus with the in and out
capabilities of Cardelli and Gordon as well the push and pull capabilities of Phillips
and Vigliotti. CMCPCA has a new form of global communication similar to that in
Milner’s CCS. We define a new notion of behavioural equivalence for our calculus
in terms of an observation predicate and action transitions. Thus, we define barbed
bisimulation and congruence, and capability barbed bisimulation and congruence.
We then prove that capability barbed congruence coincides with barbed congruence.
We also include in the calculus a new form of context awareness mechanism that
allows ambients to query their current location and surrounding. We then propose
reduction semantics and operational semantics for the context awareness primitives,
and show that the semantics coincide. Several case studies and a variety of small
examples show the expressiveness and usefulness of our calculus.Wed, 05 Aug 2015 14:17:23 GMThttp://hdl.handle.net/2381/328982015-08-05T14:17:23ZGroups, formal language theory and decidability
http://hdl.handle.net/2381/32520
Title: Groups, formal language theory and decidability
Authors: Jones, Sam Anthony Mark
Abstract: The first four chapters provide an introduction, background information and a
summary of results from some of the relevant literature. In these chapters a proof
is provided if the author was unable to find either a proof or the result itself stated
in the literature.
Chapter 5 focuses on syntactic monoids of languages, it introduces some background
material from the literature and then proves some characterisations of
monoids based on properties that the full preimage of certain subsets satisfy when
considered as a formal language over the generating set.
In Chapter 6 we examine some natural properties of formal languages which are
necessary conditions for a formal language to be a word problem of a group.
We look at which subsets of these conditions are sufficient for a formal language
satisfying them to be a word problem.
Chapter 7 focuses on decision problems. We generalise a theorem of Hartmanis
and Hopcroft and use it to settle the decidability for various language classes of
the conditions from Chapter 6.
Chapter 8 contains a brief exposition of some related areas. We first characterise
the co-word problem for groups and then examine a way of constructing groups
by intersecting their word problems. We conclude this chapter by proving some
simple results about the context-free subset membership problem for groups.
Finally, Chapter 9 contains a brief discussion of possible directions in which one
could extend the work in this thesis. The results in chapters 5, 6 and 7 are to be considered original unless stated
otherwise. Many of the results in chapter 7 have been published in [24]. Many of
the results of chapter 6 have been submitted for publication.Wed, 08 Jul 2015 14:01:15 GMThttp://hdl.handle.net/2381/325202015-07-08T14:01:15ZNominal Lambda Calculus
http://hdl.handle.net/2381/31396
Title: Nominal Lambda Calculus
Authors: Nebel, Frank
Abstract: Since their introduction, nominal techniques have been widely applied in computer
science to reason about syntax of formal systems involving name-binding operators.
The work in this thesis is in the area of “nominal" type theory, or more precisely the
study of “nominal" simple types.
We take Nominal Equational Logic (NEL), which augments equational logic with
freshness judgements, as our starting point to introduce the Nominal Lambda Calculus
(NLC), a typed lambda calculus that provides a simple form of name-dependent
function types. This is a key feature of NLC, which allows us to encode freshness in
a novel way.
We establish meta-theoretic properties of NLC and introduce a sound model theoretic
semantics. Further, we introduce NLC[A], an extension of NLC that captures
name abstraction and concretion, and provide pure NLC[A] with a strongly
normalising and confluent βη-reduction system.
A property that has not yet been studied for “nominal" typed lambda calculi is
completeness of βη-conversion for a nominal analogue of full set-theoretic hierarchies.
Aiming towards such a result, we analyse known proof techniques and identify various
issues. As an interesting precursor, we introduce full nominal hierarchies and
demonstrate that completeness holds for βη-conversion of the ordinary typed lambda
calculus.
The notion of FM-categories was developed by Ranald Clouston to demonstrate
that FM-categories correspond precisely to NEL-theories. We augment FM-categories
with equivariant exponentials and show that they soundly model NLC-theories. We
then outline why NLC is not complete for such categories, and discuss in detail an
approach towards extending NLC which yields a promising framework from which we
aim to develop a future (sound and complete) categorical semantics and a categorical
type theory correspondence.
Moreover, in pursuit of a categorical conservative extension result, we study (enriched/
internal) Yoneda isomorphisms for “nominal" categories and some form of
“nominal" gluing.Thu, 08 Jan 2015 15:07:38 GMThttp://hdl.handle.net/2381/313962015-01-08T15:07:38ZCMMI-CM compliance checking of formal BPMN models using Maude
http://hdl.handle.net/2381/31390
Title: CMMI-CM compliance checking of formal BPMN models using Maude
Authors: El-Saber, Nissreen A. S.
Abstract: From the perspective of business process improvement models, a business process
which is compliant with best practices and standards (e.g. CMMI) is necessary for defining
almost all types of contracts and government collaborations. In this thesis, we propose
a formal pre-appraisal approach for Capability Maturity Model Integration (CMMI)
compliance checking based on a Maude-based formalization of business processes in
Business Process Model and Notation (BPMN). The approach can be used to assess
the designed business process compliance with CMMI requirements as a step leading
to a full appraisal application. In particular, The BPMN model is mapped into Maude,
and the CMMI compliance requirements are mapped into Linear Temporal Logic (LTL)
then the Maude representation of the model is model checked against the LTL properties
using the Maude’s LTL model checker.
On the process model side, BPMN models may include structural issues that hinder
their design. In this thesis, we propose a formal characterization and semantics specification
of well-formed BPMN processes using the formalization of rewriting logic (Maude)
with a focus on data-based decision gateways and data objects semantics. Our formal
specification adheres to the BPMN standards and enables model checking using Maude’s
LTL model checker. The proposed semantics is formally proved to be sound based on the
classical workflow model soundness definition. On the compliance requirements side,
CMMI configuration management process is used as a source of compliance requirements
which then are mapped through compliance patterns into LTL properties. Model
checking results of Maude based implementation are explained based on a compliance
grading scheme. Examples of CMMI configuration management processes are used to
illustrate the approach.Thu, 08 Jan 2015 12:29:00 GMThttp://hdl.handle.net/2381/313902015-01-08T12:29:00ZManagement concerns in service-driven applications
http://hdl.handle.net/2381/30107
Title: Management concerns in service-driven applications
Authors: Alghamdi, Ahmed Musfer
Abstract: With the abundance of functionally-similar Web-Services, the offered or agreed-on qualities are becoming decisive factors in attracting private as well as corporate customers to a given service, among all others. Nevertheless, the state-of-art in handling qualities, in this emerging service paradigm, remains largely bound to the aspects of technology and their standards (e.g. time-response, availability, throughputs). However, current approaches still ignore capital domain-based business qualities and management concerns (e.g. customer profiles, business deadlines). The main objective of this thesis is to leverage the handling of quality and management issues in service-driven business applications toward the intuitive business level supported by a precise and flexible conceptualisation. Thus, instead of addressing qualities using just rigid IT-SLA (service-level agreements) as followed by Web Services technology and standards, we propose to cope with more abstract and domain-dependent and adaptive qualities in an intuitive, yet conceptual, manner. The approach is centred on evolving business rules and policies for management, with a clean separation of functionalities as specific rules. At the conceptual level, we propose specialised architectural connectors called management laws that we also separate from coordination laws for functionality issues. We further propose a smooth and compliant mapping of the conceptualisation toward service technology, using existing rule-based standards.Mon, 15 Dec 2014 10:36:12 GMThttp://hdl.handle.net/2381/301072014-12-15T10:36:12ZFlexibo : language and its application to static analysis
http://hdl.handle.net/2381/30106
Title: Flexibo : language and its application to static analysis
Authors: Zhou, Jianguo
Abstract: This thesis introduces a new object-based language FlexibO to support prototype development paradigm and more importantly, program static analysis. FlexibO offers extreme flexibility and hence enables developers to write programs that contain rich information for further analysis and optimization. FlexibO interpreter's seamless integration with Java (including direct access to Java classes and methods and direct inheritance of Java classes) makes it a suitable tool for fast prototype software development. FlexibO's extreme flexibility allows developers to redefine the behavior of program evaluation by overriding its default evaluation method. This mechanism can be used to translate FlexibO to other efficient languages. In this thesis we design a translator in FlexibO to translate Bulk-Synchronous Parallel specifications (expressed in FlexibO) to executable C pro grams linked with BSPLib. Before translation, the tool first checks syntax and type, then statically analyzes potential communication conflicts, and finally generates C code. The translation process can accurately analyze primitive commands but require approximation (using abstract interpretation) for more advanced commands such as loops. The appropriateness of the translator and the associated static analysis can be formally analyzed using the technique of normal form.Mon, 15 Dec 2014 10:36:12 GMThttp://hdl.handle.net/2381/301062014-12-15T10:36:12ZAutomatic presentations of groups and semigroups
http://hdl.handle.net/2381/30105
Title: Automatic presentations of groups and semigroups
Authors: Oliver, Graham
Abstract: Effectively deciding the satisfiability of logical sentences over structures is an area well-studied in the case of finite structures. There has been growing work towards considering this question for infinite structures. In particular the theory of automatic structures, considered here, investigates structures representable by finite automata. The closure properties of finite automata lead naturally to algorithms for deciding satisfiability for some logics. The use of finite automata to investigate infinite structures has been inspired by the interplay between the theory of finite automata and the theory of semigroups. This inspiration has come in particular from the theory of automatic groups and semigroups, which considers (semi)groups with regular sets of normal forms over their generators such that generator-composition is also regular. The work presented here is a contribution to the foundational problem for automatic structures: given a class of structures, classify those members that have an automatic presentation. The classes considered here are various interesting subclasses of the class of finitely generated semigroups, as well as the class of Cayley Graphs of groups. Although similar, the theories of automatic (semi)groups and automatic presentation differ in their construction. A classification for finitely generated groups allows a direct comparison of the theory of automatic presentations with the theory of automatic groups.Mon, 15 Dec 2014 10:36:10 GMThttp://hdl.handle.net/2381/301052014-12-15T10:36:10ZOptimization problems in communication networks
http://hdl.handle.net/2381/30104
Title: Optimization problems in communication networks
Authors: Mihalak, Matus
Abstract: We study four problems arising in the area of communication networks. The minimum-weight dominating set problem in unit disk graphs asks, for a given set D of weighted unit disks, to find a minimum-weight subset D' âŠ† D such that the disks D' intersect all disks D. The problem is NP-hard and we present the first constant-factor approximation algorithm. Applying our techniques to other geometric graph problems, we can obtain better (or new) approximation algorithms. The network discovery problem asks for a minimum number of queries that discover all edges and non-edges of an unknown network (graph). A query at node v discovers a certain portion of the network. We study two different query models and show various results concerning the complexity, approximability and lower bounds on competitive ratios of online algorithms. The OVSF-code assignment problem deals with assigning communication codes (nodes) from a complete binary tree to users. Users ask for codes of a certain depth and the codes have to be assigned such that (i) no assigned code is an ancestor of another assigned code and (ii) the number of (previously) assigned codes that have to be reassigned (in order to satisfy (i)) is minimized. We present hardness results and several algorithms (optimal, approximation, online and fixed-parameter tractable). The joint base station scheduling problem asks for an assignment of users to base stations (points in the plane) and for an optimal colouring of the resulting conflict graph: user u with its assigned base station b is in conflict with user v, if a disk with center at 6, and u on its perimeter, contains v. We study the complexity, and present and analyse optimal, approximation and greedy algorithms for general and various special cases.Mon, 15 Dec 2014 10:36:09 GMThttp://hdl.handle.net/2381/301042014-12-15T10:36:09ZCategories of containers
http://hdl.handle.net/2381/30102
Title: Categories of containers
Authors: Abbott, Michael Gordon
Abstract: This thesis develops a new approach to the theory of datatypes based on separating data and storage resulting in a class of datatype called a container. The extension of a container is a functor which can be regarded as a generalised polynomial functor in type variables. A representation theorem allows every natural transformation between container functors to be represented as a unique pair of morphisms in a category.;Under suitable assumptions on the ambient category container functors are closed under composition, limits, coproducts and the construction of initial algebras and final coalgebras. These closure properties allow containers to provide a functorial semantics for an important class of polymorphic types including the strictly positive types.;Since polymorphic functions between functorial polymorphic types correspond to natural transformations, every polymorphic function can be represented as a container morphism; this simplifies reasoning about such functions and provides a framework for developing concepts of generic programming.;Intuitionistic well-founded trees or W-types are the initial algebras of container functors in one parameter; the construction of the initial algebra of a container in more than one parameter leads to the solution of a problem left incomplete by earlier work of Dybjer.;We also find that containers provide a suitable framework to define the derivative of a functor as a kind of linear exponential. We show that the use of containers is essential for this approach.;The theory is developed in the context of a fairly general category to allow for a wide choice of applications. We use the language of dependent type theory to develop the theory of containers in an arbitrary extensive locally cartesian closed category; much of the development in this thesis can also be generalised to display map categories. We develop the appropriate internal language and its interpretation in a category with families.Mon, 15 Dec 2014 10:36:09 GMThttp://hdl.handle.net/2381/301022014-12-15T10:36:09ZFormal languages and the irreducible word problem in groups
http://hdl.handle.net/2381/30103
Title: Formal languages and the irreducible word problem in groups
Authors: Fonseca, Ana
Abstract: There exist structural classifications of groups with a regular, one-counter or context-free word problem. Following on from this, the main object of the work presented here has been the irreducible word problem of a group, a notion introduced by Haring-Smith, who denned it as the subset of the word problem consisting of the non-empty words which have no non-empty proper subword equal to the identity. He proved that the groups with a finite irreducible word problem with respect to some group generating set are exactly the plain groups.;We know that the class of groups with a context-free irreducible word problem is a proper subclass of the virtually free groups. We look at direct products of finitely generated free groups by finite groups and also at the plain groups and consider their irreducible word problems with respect to minimal group generating sets. We prove that, of all the direct products of the infinite cyclic group by a non-trivial finite group, only Z x Z2 and Z x Z 3 have context-free irreducible word problem (and only with respect to a few group generating sets). We also exhibit a plain group that has context-free irreducible word problem with respect to every minimal group generating set.;Looking at the direct products of finitely generated free groups by non-trivial finite groups, we have found that the only irreducible word problem that is one-counter is that of Z x Z2 with respect to the canonical group generating set.;As for irreducible word problems lying in classes of languages above context-free, on one hand, we prove that having a recursive irreducible word problem is equivalent to having a recursive word problem. On the other hand, we prove that, while there are groups such that the fact that their irreducible word problem is recursively enumerable implies that they are recursive, that is not always the case.Mon, 15 Dec 2014 10:36:09 GMThttp://hdl.handle.net/2381/301032014-12-15T10:36:09ZAlternative approaches to optophonic mappings
http://hdl.handle.net/2381/30101
Title: Alternative approaches to optophonic mappings
Authors: Capp, Michael.
Abstract: This thesis presents a number of modifications to a blind aid, known as the video optophone, which enables a blind user to more readily interpret that local environment for enhanced mobility and navigation. Versions of this form of blind aid are generally both difficult to use and interpret, and are therefore inadequate for safe mobility. The reason for this severe problem lies in the complexity and excessive bandwidth of the optophonic output after the conversion from scene-to-sound.;The work herein describes a number of modifications that can be applied to the current optophonic process to make more efficient use of the limited bandwidth provided by the auditory system when converting scene images to sound. Various image processing and stereo techniques have been employed to artificially emulate the human visual system through the use of depth maps that successfully fade out the quantity of relatively unimportant image features, whilst emphasising the more significant regions such as nearby obstacles.;A series of experiments was designed to test these various modifications to the optophonic mapping by studying important factors of mobility and subject response whilst going about everyday life. The devised system, labelled DeLIA for the Detection, Location, Identification, and Avoidance (or Action) of obstacles, provided a means for gathering statistical data on users' interpretation of the optophonic output. An analysis of this data demonstrated a significant improvement when using the stereo cartooning technique, developed as part of this work, over the more conventional plain image as an input to an optophonic mapping from scene-to-sound.;Lastly, conclusions were drawn from the results, which indicated that the use of a stereo depth map as an input to a video optophone would improve its usefulness as an aid to general mobility. For the purposes of detecting and determining text or similar detail, either a plain unmodified image or some form of edge (depth) image were found to produce the best results.Mon, 15 Dec 2014 10:36:08 GMThttp://hdl.handle.net/2381/301012014-12-15T10:36:08ZMultimodal human-computer interaction for enhancing customers’ decision-making and experience on B2C e-commerce websites
http://hdl.handle.net/2381/29330
Title: Multimodal human-computer interaction for enhancing customers’ decision-making and experience on B2C e-commerce websites
Authors: Al Sokkar, Abdullah Ahmad Musa
Abstract: The main aim of this thesis was to identify, complement and refine the factors that contribute to users’ intention to purchase, satisfaction and attitude toward using a particular B2C online environment, as well as the causal relationships between these factors. A systematic literature review on Information System (IS), Market Research, and User Experience (UX), which has informed the design and development of a pilot study, has been conducted. Results have led to the conception of an online shopping decision-making (OSDM) model called ‘Episodic UX Model on Decision-Making’ (EUX-DM). It has been developed by integrating the established Technology Acceptance Model (TAM) as well as Information System Success Model (ISSM), and emerging UX models, and Expectation-Confirmation Theory (ECT). Results from analysing 305 responses to the web-based questionnaire aimed to evaluate EUX-DM verified its validity. In addition, after investigating the users’ preferences for the possible modifications related to the use of visual avatar in a particular B2C e-Commerce website for information presentation, another research focus has been placed on identifying the real conversational functions and their related communicational behaviour in designing male and female visual avatars’ facial expressions and body gestures. Following this, four different types of information presentations have been developed to be used in a contrived B2C online shopping environment, namely: (i) 2D static graphical and textual information, (ii) non-expressive avatars, (iii) avatars with facial expressions, (iv) and avatars with facial expressions and body gestures information presentations. Consequently, these information presentations were empirically investigated through two experimental studies. The outcomes of these studies indicated that the gender of the avatar and participants were found to be insignificant factors for any of the measured qualities, and the use of visual avatars with animated facial expressions and body gestures positively influenced customers’ usage attitude, intention to purchase and satisfaction.Tue, 09 Dec 2014 11:49:14 GMThttp://hdl.handle.net/2381/293302014-12-09T11:49:14ZOn the Synthesis of Choreographies
http://hdl.handle.net/2381/29310
Title: On the Synthesis of Choreographies
Authors: Lange, Julien
Abstract: The theories based on session types stand out as effective methodologies
to specify and verify properties of distributed systems. A key result in the area shows the
suitability of choreography languages and session types as a basis for a choreography-driven
methodology for distributed software development. The methodology it advocates
is as follows: a team of programmers designs a global view of the interactions to be
implemented (i.e., a choreography), then the choreography is projected onto each role.
Finally, each program implementing one or more roles in the choreography is validated
against its corresponding projection(s).
This is an ideal methodology but it may not always be possible to design one set of
choreographies that will drive the overall development of a distributed system. Indeed,
software needs maintenance, specifications may evolve (sometimes also during the development),
and issues may arise during the implementation phase. Therefore, there is a
need for an alternative approach whereby it is possible to infer a choreography from local
behavioural specifications (i.e., session types).
We tackle the problem of synthesising choreographies from local behavioural specifications
by introducing a type system which assigns – if possible – a choreography to
set of session types. We demonstrate the importance of obtaining a choreography from
local specifications through two applications. Firstly, we give three algorithms and a
methodology to help software designers refine a choreography into a global assertion,
i.e., a choreography decorated with logical formulae specifying senders’ obligations and
receivers’ requirements. Secondly, we introduce a formal model for distributed systems
where each participant advertises its requirements and obligations as behavioural contracts
(in the form of session types), and where multiparty sessions are started when a set
of contracts allows to synthesise a choreography.Thu, 04 Dec 2014 12:10:48 GMThttp://hdl.handle.net/2381/293102014-12-04T12:10:48ZA model for supporting electrical engineering with e-learning
http://hdl.handle.net/2381/29066
Title: A model for supporting electrical engineering with e-learning
Authors: Akaslan, Dursun
Abstract: The overall goal of this research work was developing and evaluating a model for supporting electrical engineering with e-learning. The model development was based on the survey data collected from representative teachers and students in Turkey whereas the model evaluation was conducted in the relevant HEIs in Turkey and the United Kingdom. To develop the model, the study investigated the attitudes of representative key stakeholders towards e-learning in Turkey by administrating questionnaires and interviews with teachers and students. Then the responses of the teachers and students were compared. Based on the results, I proposed a model with a multi-dimensional approach to e-learning: (1) self-directed learning by studying e-book, (2) self-assessment by solving e-exercises, (3) teacher-directed learning by attending classroom sessions as an integral part of the blended learning (4) teacher-assessment by solving e-exercises, (5) computer-directed learning by playing e-games and (6) computer-assessment by solving e-exercises.
To evaluate the applicability of the model in different conditions, a case-control study was conducted to determine whether the model had the intended effect on the participating students in HEIs in Turkey and the United Kingdom. As the result of the case-control study, the effects of e-learning, blended learning and traditional learning were verified. However, there were significant differences among the groups. The overall scores indicated that e-learning and blended learning was more effective as compared to the traditional learning. The results of our study indicated that the knowledge increase in e-learners seemed to be gradual because they tended to study daily by completing each activity on time. However, the traditional learners did not have the same pattern because they usually did not read the core text and did not solve e-exercise regularly before the classroom sessions. The results of pre-placement, post-placement tests and middle tests also justified these assumptions.Mon, 08 Sep 2014 14:27:39 GMThttp://hdl.handle.net/2381/290662014-09-08T14:27:39ZCompressed representation of XML documents with rapid navigation
http://hdl.handle.net/2381/29062
Title: Compressed representation of XML documents with rapid navigation
Authors: Kharabsheh, Mohammad Kamel Ahmad
Abstract: XML(Extensible Markup Language) is a language used in data representation and
storage, and transmission and manipulation of data. Excessive memory consumption
is an important challenge when representing XML documents in main memory.
Document Object Model (DOM) APIs are used in a processing level that provides
access to all parts of XML documents through the navigation operations. Although
DOM serves as a a general purpose tool that can be used in different applications,
it has high memory cost particularly if using na¨ıve. The space usage of DOM has
been reduced significantly while keeping fast processing speeds, by use of succinct
data structures in SiXDOM [1]. However, SiXDOM does not explore in depth XML
data compression principles to improve in-memory space usage. Such XML data
compression techniques have been proven to be very effective in on-disk compression
of XML document. In this thesis we propose a new approach to represent XML
documents in-memory using XML data compression ideas to further reduce space
usage while rapidly supporting operations of the kind supported by DOM.
Our approach is based upon a compression method [2] which represents an XML
document as a directed acyclic graph (DAG) by sharing common subtrees. However,
this approach does not permit the representation of attributes and textual data,
and furthermore, a naive implementation of this idea gives very poor space usage
relative to other space-efficient DOM implementations [1]. In order to realise the
potential of this compression method as an in-memory representation, a number
of optimisations are made by application of succinct data structures and variablelength
encoding. Furthermore, a framework for supporting attribute and textual
data nodes is introduced. Finally, we propose a novel approach to representing the
textual data using Minimal Perfect Hashing(MPH).
We have implemented our ideas in a software library called DAGDOMand performed
extensive experimental evaluation on a number of standard XML files. DAGDOM
yields a good result and we are able to obtain significant space reductions over existing
space-efficient DOM implementations (typically 2 to 5 times space reduction),
with very modest degradations in CPU time for navigational operations.Fri, 05 Sep 2014 15:30:29 GMThttp://hdl.handle.net/2381/290622014-09-05T15:30:29ZDesign-by-contract for software architectures
http://hdl.handle.net/2381/28924
Title: Design-by-contract for software architectures
Authors: Poyias, Kyriakos
Abstract: We propose a design by contract (DbC) approach to specify and maintain architectural
level properties of software. Such properties are typically relevant in the design
phase of the development cycle but may also impact the execution of systems. We give a
formal framework for specifying software architectures (and their refi nements) together
with contracts that architectural con figurations abide by. In our framework, we can
specify that if an architecture guarantees a given pre- condition and a refi nement rule
satisfi es a given contract, then the refi ned architecture will enjoy a given post-condition.
Methodologically, we take Architectural Design Rewriting (ADR) as our architectural
description language. ADR is a rule-based formal framework for modelling (the
evolution of) software architectures. We equip the recon figuration rules of an ADR
architecture with pre- and post-conditions expressed in a simple logic; a pre-condition
constrains the applicability of a rule while a post-condition specifi es the properties
expected of the resulting graphs. We give an algorithm to compute the weakest precondition
out of a rule and its post-condition. Furthermore, we propose a monitoring
mechanism for recording the evolution of systems after certain computations, maintaining
the history in a tree-like structure. The hierarchical nature of ADR allows us to
take full advantage of the tree-like structure of the monitoring mechanism. We exploit
this mechanism to formally defi ne new rewriting mechanisms for ADR reconfi guration
rules. Also, by monitoring the evolution we propose a way of identifying which part of
a system has been a ffected when unexpected run-time behaviours emerge. Moreover,
we propose a methodology that allows us to select which rules can be applied at the
architectural level to reconfigure a system so to regain its architectural style when it
becomes compromised by unexpected run-time recon figurations.Mon, 16 Jun 2014 15:40:37 GMThttp://hdl.handle.net/2381/289242014-06-16T15:40:37ZActivity awareness in context-aware systems using software sensors
http://hdl.handle.net/2381/28379
Title: Activity awareness in context-aware systems using software sensors
Authors: Pathan, Kamran Taj
Abstract: Context-aware systems being a component of ubiquitous or pervasive computing environment sense the users’ physical and virtual surrounding to adapt their behaviour accordingly. To achieve activity context tracking devices are common practice. Service Oriented Architecture is based on collections of services that communicate with each other. The communication between users and services involves data that can be used to sense the activity context of the user. SOAP is a simple protocol to let applications exchange their information over the web. Semantic Web provides standards to express the relationship between data to allow machines to process data more intelligently.
This work proposes an approach for supporting context-aware activity sensing using software sensors. The main challenges in the work are specifying context information in a machine processable form, developing a mechanism that can understand the data extracted from exchanges of services, utilising the data extracted from these services, and the architecture that supports sensing with software sensors. To address these issues, we have provided a bridge to combine the traditional web services with the semantic web technologies, a knowledge structure that supports the activity context information in the context-aware environments and mapping methods that extract the data out of exchanges occurring between user and services and map it into a context model. The Direct Match, the Synonym Match and the Hierarchical Match methods are developed to put the extracted data from services to the knowledge structure.
This research will open doors to further develop automated and dynamic context-aware systems that can exploit the software sensors to sense the activity of the user in the context-aware environments.Fri, 08 Nov 2013 15:49:07 GMThttp://hdl.handle.net/2381/283792013-11-08T15:49:07ZMaintaining Transactional Integrity in Long Running Workflow Services: A Policy-Driven Framework
http://hdl.handle.net/2381/28168
Title: Maintaining Transactional Integrity in Long Running Workflow Services: A Policy-Driven Framework
Authors: Ali, Manar Sayed Salamah
Abstract: Business to Business integration is enhanced by Workflow structures, which allow for aggregating web services as interconnected business tasks to achieve a business outcome. Business processes naturally involve long running activities, and require transactional behavior across them addressed through general management, failure handling and compensation mechanisms. Loose coupling and the asynchronous nature of Web Services make an LRT subject to a wider range of communication failures. Two basic requirements of transaction management models are reliability and consistency despite failures. This research presents a framework to provide autonomous handling of long running transactions, based on dependencies which are derived from the workflow. The framework presents a solution for forward recovery from errors and compensations automatically applied to executing instances of workflows. The failure handling mechanism is based on the propagation of failures through a recursive hierarchical structure of transaction components (nodes and execution paths). The management system of transactions (COMPMOD) is implemented as a reactive system controller, where system components change their states based on rules in response to triggering of execution events. One practical feature of the model is the distinction of vital and non-vital components, allowing the process designer to express the cruciality of activities in the workflow with respect to the business logic. A novel feature of this research is that the approach permits the workflow designer to specify additional compensation dependencies which will be enforced. A notable feature is the extensibility of the model that is eased by the simple and declarative based formalism. In our approach, the main concern is the provision of flexible and reliable underlying control flow mechanisms supported by management policies. The main idea for incorporating policies is to manage the static structure of the workflow, as well as handling arbitrary failure and compensation events. Thus, we introduce new techniques and architectures to support enterprise integration solutions that support the dynamics of business needs.Thu, 12 Sep 2013 10:44:21 GMThttp://hdl.handle.net/2381/281682013-09-12T10:44:21ZAlgorithms for Wireless Communication and Sensor Networks
http://hdl.handle.net/2381/28100
Title: Algorithms for Wireless Communication and Sensor Networks
Authors: Grant, Thomas
Abstract: In this thesis we will address four problems concerned with algorithmic issues that arise from communication and sensor networks.
The problem of scheduling wireless transmissions under SINR constraints has received much attention for unicast (one to one) transmissions. We consider the scheduling problem for multicast requests of one sender to many receivers, and present a logarithmic approximation algorithm and an online lower bound for arbitrary power assignments.
We study the problem of maximising the lifetime of a sensor network for fault-tolerant target coverage in a setting with composite events, where a composite event is the simultaneous occurrence of one or more atomic events. We are the first to study this variation of the problem from a theoretical perspective, where each event must be covered twice and there are several event types, and we present a (6 + ɛ)-approximation algorithm for the problem.
The online strongly connected dominating set problem concerns the construction of a dominating set that is strongly connected at all times, and for every vertex not in the dominating set, there exists an edge to some vertex in the dominating set, and an edge from a vertex in the dominating set. We present a lower bound for deterministic online algorithms and present an algorithm that achieves competitive ratio matching the lower bound.
The monotone barrier resilience problem is to determine how many sensors must be removed from a sensor network, such that a monotone path can exist between two points that does not intersect any sensor. We present a polynomial time algorithm that can determine the monotone barrier resilience for sensor networks of convex pseudo-disks of equal width.Thu, 29 Aug 2013 10:44:20 GMThttp://hdl.handle.net/2381/281002013-08-29T10:44:20ZAnt Colony Optimization in Stationary and Dynamic Environments
http://hdl.handle.net/2381/27971
Title: Ant Colony Optimization in Stationary and Dynamic Environments
Authors: Mavrovouniotis, Michalis
Abstract: The ant colony optimization (ACO) metaheuristic is inspired by the foraging behaviour of real ant colonies. Similarly with other metaheuristics, ACO suffers from stagnation behaviour, where all ants construct the same solution from early stages.
In result, the solution quality may be degraded because the population may get trapped on local optima. In this thesis, we propose a novel approach, called direct communication (DC) scheme, that helps ACO algorithms to escape from a local optimum if they get trapped. The experimental results on two routing problems showed that the DC scheme is effective.
Usually, researchers are focused on problems in which they have static environment.
In the last decade, there is a growing interest to apply nature-inspired metaheuristics in optimization problems with dynamic environments. Usually, dynamic optimization problems (DOPs) are addressed using evolutionary algorithms. In this thesis, we apply several novel ACO algorithms in two routing DOPs. The proposed ACO algorithms are integrated with immigrants schemes in which immigrant ants are generated, either randomly or with the use of knowledge from previous environment(s), and replace other ants in the current population. The experimental results showed that each proposed algorithm performs better in different dynamic cases, and that they have better performance than other peer ACO algorithms in general.
The existing benchmark generators for DOPs are developed for binary-encoded combinatorial problems. Since routing problems are usually permutation-encoded combinatorial problems, the dynamic environments used in the experiments are generated using a novel benchmark generator that converts a static problem instance to a dynamic one. The specific dynamic benchmark generator changes the fitness landscape of the problem, which causes the optimum to change in every environmental change. Furthermore in this thesis, another benchmark generator is proposed which moves the population to another location in the fitness landscape, instead of modifying it. In this way, the optimum is known and one can see how close to the optimum an algorithm performs during the environmental changes.Fri, 14 Jun 2013 09:45:27 GMThttp://hdl.handle.net/2381/279712013-06-14T09:45:27ZBroadcasting, Coverage, Energy Efficiency and Network Capacity in Wireless Networks
http://hdl.handle.net/2381/27808
Title: Broadcasting, Coverage, Energy Efficiency and Network Capacity in Wireless Networks
Authors: Henna, Shagufta
Abstract: Broadcasting, coverage, duty cycling, and capacity improvement are some of the important areas of interest in Wireless Networks. We address different problems related with broadcasting, duty cycling, and capacity improvement by sensing different network conditions and dynamically adapting to them. We propose two cross layer broadcasting protocols called CASBA and CMAB which dynamically adapt to network conditions of congestion and mobility. We also propose a broadcasting protocol called DASBA which dynamically adapts to local node density. CASBA, CMAB, and DASBA improve the reachability while minimizing the broadcast cost. Duty cycling is an efficient mechanism to conserve energy in Wireless Sensor Networks (WSNs). Existing duty cycling techniques are unable to handle the contention under dynamic traffic loads. Our proposed protocol called SA-RI-MAC handles traffic contention much more efficiently than RI-MAC without sacrificing the energy efficiency. It improves the delivery ratio with a significant reduction in the latency and energy consumption. Due to limited battery life and fault tolerance issues posed by WSNs, efficient methods which ensure reliable coverage are highly desirable. One solution is to use disjoint set covers to cover the targets. We formulate a problem called MDC which addresses the maximum coverage by using disjoint set covers S1 and S2. We prove that MDC is NP-complete and propose a √n-approximation algorithm for the MDC problem to cover n targets. The use of multi-channel MAC protocols improves the capacity of wireless networks. Efficient multi-channel MAC protocols aim to utilize multiple channels effectively. Our proposed multi-channel MAC protocol called LCV-MMAC effectively utilizes the multiple channels by handling the control channel saturation. LCV-MMAC demonstrates significantly better throughput and fairness compared to DCA, MMAC, and AMCP in different network scenarios.Wed, 13 Mar 2013 11:14:56 GMThttp://hdl.handle.net/2381/278082013-03-13T11:14:56ZZooming out of Membrane Graph Transformation Systems
http://hdl.handle.net/2381/27791
Title: Zooming out of Membrane Graph Transformation Systems
Authors: Bapodra, Mayur
Abstract: Living cells offer a rich variety of complex interactions and interesting structures to those wishing to model processes in systems biology. Of particular interest is the hierarchical nature of cell configurations, the compartmentalized reactions that can occur within individual cells, and the interaction between different levels of this hierarchy. Graph transformation systems are an intuitive and readable modelling paradigm that lends itself to representing such systems since graphs can be utilised to represent this rich structural information, while graph rewriting rules can concisely describe cell reactions. We formulate a generic graph transformation model that captures many functional properties of membrane (or P) systems that take inspiration from such cell biological processes. The main focus is then on abstraction of systems defined as instances of this metamodel, which we refer to as membrane graph transformation systems. Often, such systems are analysed by stochastic simulation, as this allows us to examine their overall, emergent behaviour, incorporating the effect that randomness may have on the results. Stochastic simulation can be resource intensive, limiting the applicability of many modelling languages to real biological systems. To improve performance and the scalability of modelling, we formalize a methodology that hides detail in the lowest level of the hierarchy, but retains any important information as attributes. We then train the parameter of the abstract model using Bayesian networks so that the local, per-rule behaviour of the original, concrete model is preserved. Consequently, trends in global properties are preserved, such as the way in which they change with respect to the stochastic parameters of certain rules. The methodology is demonstrated and evaluated against two case studies: a hypothetical immunological response and a peer-to-peer voice over IP network.Tue, 12 Mar 2013 11:26:40 GMThttp://hdl.handle.net/2381/277912013-03-12T11:26:40ZMatching of Service Feature Diagrams based on Linear Logic
http://hdl.handle.net/2381/27741
Title: Matching of Service Feature Diagrams based on Linear Logic
Authors: Naeem, Muhammad
Abstract: Managing variability is essential for an efficient implementation of end-user services that can be customised to individual needs. Apart from variations in selection and orchestration, also third-party services may have to be customisable. Although feature diagrams provide a high-level visual notation for variability, their use for specifying variability of services raises the problem of matching a required feature diagram against a set of provided ones.
In particular, the established interpretation of feature diagrams in Propositional Logic is not expressive enough for matching in the context of service variability. The problem becomes more visible when a certain requirement is going to be satisfied by a combination of multiple offers with overlapping features, which is a consequence of idempotence in Propositional Logic.
To address this problem, we propose service feature diagrams with semantics in Linear Logic. Linear Logic only allows the use of idempotence on the propositions with modalities. The permissible selection of features of a service feature diagram is called an instance diagram. We provide rules to obtain instance diagrams from the service feature diagram. The semantics of instance diagrams are also supported by Linear Logic.
This thesis not only introduces service feature diagrams, but also formalises their matching as linear deduction. We propose two categories of rules to verify diagrammatically if a collection of service descriptions satisfy the requirements. First, graphical matching rules are used to match service feature diagrams of requestor and provider. Second, graphical merging rules are used to merge multiple feature diagrams contributing to satisfy the requestor’s demands. We prove the correctness of these rules using the inference system of Linear Logic. We also provide the analysis of graphical rules and show that the application of the graphical rules is independent of the context in service feature diagram, i.e., graphical rule can be applied anywhere in a service feature diagram.Thu, 07 Feb 2013 10:46:02 GMThttp://hdl.handle.net/2381/277412013-02-07T10:46:02ZOnline Algorithms for Temperature Aware Job Scheduling Problems
http://hdl.handle.net/2381/27686
Title: Online Algorithms for Temperature Aware Job Scheduling Problems
Authors: Birks, Martin David
Abstract: Temperature is an important consideration when designing microprocessors. When exposed to high temperatures component reliability can be reduced, while some components completely fail over certain temperatures. We consider the design and analysis of online algorithms; in particular algorithms that use knowledge of the amount of heat a job will generate. We consider algorithms with two main objectives. The first is maximising job throughput. We show upper and lower bounds for the case where jobs are unit length, both when jobs are weighted and unweighted. Many of these bounds are matching for all cooling factors in the single and multiple machine case.
We extend this to consider the single machine case where jobs have longer than unit length. When all jobs are equal length we show matching bounds for the case without preemption. We also show that both models of pre-emption enable at most a slight reduction in the competitive ratio of algorithms. We then consider when jobs have variable lengths. We analyse both the models of unweighted jobs and the jobs with weights proportional to their length. We show bounds that match within constant factors, in the non-preemptive and both preemptive models.
The second objective we consider is minimising flow time. We consider the objective of minimising the total flow time of a schedule. We show NP-hardness and inapproximability results for the offline case, as well as giving an approximation algorithm for the case where all release times are equal. For the online case we give some negative results for the case where maximum job heats are bounded. We also give some results for a resource augmentation model that include a 1-competitive algorithm when the extra power for the online algorithm is high enough. Finally we consider the objective of minimising the maximum flow time of any job in a schedule.Thu, 17 Jan 2013 11:55:28 GMThttp://hdl.handle.net/2381/276862013-01-17T11:55:28ZPartner-Based Scheduling and Routing for Grid Workflows
http://hdl.handle.net/2381/27683
Title: Partner-Based Scheduling and Routing for Grid Workflows
Authors: Ashraf, Jawad
Abstract: The Grid has enabled the scientific community to make faster progress. Scientific experiments and data analyses once spanning several years can now be completed in a matter of hours. With the advancement of technology, the execution of scientific experiments, often represented as workflows, has become more demanding. Thus, there is a vital need for improvements in the scheduling of scientific workflows. Efficient execution of scientific workflows can be achieved by the timely allocation of the resources. Advance reservation can ensure the future availability of heterogeneous resources and help a scheduler to produce better schedules.
We propose a novel resource mapping technique for jobs of a Grid workflow in an advance reservation environment. Using a dynamic critical path based job selection method, our proposed technique considers the conditional mapping of parent and child jobs to the same resource, trying to minimise the communication duration between jobs and thus optimising the workflow completion time. The proposed method is analysed in both static and dynamic environments, and the simulation results show encouraging performance especially for workflows where the communication costs are higher than the computation costs.
We also propose a hybrid of multiple scheduling heuristics for the aforementioned problem, which chooses the best among multiple schedules computed by different algorithms. Simulation results show a significant improvement over well known scheduling heuristics in terms of workflow completion time.
Considering the advance reservation environment, a better schedule for the earliest completion of a workflow can be achieved if better paths can be found for the transfer of data files between jobs executed on different resources. We propose a K-shortest path based routing algorithm for finding good paths in the advance reservation environment. The results show that our proposed algorithm performs very well in terms of the earliest arrival time of the data.
Finally, we also study a modified partner based scheduling heuristic for non-advance reservation environments. The results demonstrate that our proposed algorithm is a promising candidate for adoption in such Grid environments.Wed, 16 Jan 2013 14:15:54 GMThttp://hdl.handle.net/2381/276832013-01-16T14:15:54ZMining Sequential Patterns from Probabilistic Data
http://hdl.handle.net/2381/27638
Title: Mining Sequential Patterns from Probabilistic Data
Authors: Muzammal, Muhammad
Abstract: Sequential Pattern Mining (SPM) is an important data mining problem. Although it is assumed in classical SPM that the data to be mined is deterministic, it is now recognized that data obtained from a wide variety of data sources is inherently noisy or uncertain, such as data from sensors or data being collected from the web from different (potentially conflicting) data sources. Probabilistic databases is a popular framework for modelling uncertainty. Recently, several data mining and ranking problems have been studied in probabilistic databases. To the best of our knowledge, this is the first systematic study of mining sequential patterns from probabilistic databases.
In this work, we consider the kind of uncertainties that could arise in SPM. We propose four novel uncertainty models for SPM, namely tuple-level uncertainty, event-level uncertainty, source-level uncertainty and source-level uncertainty in deduplication, all of which fit into the probabilistic databases framework, and motivate them using potential real-life scenarios. We then define the interestingness predicate for two measures of interestingness, namely expected support and probabilistic frequentness. Next, we consider the computational complexity of evaluating the interestingness predicate, for various combinations of uncertainty models and interestingness measures, and show that different combinations have very different outcomes from a complexity theoretic viewpoint: whilst some cases are computationally tractable, we show other cases to be computationally intractable.
We give a dynamic programming algorithm to compute the source support probability and hence the expected support of a sequence in a source-level uncertain database. We then propose optimizations to speedup the support computation task. Next, we propose probabilistic SPM algorithms based on the candidate generation and pattern growth frameworks for the source-level uncertainty model and the expected support measure. We implement these algorithms and give an empirical evaluation of the probabilistic SPM algorithms and show the scalability of these algorithms under different parameter settings using both real and synthetic datasets. Finally, we demonstrate the effectiveness of the probabilistic SPM framework at extracting meaningful patterns in the presence of noise.Thu, 20 Dec 2012 11:37:59 GMThttp://hdl.handle.net/2381/276382012-12-20T11:37:59ZModel-Based Testing Using Visual Contracts
http://hdl.handle.net/2381/27571
Title: Model-Based Testing Using Visual Contracts
Authors: Khan, Tamim Ahmed
Abstract: Web services only expose interface level information, abstracting away implementation details. Testing is a time consuming and resource-intensive activity. Therefore, it is important to minimize the set of test cases executed without compromising quality. Since white-box testing techniques and traditional structural coverage criteria require access to code, we require a model-based approach for web service testing. Testing relies on oracles to provide expected outcomes for test cases and, if implemented manually, they depend on testers’ understanding of functional requirements to decide the correct response of the system on every given test case. As a result, they are costly in creation and maintenance and their quality depends on the correct interpretation of the requirements. Alternatively, if suitable specifications are available, oracles can be generated automatically at lower cost and with better quality. We propose to specify service operations as visual contracts with executable formal specifications as rules of a typed attributed graph transformation system. We associate operation signatures with these rules for providing test oracles.
We analyze dependencies and conflicts between visual contracts to develop a dependency graph. We propose model-based coverage criteria, considering this dependency graph, to assess the completeness of test suites. We also propose a mechanism to find out which of the potential dependencies and the conflicts were exercised by a given test case. While executing the tests, the model is simulated and coverage is recorded as well as measured against the criteria. The criteria are formalized and the dynamic detection of conflicts and dependencies is developed. This requires keeping track of occurrences and overlaps of pre- and post-conditions, their enabling and disabling, in successive model states, and interpreting these in terms of the static dependency graph.
Systems evolve over time and need retesting each time there is a change. In order to verify that the quality of the system is maintained, we use regression testing. Since regression test suites tend to be large, we isolate the affected part in the system only retesting affected parts by rerunning a selected subset of the total test suite. We analyze the test cases that were executed on both versions and propose a mechanism to transfer the coverage provided by these test cases. This information helps us to assess the completeness of the test suite on the new version without executing all of it.Fri, 02 Nov 2012 12:37:51 GMThttp://hdl.handle.net/2381/275712012-11-02T12:37:51ZSearch-Based and Goal-Oriented Refactoring Using Unfolding of Graph Transformation Systems
http://hdl.handle.net/2381/10999
Title: Search-Based and Goal-Oriented Refactoring Using Unfolding of Graph Transformation Systems
Authors: Qayum, Fawad
Abstract: To improve automation and traceability of search-based refactoring, in this thesis we propose a formulation of using graph transformation, where graphs represent object-oriented software architectures at the class level and rules describe refactoring operations. This formalisation allows us to make use of partial order semantics and an associated analysis technique, the approximated unfolding of graph transformation systems. In the unfolding we can identify dependencies and conflicts between refactoring steps leading to an implicit and therefore more scalable representation of the search space by sets of transformation steps equipped with relations of causality and conflict.
To implement search based refactoring we make use of the approximated unfolding of graph transformation systems. An optimisation algorithm based on the Ant Colony paradigm is used to explore the search space, aiming to find a sequence of refactoring steps that leads to the best design at a minimal cost.
Alternatively, we propose a more targeted approach, aiming at the removal of design flaws. The idea is that such sequences should be relevant to the removal of the flaw identified, i.e., contain only steps which are directly or indirectly contributes to the desired goal.Thu, 06 Sep 2012 13:17:42 GMThttp://hdl.handle.net/2381/109992012-09-06T13:17:42ZGenetic Algorithms for University Course Timetabling Problems
http://hdl.handle.net/2381/10997
Title: Genetic Algorithms for University Course Timetabling Problems
Authors: Naseem Jat, Sadaf
Abstract: The university course timetabling problem is a difficult optimisation problem due to its highly-constrained nature. Finding an optimal, or even a high quality, timetable is a challenging task, especially when resources (e.g., rooms and time slots) are limited. In the literature, many approaches have been studied to solve this problem. In this thesis, we investigate genetic algorithms to solve the problem because they have been successfully used for a wide range of real-world problems. However, for university course timetabling problems, traditional genetic algorithms are not usually considered as efficient solvers.
In this thesis, we investigate genetic algorithms to acquire good solutions for university course timetabling problems. Several ideas are introduced to increase the general performance of genetic algorithms on these problems. Local search strategies are introduced into the traditional genetic algorithm to enhance its performance for the university course timetabling problem. This differs from many works in the literature because it works on time slots of the timetable rather than events directly.
A guided search approach is also introduced into genetic algorithms to produce high quality individuals into the population. In the guided search technique, the best parts of selected individuals from the current population are stored in an extra memory (or data structure) and are re-used to guide the generation of new individuals for subsequent populations.
In addition to solving university course timetabling problems as a single-objective optimisation problem, we also tackle the multi-objective university course timetabling problem. We integrate the above proposed approaches into multi-objective evolutionary algorithms and propose a framework of multi-objective evolutionary algorithms based on local search and guided search strategies for the multi-objective university course timetabling problem. This framework is then instantiated into a set of multi-objective evolutionary algorithms for the multi-objective university course timetabling problem based on a set of multi-objective evolutionary algorithms that are typically used for general multi-objective optimisation problems.
Computational results based on a set of well-known university course timetabling benchmark instances, show the effectiveness of the proposed approaches for both single- and multi-objective university course timetabling problems.Thu, 06 Sep 2012 12:41:18 GMThttp://hdl.handle.net/2381/109972012-09-06T12:41:18ZStructural Domain Modelling for Policy Language Specialization with Conflict Analysis
http://hdl.handle.net/2381/10994
Title: Structural Domain Modelling for Policy Language Specialization with Conflict Analysis
Authors: Khowaja, Zohra Ahsan
Abstract: Policies are descriptive and provide information which can be used to modify the behaviour of a system without the need of recompilation and redeployment. They are usually written in a policy definition language which allows end users to specify their requirements, preferences and constraints. Policies are used in many software application areas: network management, telecommunications, security, and access control are some typical examples. Ponder, KAoS, Rein, XACML, and WSPL are examples of policy definition languages. These languages are usually targeted at a specific domain, hence there is a plethora of languages. APPEL (the Adaptable Programmable Policy Environment Language) [69] has followed a different approach: It is a generic policy description language conceived with a clear separation between core language and its specialization for concrete domains.
So far, there has not been any formal method for the extension and domain specialization of the APPEL policy language.
Policy conflict can occur when a new or a modified policy is deployed in a policy server, which leads to unspecified behaviour. To make policy based systems conflict free it is necessary to detect and resolve conflicts before they occur, otherwise the intended behaviour of a policy cannot be guaranteed.
We introduce a structural modelling approach to specialize the policy language for different domains, implemented in the VIATRA2 graph transformation tool. This approach is applied to APPEL. Our method for conflict analysis is based on the modelling methodology. As conflicts depend on domain knowledge, it is sensible to use this knowledge for conflict analysis. The identified conflicting actions are then encoded in the ALLOY model checker that confirm the existence of actual and potential conflicts.Thu, 06 Sep 2012 11:47:41 GMThttp://hdl.handle.net/2381/109942012-09-06T11:47:41ZVOML: Virtual Organization Modelling Language
http://hdl.handle.net/2381/10942
Title: VOML: Virtual Organization Modelling Language
Authors: Rajper, Noor Jehan
Abstract: Virtual organizations (VOs) and their breeding environments are an emerging approach for developing systems as a consortium of autonomous entities formed to share costs and resources, better respond to opportunities, achieve shorter time-to-market and exploit fast changing market opportunities. VOs cater for those demands by incorporating reconfigurations making VOs highly resilient and agile by design. Reconfiguration of systems is an active research area. Many policy and specification languages have been dedicated for the purpose. However, all these approaches consider reconfiguration of a system as somewhat isolated from its business and operational model; it is usually assumed that the latter two remain unaffected through such reconfigurations and the reconfiguration is usually limited to dynamic binding of components the system consists of. However the demands of VO reconfiguration go beyond dynamic binding and reach the level where it becomes crucial to keep changing the organizational structure (process model) of the system as well, which leads to changes of the operational/functional model. This continuous reconfiguration of the operational model emphasizes the need of a modelling language that allows specification and validation of such systems.
This thesis approaches the problem of formal specification of VOs through the Virtual Organization Modelling Language (VOML) framework. The core of this framework are three languages each capturing a specific aspect. The first language named Virtual Organization Structural modelling language (VO-S), focuses on structural aspects and many of the characteristics particular to VOs such as relationship between the members expressed in domain terminology. The second language named VO Reconfiguration (VO-R for short), permits different reconfigurations on the structure of the VO. This language is an extension of APPEL for the domain of VOs. The third language named VO Operational modelling language (VO-O) describes the operational model of a VO in more details.
This language is an adaptation and extension of the Sensoria Reference Modelling
Language for service oriented architecture (SRML).
Our framework models VOs using the VO-S and the VO-R which are at a high level of abstraction and independent of a specific computational model. Mapping rules provide guidelines to generate operational models, thus ensuring that the two models conform to each other.
The usability and applicability of VOML is validated through two cases studies one of which offers travel itineraries as a VO service and is a running example.
The other case study is an adaptation of a case study on developing a chemical plant from [14].Thu, 16 Aug 2012 10:24:00 GMThttp://hdl.handle.net/2381/109422012-08-16T10:24:00ZApproximating Node-Weighted Steiner Subgraphs for Multicast Communication in Wireless Networks
http://hdl.handle.net/2381/10837
Title: Approximating Node-Weighted Steiner Subgraphs for Multicast Communication in Wireless Networks
Authors: Shahnaz, Ambreen
Abstract: We are motivated by the problem of computing multicast routing structures in wireless ad-hoc networks modelled by special classes of graphs including unit disk graphs, quasi-unit disk graphs and (λ + 1)-claw-free graphs. Multicast communication can be established by a tree known as Steiner tree. Wireless ad-hoc networks must operate using limited resources, therefore, the suitability of nodes for inclusion in a Steiner tree can vary widely between different nodes. We model this by assuming that each node of the network is assigned a weight that represents the cost of including it in the Steiner tree. Our goal is to compute a Steiner tree with minimum total node weight. However, in scenarios where nodes and links are not reliable, a tree has the drawback that it can be disconnected by the failure of even a single link or node in the network. Therefore, we also consider various fault-tolerant routing structures called 2-edge-connected Steiner subgraphs, k-edge-connected Steiner subgraphs, 2-vertex-connected Steiner subgraphs, and 2-edge-connected group Steiner subgraphs. The problems we consider are NP-hard, so we are interested in algorithms that compute provably good approximate solutions in polynomial time. We present a generalization of Steiner subgraph problems referred to as the node-weighted δ-Steiner subgraph problem, where δ represents connectivity requirements. We present an algorithm with approximation ratio 0.5dρ for the node-weighted δ-Steiner subgraph problem, where d is the bounded maximum degree of the solution subgraph, and ρ is the approximation ratio of the edge-weighted version of the δ-Steiner subgraph problem. We then shown how to construct solution subgraphs of bounded maximum degree d in several graph classes for our problem variants. As a result, we obtain algorithms for the problems we consider, on graph classes that admit subgraphs of small degree, whose approximation ratios are better than the best known ratios for the same problems on general graphs.Tue, 12 Jun 2012 15:23:31 GMThttp://hdl.handle.net/2381/108372012-06-12T15:23:31ZModular Performance Modelling of Mobile Applications using Graph Transformation
http://hdl.handle.net/2381/10831
Title: Modular Performance Modelling of Mobile Applications using Graph Transformation
Authors: Arijo, Niaz Hussain
Abstract: Graph transformation provides a visual and formal notation for modelling systems of dynamic nature. We use graph transformation for modelling mobility and performance, and provide a methodology for modular system modelling to handle scalbility issues of large systems. In our methodology we have distinguished three approaches for system modelling, monolithic, topdown and bottom-up. In the monolithic approach, a system is modelled as a global or whole-world system. In the top-down approach, a global system is projected to its views based on their local type graphs. In the bottom-up approach, a system is modelled as a set of subsystems with shared interface. A whole system is composed from its subsystems.
We generate labelled transition systems (LTSs) from graph transformation systems/views in GROOVE and transform them into Continuous Time Markov Chains (CTMCs). These CTMCs are further translated into the Performance Evalution Process Algebra (PEPA) or PRISM. In PEPA and PRISM subsystems are synchronized over shared labels to compose a global system. We demonstrate that the composed model is bisimilar to its original global model. In addition stochastic analysis of models are also carried out in PEPA or PRISM for performance checking.
We have given tool support for view generation from a global graph transformation system in GROOVE and transforming LTSs generated from graph transformation systems, into CTMCs, and CTMCs into PEPA or PRISM models.Tue, 12 Jun 2012 12:25:35 GMThttp://hdl.handle.net/2381/108312012-06-12T12:25:35ZSequence Based Memetic Algorithms for Static and Dynamic Travelling Salesman Problems
http://hdl.handle.net/2381/10809
Title: Sequence Based Memetic Algorithms for Static and Dynamic Travelling Salesman Problems
Authors: Arshad, Shakeel
Abstract: Hybridization of genetic algorithms (GAs) with local search techniques has received significant attention in recent years and is being widely used to solve real-world problems. These hybrid GAs, also called memetic algorithms (MAs), are able to incorporate other powerful techniques within the framework of GAs, working as a single unit and counterbalancing each other’s disadvantages.
In this thesis, we propose a hybrid GA, called Sequence Based Memetic Algorithm
(SBMA) with Inver Over (IO), for solving the travelling salesman problem (TSP). This is a 2-phase MA. The first phase (SBMA) consists of traditional binary operators, and the second phase is based on a unary operator. In SBMA, a tour is split into equal sub-tours. Further, the shortest tour is selected among the sub-tours and then optimized locally. The sub-tours are stored in the memory and then used to guide the evolutionary process via a kind of embedded local search. Additionally, we apply some techniques to adapt the key parameters based on whether the best individual within the population improves or not while also maintaining the diversity. After the first phase, the hybrid algorithm enters the second phase which is the Inver Over with elite population. Here, the IO is directed to get a clue from the elite population by adding and preserving good edges.
We have also shown that the above approach can be extended to handle the dynamic TSP. The framework of our hybrid approach, along with the integration of the nearest neighbour list, applying 2-Opt local search on sub-tours and adaptive parameter control in the first phase, and the elite population with the rotating gene pool strategies in the second phase, works well for the DTSP. In order to test the performance of the proposed approach for the DTSP, experiments were carried out based on different DTSP test beds. From the study, it has been observed that the integrated heuristics or meta-heuristics are able to produce good-quality solutions for the DTSP. We also analysed the effect of the gene pool and immigrants generated with the nearest neighbour algorithm, which works well with all DTSP test instances, under different dynamics.Thu, 07 Jun 2012 12:10:43 GMThttp://hdl.handle.net/2381/108092012-06-07T12:10:43ZStochastic Simulation of P2P VoIP Network Reconfiguration Using Graph Transformation
http://hdl.handle.net/2381/10428
Title: Stochastic Simulation of P2P VoIP Network Reconfiguration Using Graph Transformation
Authors: Khan, Ajab
Abstract: Peer-to-Peer (P2P) networks provide an alternative approach to distributed systems, relaxing the requirements for dedicated servers from the client-server model. A P2P network operates as an overlay at application layer, on top of the physical network. In the early years of P2P, most applications lacked mechanisms for enforcing a particular overlay topology. This resulted in inefficient communication schemes, such as flooding or the maintenance of large numbers of connections with other peers. However, researchers and practitioners have realized the importance of constructing and maintaining appropriate overlay topologies for efficient and robust P2P systems.
P2P-based Voice over IP (VoIP) networks, such as Skype, distinguish client peers from super peers. This results in a two-level hierarchy: Peers with powerful CPU, more free memory and greater bandwidth take on server-like responsibilities and provide services to a set of client peers. But building and maintaining a super peer-based overlay topology is not easy. In particular, the uncontrollable and unpredictable behaviour of peers results in volatile overlay topologies. This makes it challenging to design reconfigurable and stable networks that provide good Quality of Service (QoS). Various solutions have been proposed. However, peer dynamics, scale and complexity make it hard and expensive to validate them by testing. Simulation can help to validate network designs and protocols, but most existing approaches cannot cope with unbounded dynamic change of network topology.
We propose a new approach to the modelling and simulation of P2P network reconfigurations using graph transformation, a visual rule based formalism. Based on existing alternatives we classify network design variations by means of a feature tree. Focussing on P2P VoIP applications, we develop a structural model and transformation rules to compare alternative solutions to the problems of selection and connection to super peers, peer promotion, and load balancing, evaluating their QoS properties. We validate the model using statistics from the real Skype network and experimental data in the literature.Fri, 18 May 2012 11:06:39 GMThttp://hdl.handle.net/2381/104282012-05-18T11:06:39ZAdaptive Mutation Operators for Evolutionary Algorithms
http://hdl.handle.net/2381/10315
Title: Adaptive Mutation Operators for Evolutionary Algorithms
Authors: Korejo, Imtiaz Ali
Abstract: Evolutionary algorithms (EAs) are a class of stochastic search and optimization algorithms
that are inspired by principles of natural and biological evolution. Although
EAs have been found to be extremely useful in finding solutions to practically intractable
problems, they suffer from issues like premature convergence, getting stuck
to local optima, and poor stability. Recently, researchers have been considering
adaptive EAs to address the aforementioned problems. The core of adaptive EAs is
to automatically adjust genetic operators and relevant parameters in order to speed
up the convergence process as well as maintaining the population diversity.
In this thesis, we investigate adaptive EAs for optimization problems. We study
adaptive mutation operators at both population level and gene level for genetic
algorithms (GAs), which are a major sub-class of EAs, and investigate their performance
based on a number of benchmark optimization problems. An enhancement
to standard mutation in GAs, called directed mutation (DM), is investigated in
this thesis. The idea is to obtain the statistical information about the fitness of
individuals and their distribution within certain regions in the search space. This
information is used to move the individuals within the search space using DM. Experimental
results show that the DM scheme improves the performance of GAs on
various benchmark problems.
Furthermore, a multi-population with adaptive mutation approach is proposed to
enhance the performance of GAs for multi-modal optimization problems. The main
idea is to maintain multi-populations on different peaks to locate multiple optima for
multi-modal optimization problems. For each sub-population, an adaptive mutation
scheme is considered to avoid the premature convergence as well as accelerating the
GA toward promising areas in the search space. Experimental results show that the
proposed multi-population with adaptive mutation approach is effective in helping
GAs to locate multiple optima for multi-modal optimization problems.Mon, 02 Apr 2012 10:42:21 GMThttp://hdl.handle.net/2381/103152012-04-02T10:42:21ZParticle Swarm Optimization in Stationary and Dynamic Environments
http://hdl.handle.net/2381/10284
Title: Particle Swarm Optimization in Stationary and Dynamic Environments
Authors: Li, Changhe
Abstract: Inspired by social behavior of bird flocking or fish schooling, Eberhartand Kennedy first developed the particle swarm optimization (PSO) algorithm in 1995. PSO, as a branch of evolutionary computation, has been successfully applied in many research and application areas in the past several years, e.g., global optimization, artificial neural network training, and fuzzy system control, etc… Especially, for global optimization, PSO has shown its superior advantages and effectiveness.
Although PSO is an effective tool for global optimization problems, it shows weakness while solving complex problems (e.g., shifted, rotated, and compositional problems) or dynamic problems (e.g., the moving peak problem and the DF1 function). This is especially true for the original PSO algorithm.
In order to improve the performance of PSO to solve complex problems, we present a novel algorithm, called self-learning PSO (SLPSO). In SLPSO, each particle has four different learning strategies to deal with different situations in the search space. The cooperation of the four learning strategies is implemented by an adaptive framework at the individual level, which can enable each particle to choose the optimal learning strategy according to the properties of its own local fitness landscape. This flexible learning mechanism is able to automatically balance the behavior of exploration and exploitation for each particle in the entire search space during the whole running process.
Another major contribution of this work is to adapt PSO to dynamic environments, we propose an idea that applies hierarchical clustering techniques to generate multiple populations. This idea is the first attempt to solve some open issues when using multiple population methods in dynamic environments, such as, how to define the size of search region of a sub-population, how many individuals are needed in each sub-population, and how many sub-populations are needed, etc... Experimental study has shown that this idea is effective to locate and track multiple peaks in dynamic environments.Tue, 27 Mar 2012 11:54:34 GMThttp://hdl.handle.net/2381/102842012-03-27T11:54:34ZInvestigations into Algebra and Topology over Nominal Sets
http://hdl.handle.net/2381/10187
Title: Investigations into Algebra and Topology over Nominal Sets
Authors: Petrisan, Daniela Luana
Abstract: The last decade has seen a surge of interest in nominal sets and their applications to formal methods for programming languages. This thesis studies two subjects: algebra and duality in the nominal setting.
In the first part, we study universal algebra over nominal sets. At the heart of our approach lies the existence of an adjunction of descent type between nominal sets and a category of many-sorted sets. Hence nominal sets are a full reflective subcategory of a many-sorted variety. This is presented in Chapter 2.
Chapter 3 introduces functors over many-sorted varieties that can be presented by operations and equations. These are precisely the functors that preserve sifted colimits.
They play a central role in Chapter 4, which shows how one can systematically transfer results of universal algebra from a many-sorted variety to nominal sets. However, the equational logic obtained is more expressive than the nominal equational logic of Clouston and Pitts, respectively, the nominal algebra of Gabbay and Mathijssen. A uniform fragment of our logic with the same expressivity as nominal algebra is given.
In the second part, we give an account of duality theory in the nominal setting. Chapter 5 shows that Stone’s representation theorem cannot be internalized in nominal sets. This is due to the fact that the adjunction between nominal Boolean algebras and nominal sets is no longer of descent type. We prove a duality theorem for nominal distributive lattices with a restriction operation in terms of nominal bitopological spaces. This duality restricts to duality between nominal Boolean algebras and a category of nominal topological spaces. Our notion of compactness allows for generalisation of Manes’ theorem to the nominal setting.Wed, 14 Mar 2012 10:13:10 GMThttp://hdl.handle.net/2381/101872012-03-14T10:13:10ZDirected Symbolic Model Checking of Security Protocols
http://hdl.handle.net/2381/10181
Title: Directed Symbolic Model Checking of Security Protocols
Authors: Nizamani, Qurat Ul Ain
Abstract: This thesis promotes the use of directed model checking for security protocol verification. In particular, we investigated the possibility of designing heuristics that can reduce the overall size of the state space and can direct the search towards states containing an attack. More precisely,
• We have designed three property-specific heuristics namely H1, H2, and H3. The heuristics derive their hints from the security property to be verified and assign weights to states according to their possibility of leading to an attack.
• H1 is formally proved correct, i.e., the states pruned by the heuristic H1 do not contain any attack.
• An existing tool ASPASyA with conventional model checking algorithm (i.e., depth first search) has been modified so as to integrate our heuristics into it. The resulting tool H -ASPASyA uses an informed search algorithm that is equipped with our heuristics. The heuristics evaluate the states which are then explored in decreasing order of their weights.
• The new tool H -ASPASyA is tested against a few protocols to gauge the performance of our heuristics.
The results demonstrate the efficiency of our approach. It is worth mentioning that despite being a widely applied verification technique, model checking suffers from the state space explosion problem. Recently directed model checking has been used to mitigate the state space explosion problem in general model checking. However, the directed model checking approaches have not been studied extensively for security protocol verification. This thesis demonstrates the fact that directed model checking can be adapted for security protocol verification in order to yield better results.Tue, 13 Mar 2012 12:22:39 GMThttp://hdl.handle.net/2381/101812012-03-13T12:22:39ZModelling Architectures of Federated Identity Management Systems
http://hdl.handle.net/2381/10180
Title: Modelling Architectures of Federated Identity Management Systems
Authors: Nizamani, Hyder Ali
Abstract: Today’s dynamic and scalable collaborative systems demand not only to deal with functional but also some non-functional (e.g., security) requirements. For a secure inter-organisational collaboration scenario, Federated Identity Management systems (FIMs) provide a suitable mechanism to deal with access control. FIMs enable users of an organisation to access resources (or services) of the other trusted organisations in a secure and seamless way. More precisely, FIMs allow cross-domain user authentication to enable access control across organisations under the concept known as Circle of Trust (CoT). Patterns of FIMs emerged as recurring CoT scenarios due to the fact that each of these patterns has different security requirements. More importantly, organisations may join up or leave the CoT during the development life-cycle. Such a change in a FIM system may have an impact on its security requirements. Therefore, it is important to formally describe architectural and reconfiguration aspects of FIMs by considering their patterns.
To this purpose, we propose
• two UML models for FIMs where one model uses the standard UML notations to describe architectural aspects of FIMs while the other uses the UML profile in [33] to describe those aspects of FIMs together with their reconfigurations
• a formal model for FIMs in ADR (Architectural Design Rewriting) to characterise their patterns by describing an architectural style together with style-preserving reconfigurations.
We also study the adequacy of UML to describe architectural aspects of systems and compare it with ADR. Our comparison develops through the modelling of architectural and reconfiguration aspects of FIMs. In ADR, these aspects of FIMs are suitably represented through style-consistent (graphical) designs in terms of ADR productions. On the other hand, UML has limitations in expressing constraints over complex associations; also, UML seems to provide unsatisfactory support for presenting architectural styles in a general way. Overall, our investigation shows that UML has some drawbacks due to the complexity of diagrams, their proliferation, and the lack of a precise semantics that consistently relates them. ADR gives precise and simpler specifications for architectural design.Tue, 13 Mar 2012 12:08:18 GMThttp://hdl.handle.net/2381/101802012-03-13T12:08:18ZReengineering Software to Three-tier Applications and Services
http://hdl.handle.net/2381/10179
Title: Reengineering Software to Three-tier Applications and Services
Authors: Matos, Carlos Manuel Pinto de
Abstract: Driven by the need of a very demanding world, new technology arises as a way to solve problems found in practice. In the context of software, this occurs in the form of new programming paradigms, new application design methodologies, new tool support and new architectural patterns.
Newly developed systems can take advantage of recent advances and choose from a state-of-the-art portfolio of techniques, taking stock of an understanding built across the years, learning from past, good and bad, experiences. However, existing software was built in a completely different context.
Software engineering advances occur at a very fast pace, and applications are quickly seen as legacy due to a number of reasons, including difficulties to adapt to business needs, lack of integration capabilities with other systems, or general maintenance issues.
There are various approaches to address these problems depending on the requirements or major concerns. The solution can either be rewriting the applications from scratch or evolving the existing systems.
This thesis presents a methodology for systematically addressing the evolution of existing application into more modern architectures, including proposing implementations to address several classes of modernisation, with particular emphasis in reengineering towards tiered architectures and service-oriented architectures.
The methodology is based on a combination of source code pattern detection guiding the extraction of structural graph models, rule-based transformations of these models, and the generation and execution of code-level refactoring scripts to affect the actual changes to the software.
This dissertation presents the process, methodology, and tool support. Additionally, the proposed techniques are evaluated in the context of case studies, in order to allow conclusions regarding applicability, scalability, and overall benefits, both in terms of computational and human effort.Tue, 13 Mar 2012 11:44:59 GMThttp://hdl.handle.net/2381/101792012-03-13T11:44:59Z