DSpace Collection:
http://hdl.handle.net/2381/4072
2016-02-13T08:51:07Z
2016-02-13T08:51:07Z
Finding Recurrent Sets with Backward Analysis and Trace Partitioning
Piterman, Nir
Bakhirkin, Alexey
http://hdl.handle.net/2381/36303
2016-01-18T14:58:11Z
2016-01-18T14:57:54Z
Title: Finding Recurrent Sets with Backward Analysis and Trace Partitioning
Authors: Piterman, Nir; Bakhirkin, Alexey
Abstract: We propose an abstract-interpretation-based analysis for recurrent sets.
A recurrent set is a set of states from which the execution of a program cannot or
might not (as in our case) escape. A recurrent set is a part of a program’s nontermination
proof (that needs to be complemented by reachability analysis). We
find recurrent sets by performing a potentially over-approximate backward analysis
that produces an initial candidate. We then perform over-approximate forward
analysis on the candidate to check and refine it and ensure soundness. In practice,
the analysis relies on trace partitioning that predicts future paths through the
program that non-terminating executions will take. Using our technique, we were
able to find recurrent sets in many benchmarks found in the literature including
some that, to our knowledge, cannot be handled by existing tools. In addition,
we note that typically, analyses that search for recurrent sets are applied to linear
under-approximations of programs or employ some form of non-approximate
numeric reasoning. In contrast, our analysis uses standard abstract-interpretation
techniques and is potentially applicable to a larger class of abstract domains (and
therefore – programs).
Description: The file is under embargo for 12 months from publication.
2016-01-18T14:57:54Z
T2: Temporal Property Verification
Brockschmidt, Mark
Cook, Byron
Ishtiaq, Samin
Khlaaf, Heidy
Piterman, Nir
http://hdl.handle.net/2381/36301
2016-01-18T14:14:35Z
2016-01-18T14:14:13Z
Title: T2: Temporal Property Verification
Authors: Brockschmidt, Mark; Cook, Byron; Ishtiaq, Samin; Khlaaf, Heidy; Piterman, Nir
Abstract: We present the open-source tool T2, the first public release
from the TERMINATOR project. T2 has been extended over the past
decade to support automatic temporal-logic proving techniques and to
handle a general class of user-provided liveness and safety properties.
Input can be provided in a native format and in C, via the support of
the LLVM compiler framework. We briefly discuss T2’s architecture, its
underlying techniques, and conclude with an experimental illustration of
its competitiveness and directions for future extensions.
Description: The file is under embargo for 12 months from publication.
2016-01-18T14:14:13Z
An Evidential Reasoning Approach for Assessing Confidence in Safety Evidence
Nair, S.
Walkinshaw, Neil
Kelly, T.
Vara, J.
http://hdl.handle.net/2381/36003
2015-12-08T03:06:36Z
2015-12-07T11:32:28Z
Title: An Evidential Reasoning Approach for Assessing Confidence in Safety Evidence
Authors: Nair, S.; Walkinshaw, Neil; Kelly, T.; Vara, J.
Abstract: Safety cases present the arguments and evidence that can be used to justify the acceptable safety of a system. Many secondary factors such as the tools
used, the techniques applied, and the experience of the people who created the evidence, can affect an assessor’s confidence in the evidence cited by a safety case. One means of reasoning about this confidence and its inherent uncertainties is to present a ‘confidence argument’ that explicitly justifies the provenance of the evidence used. In this paper, we propose a novel approach to automatically construct these confidence arguments by enabling assessors to provide individual judgements concerning the trustworthiness and the appropriateness of the evidence. The approach is based on Evidential Reasoning and enables the derivation of a quantified aggregate of the overall confidence. The proposed approach is supported by a prototype tool (EviCA) and has been evaluated using the Technology Acceptance Model.
2015-12-07T11:32:28Z
How to Make Best Use of Cross-Company Data for Web Effort Estimation?
Minku, Leandro Lei
Sarro, Federica
Mendes, Emilia
Ferrucci, Filomena
http://hdl.handle.net/2381/35961
2015-12-08T03:05:42Z
2015-11-30T10:12:25Z
Title: How to Make Best Use of Cross-Company Data for Web Effort Estimation?
Authors: Minku, Leandro Lei; Sarro, Federica; Mendes, Emilia; Ferrucci, Filomena
Abstract: [Context]: The numerous challenges that can hinder software companies from gathering their own data have motivated over the past 15 years research on the use of cross-company (CC) datasets for software effort prediction. Part of this research focused on Web effort prediction, given the large increase worldwide in the development of Web applications. Some of these studies indicate that it may be possible to achieve better performance using CC models if some strategy to make the CC data more similar to the within-company (WC) data is adopted. [Goal]: This study investigates the use of a recently proposed approach called Dycom to assess to what extent Web effort predictions obtained using CC datasets are effective in relation to the predictions obtained using WC data when explicitly mapping the CC models to the WC context. [Method]: Data on 125 Web projects from eight different companies part of the Tukutuku database were used to build prediction models. We benchmarked these models against baseline models (mean and median effort) and a WC base learner that does not benefit of the mapping. We also compared Dycom against a competitive CC approach from the literature (NN-filtering). We report a company-by- company analysis. [Results]: Dycom usually managed to achieve similar or better performance than a WC model while using only half of the WC training data. These results are also an improvement over previous studies that investigated the use of different strategies to adapt CC models to the WC data for Web effort estimation. [Conclusions]: We conclude that the use of Dycom for Web effort prediction is quite promising and in general supports previous results when applying Dycom to conventional software datasets.
Description: Archived in accordance with the publisher's posting policy, available at http://www.ieee.org/publications_standards/publications/rights/rights_policies.html
2015-11-30T10:12:25Z
Maximizing Throughput in Energy-Harvesting Sensor Nodes
Fung, Ping Yuen
http://hdl.handle.net/2381/33484
2016-02-04T02:45:11Z
2015-11-03T12:15:43Z
Title: Maximizing Throughput in Energy-Harvesting Sensor Nodes
Authors: Fung, Ping Yuen
Abstract: We consider an online throughput maximization problem in sensor nodes that can harvest energy. The sensor nodes generate and forward packets, which cost energy; they can also harvest energy from the environment, but the amount of energy that can be harvested is not known in advance. We give a number of algorithms and lower bounds for the case of a single node. We consider both the general case and some types of ‘non-idling’ adversaries where we can get better bounds. We also consider the case of networks with multiple nodes and demonstrate that some very simple scenarios already admit no competitive algorithms.
2015-11-03T12:15:43Z
Modeling and reasoning over distributed systems using aspect-oriented graph grammars
Machado, Rodrigo
Heckel, Reiko
Ribeiro, Leila
http://hdl.handle.net/2381/33145
2015-10-02T02:00:52Z
2015-10-01T11:02:25Z
Title: Modeling and reasoning over distributed systems using aspect-oriented graph grammars
Authors: Machado, Rodrigo; Heckel, Reiko; Ribeiro, Leila
Abstract: Aspect-orientation is a relatively new paradigm that introduces abstractions to modularize the implementation of system-wide policies. It is based on a composition operation, called aspect weaving, that implicitly modifies a base system by performing related changes within the system modules. Aspect-oriented graph grammars (AOGG) extend the classic graph grammar formalism by defining aspects as sets of rule-based modifications over a base graph grammar. Despite the advantages of aspect-oriented concepts regarding modularity, the implicit nature of the aspect weaving operation may also introduce issues when reasoning about the system behavior. Since in AOGGs aspect weaving is characterized by means of rule-based rewriting, we can overcome these problems by using known analysis techniques from the graph transformation literature to study aspect composition. In this paper, we present a case study of a distributed client-server system with global policies, modeled as an aspect-oriented graph grammar, and discuss how to use the AGG tool to identify potential conflicts in aspect weaving.
2015-10-01T11:02:25Z
Towards an embedding of Graph Transformation in Intuitionistic Linear Logic
Torrini, Paolo
Heckel, Reiko
http://hdl.handle.net/2381/33144
2015-10-02T02:00:52Z
2015-10-01T10:46:22Z
Title: Towards an embedding of Graph Transformation in Intuitionistic Linear Logic
Authors: Torrini, Paolo; Heckel, Reiko
Abstract: Linear logics have been shown to be able to embed both rewriting-based approaches and process calculi in a single, declarative framework. In this paper we are exploring the embedding of double-pushout graph transformations into quantified linear logic, leading to a Curry-Howard style isomorphism between graphs and transformations on one hand, formulas and proof terms on the other. With linear implication representing rules and reachability of graphs, and the tensor modelling parallel composition of graphs and transformations, we obtain a language able to encode graph transformation systems and their computations as well as reason about their properties.
2015-10-01T10:46:22Z
From nondeterministic Buchi and Streett automata to deterministic parity automata
Piterman, Nir
http://hdl.handle.net/2381/33113
2015-09-29T02:00:43Z
2015-09-28T10:47:34Z
Title: From nondeterministic Buchi and Streett automata to deterministic parity automata
Authors: Piterman, Nir
Abstract: In this paper we revisit Safra's determinization constructions. We show how to construct deterministic automata with fewer states and, most importantly, parity acceptance conditions. Specifically, starting from a nondeterministic Buchi automaton with n states our construction yields a deterministic parity automaton with n2n+2 states and index 2n (instead of a Rabin automaton with (12)nn2n states and n pairs). Starting from a nondeterministic Streett automaton with n states and k pairs our construction yields a deterministic parity automaton with nn(k+2)+2(k+1)2n(K+1) states and index 2n(k+1) (instead of a Rabin automaton with (12)n(k+1)n n(k+2)(k+1)2n(k+1) states and n(k+1) pairs). The parity condition is much simpler than the Rabin condition. In applications such as solving games and emptiness of tree automata handling the Rabin condition involves an additional multiplier of n2n!(or(n(k+1))2(n(k+1))! in the case of Streett) which is saved using our construction.
2015-09-28T10:47:34Z
Reducing Idle Listening during Data Collection in Wireless Sensor Networks
Rasul, Aram
Erlebach, Thomas
http://hdl.handle.net/2381/32370
2015-06-13T02:00:43Z
2015-06-12T09:26:08Z
Title: Reducing Idle Listening during Data Collection in Wireless Sensor Networks
Authors: Rasul, Aram; Erlebach, Thomas
Abstract: Data collection is one of the predominant operations in wireless sensor networks. This paper focuses on the problem of efficient data collection in a setting where some nodes may not possess data each time data is collected. In that case, idle listening slots may occur, which lead to a waste of energy and an increase in latency. To alleviate these problems, successive-slot schedules were proposed by Zhao and Tang (Infocom 2011). In this paper, we introduce a so-called extra-bit technique to reduce idle listening further. Each packet includes an extra bit that informs the receiver whether further data packets will follow or not. The extra-bit technique leads to significantly reduced idle listening and improved latency in many cases. We prove that every successive-slot schedule is also an extra-bit schedule. We then consider the special case of linear networks and prove that the optimal length of a successive-slot schedule (or extra-bit schedule) is 4N - 6 time slots, where N ≥ 3 is the number of nodes excluding the sink. Then the proposed extra-bit technique is compared with the successive-slot technique with respect to the expected amount of idle listening, and it is shown that the extra-bit technique reduces idle listening substantially.
Description: timestamp: Thu, 05 Mar 2015 11:05:43 +0100 biburl: http://dblp.uni-trier.de/rec/bib/conf/msn/RasulE14 bibsource: dblp computer science bibliography, http://dblp.org
2015-06-12T09:26:08Z
Better Algorithms for Online Bin Stretching
Böhm, Martin
Sgall, Jin
Stee, Rob van
Veselý, Pavel
http://hdl.handle.net/2381/32322
2015-12-04T12:17:10Z
2015-06-01T10:31:30Z
Title: Better Algorithms for Online Bin Stretching
Authors: Böhm, Martin; Sgall, Jin; Stee, Rob van; Veselý, Pavel
Abstract: Online Bin Stretching is a semi-online variant of bin packing in which the algorithm has to use the same number of bins as the optimal packing, but is allowed to slightly
overpack the bins. The goal is to minimize the amount of overpacking, i.e., the maximum
size packed into any bin.
We give an algorithm for Online Bin Stretching with a stretching factor of 1:5 for
any number of bins. We also show a specialized algorithm for three bins with a stretching
factor of 11=8 = 1:375.
Description: The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-18263-6_3
2015-06-01T10:31:30Z
The optimal absolute ratio for online bin packing
Balogh, Janos
Békési, Jozsef
Dósa, Gyorgy
Sgall, Jiri
Stee, Rob van
http://hdl.handle.net/2381/32320
2015-06-01T09:53:41Z
2015-06-01T09:53:03Z
Title: The optimal absolute ratio for online bin packing
Authors: Balogh, Janos; Békési, Jozsef; Dósa, Gyorgy; Sgall, Jiri; Stee, Rob van
Abstract: We present an online bin packing algorithm with absolute competitive ratio 5/3, which is optimal.
2015-06-01T09:53:03Z
On Automation of CTL* Verification for Infinite-State Systems
Cook, B.
Khlaaf, H.
Piterman, Nir
http://hdl.handle.net/2381/32307
2015-11-20T15:15:47Z
2015-05-26T11:33:09Z
Title: On Automation of CTL* Verification for Infinite-State Systems
Authors: Cook, B.; Khlaaf, H.; Piterman, Nir
Abstract: In this paper we introduce the first known fully automated tool for symbolically proving CTL* properties of (infinite-state) integer programs. The method uses an internal encoding which facilitates reasoning about the subtle interplay between the nesting of path and state temporal operators that occurs within \ctlstar proofs. A precondition synthesis strategy is then used over a program transformation which trades nondeterminism in the transition relation for nondeterminism explicit in variables predicting future outcomes when necessary. We show the viability of our approach in practice using examples drawn from device drivers and various industrial examples.
2015-05-26T11:33:09Z
Synthesising Executable Gene Regulatory Networks from Single-Cell Gene Expression Data
Fisher, J.
Köksal, A. S.
Piterman, Nir
Woodhouse, S.
http://hdl.handle.net/2381/32306
2015-08-20T11:57:21Z
2015-05-26T11:29:52Z
Title: Synthesising Executable Gene Regulatory Networks from Single-Cell Gene Expression Data
Authors: Fisher, J.; Köksal, A. S.; Piterman, Nir; Woodhouse, S.
Abstract: Recent experimental advances in biology allow researchers to obtain gene expression profiles at single-cell resolution over hundreds, or even thousands of cells at once. These single-cell measurements provide snapshots of the states of the cells that make up a tissue, instead of the population-level averages provided by conventional high-throughput experiments. This new data therefore provides an exciting opportunity for computational modelling. In this paper we introduce the idea of viewing single-cell gene expression profiles as states of an asynchronous Boolean network, and frame model inference as the problem of reconstructing a Boolean network from its state space. We then give a scalable algorithm to solve this synthesis problem. We apply our technique to both simulated and real data. We first apply our technique to data simulated from a well established model of common myeloid progenitor differentiation. We show that our technique is able to recover the original Boolean network rules. We then apply our technique to a large dataset taken dur- ing embryonic development containing thousands of cell measurements. Our technique synthesises matching Boolean networks, and analysis of these models yields new predictions about blood development which our experimental collaborators were able to verify.
2015-05-26T11:29:52Z
Performance and energy evaluation of RESTful web services in Raspberry Pi
Nunes, L. H.
Nakamura, L. H. V.
De F. Vieira, H..
De O. Libardi, R. M.
De Oliveira, E. M.
Estrella, J. C.
Reiff-Marganiec, Stephan
http://hdl.handle.net/2381/32267
2015-05-14T02:00:24Z
2015-05-13T10:06:24Z
Title: Performance and energy evaluation of RESTful web services in Raspberry Pi
Authors: Nunes, L. H.; Nakamura, L. H. V.; De F. Vieira, H..; De O. Libardi, R. M.; De Oliveira, E. M.; Estrella, J. C.; Reiff-Marganiec, Stephan
Abstract: Green computing has emerged as a hot topic leading to a need to understand energy consumption of computations. This need also extends to devices with limited resources as are common in the internet of things. RESTful services have shown their potential on such devices, but there are many choices of frameworks for their development and execution. Current research has analysed performance of the frameworks but no attention has been given to systematically studying their power consumption. In this paper we analyse the execution behaviour and power consumption of web services on devices with limited resources and make initial observations that should influence future development of web service frameworks. Specifically, we conduct experiments comparing web services in the Axis2 and CXF frameworks analysing the respective performance and power consumption. Bringing together the best features of small devices and SoC, it is possible to provide diverse, mobile and green applications - however careful selection of development environments can make significant differences in performance and energy consumption.
2015-05-13T10:06:24Z
Observing access control policies using scrabble games
Ahmad, S.
Abidin, S. Z. Z.
Omar, N.
Reiff-Marganiec, Stephan
http://hdl.handle.net/2381/32266
2015-05-14T02:00:26Z
2015-05-13T09:55:17Z
Title: Observing access control policies using scrabble games
Authors: Ahmad, S.; Abidin, S. Z. Z.; Omar, N.; Reiff-Marganiec, Stephan
Abstract: Access control is concerned with the policies that manage data sharing activities. Access control plays a crucial role in application areas such as education, health and business. However, most programming languages and programming environments do not naturally provide support for implementing access control policies requiring access control policies for systems to be coded as part of the development effort. Access control management policies are high-level features so having to involve a computer programmer during deployment stages for making changes to policies is costly. In this paper, we present an abstraction of access control management policies in the form of extended scrabble in its rules. The needs of access control policies program construct for supporting this game are examined. New relevant program constructs are then incorporated into JACIE (Java-based Authoring language for Collaborative Interactive Environments). The usefulness of these program construct are being demonstrated through the extended scrabble.
2015-05-13T09:55:17Z
Classifying Smart Objects using capabilities
Pérez Hernández, Marco E.
Reiff-Marganiec, Stephan
http://hdl.handle.net/2381/32265
2015-05-14T02:00:22Z
2015-05-13T09:46:00Z
Title: Classifying Smart Objects using capabilities
Authors: Pérez Hernández, Marco E.; Reiff-Marganiec, Stephan
Abstract: The Internet Of Things has emerged, providing an umbrella for the increasing number of heterogeneous Smart Objects that are becoming part of our daily activities. In this scenario, classification approaches are useful to understand differences and identify opportunities of generalization and common solutions, especially when different disciplines are coming together and bringing their individual terms and concepts. We propose a novel model for classifying Smart Objects using capabilities. This five-level model, inspired in the Capability Maturity Models, aims to be simple and inclusive, separating objects with basic capabilities from those with complex ones. In addition, examples of objects for each level are provided as validation of the proposal. The model is useful to identify requirements that Smart Objects have to cover externally as they cannot themselves support them and thus it allows for clear understanding of the external support system (or Middleware) into which the smart object is embedded.
2015-05-13T09:46:00Z
Design and implementation of fault tolerance techniques to improve QoS in SOA
Oliveira, E. M.
Estrella, J. C.
Kuehne, B. T.
Filho, D. M. L.
Adami, L. J.
Nunes, L. H.
Nakamura, L. H.
Libardi, R. M.
Souza, P. S. L.
Reiff-Marganiec, Stephan
http://hdl.handle.net/2381/32264
2015-05-14T02:00:22Z
2015-05-13T09:23:28Z
Title: Design and implementation of fault tolerance techniques to improve QoS in SOA
Authors: Oliveira, E. M.; Estrella, J. C.; Kuehne, B. T.; Filho, D. M. L.; Adami, L. J.; Nunes, L. H.; Nakamura, L. H.; Libardi, R. M.; Souza, P. S. L.; Reiff-Marganiec, Stephan
Abstract: Fault tolerance techniques can improve the trust of users in service oriented architectures as they can ensure data availability. This paper presents an implementation of a novel fault tolerance mechanism in a SOA architecture which simultaneously provides increased availability and better quality of service. In addition to this mechanism, a service selector using reputation ratings of the architecture components is discussed. The selection is based on information from past transactions of the components of the architecture, which allows to identify the best web services able to meet the requests of customers. The mechanisms are tested and a performance evaluation is presented to validate the results.
2015-05-13T09:23:28Z
A semantic approach for efficient and customized management of IaaS resources
Nakamura, L. H. V.
Estrella, J. C.
Santana, R. H. C.
Santana, M. J.
Reiff-Marganiec, Stephan
http://hdl.handle.net/2381/32263
2015-05-14T02:00:24Z
2015-05-13T09:15:14Z
Title: A semantic approach for efficient and customized management of IaaS resources
Authors: Nakamura, L. H. V.; Estrella, J. C.; Santana, R. H. C.; Santana, M. J.; Reiff-Marganiec, Stephan
Abstract: This paper presents a semantic approach to custom management of IaaS (Infrastructure as a Service) resources in a cloud computing environment requiring minimal human intervention from both the cloud provider and the user. The proposal differs from other approaches by using autonomic computing and semantic web techniques together to provide a self-configuring and self-optimizing environment that aims to satisfy SLAs (Service Level Agreements). The approach monitors the virtualized resources to guarantee a customized and optimized use based on financial criteria and energy consumption policies.
2015-05-13T09:15:14Z
Managing access control policy from end user perspective in collaborative environment
Ahmad, S.
Omar, N.
Abidin, S. Z. Z.
Reiff-Marganiec, Stephan
http://hdl.handle.net/2381/32252
2015-05-09T02:04:07Z
2015-05-08T14:55:00Z
Title: Managing access control policy from end user perspective in collaborative environment
Authors: Ahmad, S.; Omar, N.; Abidin, S. Z. Z.; Reiff-Marganiec, Stephan
Abstract: Currently, collaborative environments offer unlimited data sharing for users. Data owners are poorly involved in handling their data for such environment when it deals with data policy. Normally, data access control policy consists of a resource and authorization descriptions which are assigned by the administrator. It is the responsibility of the administrator to set and specify the policy for application services. The policy details are massive and complex for administrator to handle where most of the times there will be cases of unreview services. This paper proposes a framework that allows data owners to provision policies for storing and managing their shared data with third parties. By adapting RBAC model and adding owner's interest on permissions for data operations and objects, the proposed framework will facilitate data access control whereby owners have the freedom to set their own data access policy.
2015-05-08T14:55:00Z
Performance Evaluation in a Cloud with the Provisioning of Different Resources Configurations
Batista, B. G.
Estrella, J. C.
Santana, M. J.
Santana, R. H. C.
Reiff-Marganiec, Stephan
http://hdl.handle.net/2381/32250
2015-05-09T02:03:54Z
2015-05-08T14:11:44Z
Title: Performance Evaluation in a Cloud with the Provisioning of Different Resources Configurations
Authors: Batista, B. G.; Estrella, J. C.; Santana, M. J.; Santana, R. H. C.; Reiff-Marganiec, Stephan
Abstract: Cloud computing is a computing style where resource providers can offer on-demand services in a transparent way and clients usually pay as they go. It introduces a new level of flexibility and scalability for IT users addressing challenges such as the rapid change in IT and the need to reduce cost and time of infrastructure management. However, to be able to offer QoS guarantees without limiting the number of accepted requests, providers must be able to dynamically adjust the available resources to serve requests. This dynamic resource management is not a trivial task, bringing its own challenges related to workload and performance modelling, and deployment and monitoring of applications on virtualised IT resources. An efficient mapping between resources and applications ensures workload balancing and good resource utilization and allows to meet the QoS levels required by clients. This paper presents a performance evaluation that considers different resource configurations in a cloud environment to define which dimension of resource scaling has real impact on client applications.
2015-05-08T14:11:44Z
Low-Latency Service Data Aggregation Using Policy Obligations
Reiff-Marganiec, Stephan
Tilly, M.
Janicke, H.
http://hdl.handle.net/2381/32249
2015-05-09T02:04:03Z
2015-05-08T13:59:21Z
Title: Low-Latency Service Data Aggregation Using Policy Obligations
Authors: Reiff-Marganiec, Stephan; Tilly, M.; Janicke, H.
Abstract: The Internet of Things, large scale sensor networks or even in social media, are now well established and their use is growing daily. Usage scenarios in these fields highlight the requirement to process, procure, and provide information with almost zero latency. This work is introducing new concepts for enabling fast communication by limiting information flow through filtering concepts combined with data processing techniques adopted from complex event processing. Specifically we introduce a novel mediation services architecture using filter policies to reduce latency. The filter policies define when and what data services need to provide to the mediator and thus save on bandwidth. The filter policies describe temporal conditions between two events removing the need to keep a complete history while still allowing temporal reasoning. Promising experimental results highlight the advantages to be gained from the approach.
2015-05-08T13:59:21Z
PEESOS: A Web Tool for Planning and Execution of Experiments in Service Oriented Systems
Nunes, L. H.
Vasconcelos Nakamura, L. H.
Tardiole Kuehne, B.
De Oliveira, E. M.
De O Libardi, R. M.
Junqueira Adami, L.
Estrella, J. C.
Reiff-Marganiec, Stephan
http://hdl.handle.net/2381/32241
2015-09-15T09:34:26Z
2015-05-08T10:56:39Z
Title: PEESOS: A Web Tool for Planning and Execution of Experiments in Service Oriented Systems
Authors: Nunes, L. H.; Vasconcelos Nakamura, L. H.; Tardiole Kuehne, B.; De Oliveira, E. M.; De O Libardi, R. M.; Junqueira Adami, L.; Estrella, J. C.; Reiff-Marganiec, Stephan
Abstract: Performing functionality testing in service-oriented architectures is not a trivial task. The difficulty is especially the large number of components that may be present in a SOA such as brokers, providers, service registries, clients, monitoring tools, data storage tools, etc. Thus, in order to facilitate the process of conducting functional testing and capacity planning in service-oriented systems, we present PEESOS. This first version is a functional prototype that offers facilities to assist researchers and industry to test their new applications, allowing collaborations that can be done between the participants to achieve an appropriate objective when developing a new application. The first results show that it is possible to make a planning environment easier to operate and to readily obtain results for performance evaluation of a target architecture. Since this is a first version of the prototype, it has interface and scalability limitations as well as needing improvements in performance of the logs repository and also in a core engine. We hope that such limitations can be corrected in the near future, including gathering information from the scientific community to make the prototype a useful and accessible tool. PEESOS is on-line and available at http://peesos.wsarch.lasdpc.icmc.usp.br.
Description: PEESOS is on-line and available at http://peesos.wsarch.lasdpc.icmc.usp.br.
2015-05-08T10:56:39Z
Providing Quality of Service on Services Selection Using Anycast Techniques
Adami, L. J.
Estrella, J. C.
De Oliveira, E. M.
Reiff- Marganiec, Stephan
http://hdl.handle.net/2381/32239
2015-05-09T02:03:40Z
2015-05-08T10:48:38Z
Title: Providing Quality of Service on Services Selection Using Anycast Techniques
Authors: Adami, L. J.; Estrella, J. C.; De Oliveira, E. M.; Reiff- Marganiec, Stephan
Abstract: Over the last years, the complexity and variety of services available on the Internet increased. This fact is leading to the search for efficient techniques of routing client requests to the best server available. A known technique is the application layer anycast (ALA). The main goal of this work is to elaborate efficient ways to provide ALA with quality of service in the context of cloud computing. To achieve this goal, we proposed a new algorithm (GALA, Global Application Layer Anycast). It inherits characteristics from another existing system (GAA, Global Application-layer Anycast), and uses geolocation as a differential. The results of the experiments show that GALA, compared to the inherited algorithm, maintains the client requests efficiencies and substantially lowers their latencies.
2015-05-08T10:48:38Z
A Utility-Aware Runtime Conflict Resolver for Composite Web services
Ning, X.
Xu, J.
Xu, N.
Reiff-Marganiec, Stephan
http://hdl.handle.net/2381/32237
2015-10-22T14:19:16Z
2015-05-08T10:40:16Z
Title: A Utility-Aware Runtime Conflict Resolver for Composite Web services
Authors: Ning, X.; Xu, J.; Xu, N.; Reiff-Marganiec, Stephan
Abstract: Web services are developed independently and
deployed in a distributed environment, new service can be
obtained by composing existing ones. The rapid introduction
of new services also results in undesirable interactions between
services. These conflicts are not mismatches of interfaces, but
are usually based on the data in the executing instance and
therefore runtime management of conflicts in Web services
should be considered. We study the problem from the perspective
of user’s revenue, and propose an online approach to
resolve conflicts is proposed.
2015-05-08T10:40:16Z
Study Case of Restful Frameworks in Raspberry Pi: A Perfomance and Energy Overview
Nunes, L. H.
Nakamura, L. H. V.
De F. Vieira, H.
De O. Libardi, R. M.
De Oliveira, E. M.
Adami, L. J.
Estrella, J. C.
Reiff-Marganiec, Stephan
http://hdl.handle.net/2381/32236
2015-05-09T02:03:38Z
2015-05-08T10:34:01Z
Title: Study Case of Restful Frameworks in Raspberry Pi: A Perfomance and Energy Overview
Authors: Nunes, L. H.; Nakamura, L. H. V.; De F. Vieira, H.; De O. Libardi, R. M.; De Oliveira, E. M.; Adami, L. J.; Estrella, J. C.; Reiff-Marganiec, Stephan
Abstract: This paper analyzes the execution behavior of web
services on devices with limited resources. The experiments
compare web services in the Axis2 and CXF frameworks
analyzing performance and power consumption. To determine
which framework is better suited for service provision, a testing
environment and a performance and energy evaluation between
them are presented. We show that the Raspberry Pi can be
useful in service-oriented applications for different types of
tasks. Bringing together the best features of small devices
and SoC, it is possible to provide diverse, mobile and green
applications.
2015-05-08T10:34:01Z
Fast Selection of Web Services with QoS using a Distributed Parallel Semantic Approach
Nakamura, L. H. V.
do Prado, P. F.
de O. Libardi, R. M.
Nunes, L. H.
Estrella, J. C.
Santana, R. H. C.
Santana, M. J.
Reiff-Marganiec, Stephan
http://hdl.handle.net/2381/32235
2015-09-15T09:34:20Z
2015-05-08T10:25:34Z
Title: Fast Selection of Web Services with QoS using a Distributed Parallel Semantic Approach
Authors: Nakamura, L. H. V.; do Prado, P. F.; de O. Libardi, R. M.; Nunes, L. H.; Estrella, J. C.; Santana, R. H. C.; Santana, M. J.; Reiff-Marganiec, Stephan
Abstract: This paper presents a solution to performance
issues in the quality of service aware selection of Web services
using techniques of parallelism and mechanisms of inference
provided by Semantic Web. The results point to a significant
improvement in the speed of searching Web services and thus
makes the use of semantic resources viable in distributed
systems to provide better quality of service to the clients.
2015-05-08T10:25:34Z
Encoding Data Structures
Raman, Rajeev
http://hdl.handle.net/2381/32217
2015-05-08T02:00:49Z
2015-05-07T13:20:56Z
Title: Encoding Data Structures
Authors: Raman, Rajeev
Abstract: In recent years, there has been an explosion of interest in
succinct data structures, which store the given data in compact or compressed
formats and answer queries on the data rapidly while it is still
in its compressed format. Our focus in this talk is to introduce encoding
data structures. Encoding data structures consider the data together
with the queries and aim to store only as much information about the
data as is needed to store the queries. Once this is done, the original data
can be deleted. In many cases, one can obtain space-efficient encoding
data structures even when the original data is incompressible.
Description: Abstract of invited talk.
2015-05-07T13:20:56Z
Compact Encodings and Indexes for the Nearest Larger Neighbor Problem
Jo, S.
Raman, Rajeev
Satti, S. R.
http://hdl.handle.net/2381/32215
2015-05-08T02:00:55Z
2015-05-07T13:05:29Z
Title: Compact Encodings and Indexes for the Nearest Larger Neighbor Problem
Authors: Jo, S.; Raman, Rajeev; Satti, S. R.
Abstract: Given a d-dimensional array, for any integer d > 0, the nearest
larger value (NLV) query returns the position of the element which
is closest, in L1 distance, to the query position, and is larger than the
element at the query position. We consider the problem of preprocessing
a given array, to construct a data structure that can answer NLV queries
efficiently. In the 2-D case, given an n × n array A, we give an asymptotically
optimal O(n
2
)-bit encoding that answers NLV queries in O(1)
time. When A is a binary array, we describe a simpler O(n
2
)-bit encoding
that also supports NLV queries in O(1) time. Using this, we obtain
an index of size O(n
2
/c) bits that supports NLV queries in O(c) time,
for any parameter c, where 1 ≤ c ≤ n, matching the lower bound. For
the 1-D case we consider the nearest larger right value (NLRV) problem
where the nearest larger value to the right is sought. For an array of
length n, we obtain an index that takes O((n/c) log c) bits, and supports
NLRV queries in O(c) time, for any any parameter c, where 1 ≤ c ≤ n,
improving the earlier results of Fischer et al. and Jayapaul et al.
2015-05-07T13:05:29Z
Black-Box Test Generation from Inferred Models
Papadopoulos, Petros
Walkinshaw, Neil
http://hdl.handle.net/2381/32206
2015-08-25T01:45:08Z
2015-05-07T10:44:39Z
Title: Black-Box Test Generation from Inferred Models
Authors: Papadopoulos, Petros; Walkinshaw, Neil
Abstract: Automatically generating test inputs for components
without source code (are ‘black-box’) and specification is challenging.
One particularly interesting solution to this problem is to
use Machine Learning algorithms to infer testable models from
program executions in an iterative cycle. Although the idea has
been around for over 30 years, there is little empirical information
to inform the choice of suitable learning algorithms, or to show
how good the resulting test sets are. This paper presents an
openly available framework to facilitate experimentation in this
area, and provides a proof-of-concept inference-driven testing
framework, along with evidence of the efficacy of its test sets on
three programs.
2015-05-07T10:44:39Z
CPT+: Decreasing the time/space complexity of the Compact Prediction Tree
Gueniche, T.
Fournier-Viger, P.
Raman, Rajeev
Tseng, V.
http://hdl.handle.net/2381/32181
2015-06-05T13:40:30Z
2015-05-07T10:25:53Z
Title: CPT+: Decreasing the time/space complexity of the Compact Prediction Tree
Authors: Gueniche, T.; Fournier-Viger, P.; Raman, Rajeev; Tseng, V.
Abstract: Predicting next items of sequences of symbols has many applications in a wide range of domains. Several sequence prediction models have been proposed such as DG, All-k-order markov and PPM. Recently, a model named Compact Prediction Tree (CPT) has been proposed. It relies on a tree structure and a more complex prediction algorithm to offer considerably more accurate predictions than many state-of-the-art prediction models. However, an important limitation of CPT is its high time and space complexity. In this article, we address this issue by proposing three novel strategies to reduce CPT’s size and prediction time, and increase its accuracy. Experimental results on seven real life datasets show that the resulting model (CPT+) is up to 98 times more compact and 4.5 times faster than CPT, and has the best overall accuracy when compared to six state-of-the-art models from the literature: All-K-order Markov, CPT, DG, Lz78, PPM and TDAG.
Description: Accepted as "REGULAR PAPER WITH LONG PRESENTATION" 27 of 405 submisisons accepted in this category.
2015-05-07T10:25:53Z
Encoding Nearest Larger Values
Nicholson, P. K.
Raman, Rajeev
http://hdl.handle.net/2381/32178
2015-06-23T15:57:32Z
2015-05-07T10:24:32Z
Title: Encoding Nearest Larger Values
Authors: Nicholson, P. K.; Raman, Rajeev
Abstract: In nearest larger value (NLV) problems, we are given an array A[1..n] of numbers, and need to preprocess A to answer queries of the following form: given any index i ∈ [1, n], return a “nearest” index j such that A[j] > A[i]. We consider the variant where the values in A are distinct, and we wish to return an index j such that A[j] > A[i] and |j − i| is minimized, the nondirectional NLV (NNLV) problem. We consider NNLV in the encoding model, where the array A is delete after preprocessing, and note that NNLV encoding problem has an unexpectedly rich structure: the effective entropy (optimal space usage) of the problem depends crucially on details in the definition of the problem. Using a new path-compressed representation of binary trees, that may have other applications, we encode NNLV in 1.9n + o(n) bits, and answer queries in O(1) time.
2015-05-07T10:24:32Z
MSSF: User-friendly multi-cloud data dispersal
Libardi, R. M. de O.
Reiff-Marganiec, Stephan
Nunes, L. H.
Adami, L. J.
Ferreira, C. H. G.
Estrella, J. C.
http://hdl.handle.net/2381/32159
2015-11-16T11:31:42Z
2015-05-07T10:13:11Z
Title: MSSF: User-friendly multi-cloud data dispersal
Authors: Libardi, R. M. de O.; Reiff-Marganiec, Stephan; Nunes, L. H.; Adami, L. J.; Ferreira, C. H. G.; Estrella, J. C.
Abstract: Using a multi-cloud storage solution requires a
user to make complex decisions. Making these decisions can
be a problem for regular users who are not familiar with
multi-cloud storage. We propose MSSF, a Multi-cloud Storage
Selection Framework to automatically select a storage dispersal
strategy. MSSF formalises the selection process using a knapsack
optimisation problem using integer linear programming along
with a rule-based system to select a multi-cloud storage strategy
that fits the user needs and requires only simple inputs from
the user. Our experiments show the performance and usability
aspects of our solution, making it useful in real environments.
2015-05-07T10:13:11Z
Local Reputation Management in Cloud Computing
Jiang, D.
Xu, J.
Yang, D.
Reiff-Marganiec, Stephan
http://hdl.handle.net/2381/32148
2015-08-26T01:45:08Z
2015-05-07T10:06:10Z
Title: Local Reputation Management in Cloud Computing
Authors: Jiang, D.; Xu, J.; Yang, D.; Reiff-Marganiec, Stephan
Abstract: In the Cloud computing community, the calculation
of the reputation using the feedback of cloud customers is
widely adopted to address the issue of trustworthiness of cloud
services. Currently, most methods pursue a global reputation
score essentially assuming that the value of a cloud service’s
reputation is the same for every consumer. However depending
on the expectations and needs of a consumer, there can be
significant deviation of perceived reputation for the same cloud
service. In this paper we propose a trust management framework
that differentiates reputation for various user groups
thus providing what we term local reputation. To achieve this
we compute the similarity of consumers based a decision-tree
model which is used to cluster feedback into localised scores.
To refine the result, a time decay factor applicable to feedback
is also to be considered. The simulation results illustrate that
our approach is feasible and also effective for consumers to
choose reputable cloud service.
2015-05-07T10:06:10Z
Quality of Service on Services Selection using Anycast Techniques: a Convergence Analysis
Adami, L. J.
Estrella, J. C.
Reiff-Marganiec, Stephan
Libardi, R. M. D. O.
http://hdl.handle.net/2381/32147
2015-11-17T09:51:39Z
2015-05-07T10:05:48Z
Title: Quality of Service on Services Selection using Anycast Techniques: a Convergence Analysis
Authors: Adami, L. J.; Estrella, J. C.; Reiff-Marganiec, Stephan; Libardi, R. M. D. O.
Abstract: Anycast is an effective technique to select system servers among many and by spreading client requests achieve high performance and scalability. In our previous work, we presented the Global Application Layer Anycast (GALA) system. By combining real time network distances measures and geolocation, it performed better than its inherited algorithm, GAA. In this work we analyze how fast the GALA algorithm can find the best server to attend a client request and comparing its convergence to GAA. Using simulations, we show that it converges much faster and we propose a maximum selection time metric to be used in the selection process. Experimental results reveal that the GALA algorithm is two times better than the GAA considering the metric proposed.
2015-05-07T10:05:48Z
On Temporal Graph Exploration
Erlebach, Thomas
Hoffmann, Michael
Kammer, F.
http://hdl.handle.net/2381/32123
2015-07-13T11:40:41Z
2015-05-07T09:24:41Z
Title: On Temporal Graph Exploration
Authors: Erlebach, Thomas; Hoffmann, Michael; Kammer, F.
Editors: Speckmann, B.; Kobayashi, N.; Halldorsson, M. M.
Abstract: A temporal graph is a graph in which the edge set can change from step to step. The temporal graph exploration problem TEXP is the problem of computing a foremost exploration schedule for a temporal graph, i.e., a temporal walk that starts at a given start node, visits all nodes of the graph, and has the smallest arrival time. We consider only temporal graphs that are connected at each step. For such temporal graphs with $n$ nodes, we show that it is $\NP$-hard to approximate TEXP with ratio $O(n^{1-\epsilon})$ for any $\epsilon>0$. We also provide an explicit construction of temporal graphs that require $\Theta(n^2)$ steps to be explored. We then consider TEXP under the assumption that the underlying graph (i.e. the graph that contains all edges that are present in the temporal graph in at least one step) belongs to a specific class of graphs. Among other results, we show that temporal graphs can be explored in $O(n^{1.5}k^2\log n)$ steps if the underlying graph has treewidth $k$ and in $O(n\log^3 n)$ steps if the underlying graph is a $2\times n$ grid. Finally, we show that sparse temporal graphs with regularly present edges can always be explored in $O(n)$ steps.
2015-05-07T09:24:41Z
MSSF: A step towards user-friendly multi-cloud data dispersal
Libardi, R. M. de O.
Bedo, M. V. N.
Reiff-Marganiec, Stephan
Estrella, Julio C.
http://hdl.handle.net/2381/32118
2015-05-07T02:00:20Z
2015-05-06T12:06:35Z
Title: MSSF: A step towards user-friendly multi-cloud data dispersal
Authors: Libardi, R. M. de O.; Bedo, M. V. N.; Reiff-Marganiec, Stephan; Estrella, Julio C.
Abstract: With an increasing number of companies and individuals
adopting cloud computing for their data needs. Naturally,
there is a shift in financial and operational costs and and provided
services should meet users’ performance and cost expectations.
We focus on storage and propose MSSF, a Multi-cloud Storage
Selection Framework. MSSF contains a basic set of algorithms,
a set of security rules and a formal definition of user profiles
allowing to fit cloud storage services to user needs. Preliminary
experiments investigate the cost differences between two baseline
algorithms and user profile models. Considering the promising
initial results we provide several observations about the MSSF
decision making process that will help with future improvements.
2015-05-06T12:06:35Z
Tractable Probabilistic μ-Calculus that Expresses Probabilistic Temporal Logics
Castro, P.
Kilmurray, C.
Piterman, Nir
http://hdl.handle.net/2381/32065
2015-04-25T02:04:03Z
2015-04-24T16:40:02Z
Title: Tractable Probabilistic μ-Calculus that Expresses Probabilistic Temporal Logics
Authors: Castro, P.; Kilmurray, C.; Piterman, Nir
Abstract: We revisit a recently introduced probabilistic μ-calculus and study an expressive fragment of it. By using the probabilistic quantification as an atomic operation of the calculus we establish a connection between the calculus and obligation games. The calculus we consider is strong enough to encode well-known logics such as pCTL and pCTL*. Its game semantics is very similar to the game semantics of the classical μ-calculus (using parity obligation games instead of parity games). This leads to an optimal complexity of NP intersection co-NP for its finite model checking procedure. Furthermore, we investigate a (relatively) well-behaved fragment of this calculus: an extension of pCTL with fixed points. An important feature of this extended version of pCTL is that its model checking is only exponential w.r.t. the alternation depth of fixed points, one of the main characteristics of Kozen's μ-calculus.
Description: 1998 ACM Subject Classification F.4.1 Mathematical Logic
2015-04-24T16:40:02Z
Fairness for Infinite-State Systems
Cook, B.
Khlaaf, H.
Piterman, Nir
http://hdl.handle.net/2381/31957
2015-04-09T02:00:20Z
2015-04-08T09:51:07Z
Title: Fairness for Infinite-State Systems
Authors: Cook, B.; Khlaaf, H.; Piterman, Nir
Editors: Baier, C.; Tinelli , C.
Abstract: In this paper we introduce the first known tool for symbolically proving fair-CTL properties of (infinite-state) integer programs. Our solution is based on a reduction to existing techniques for fairness- free CTL model checking via the use of infinite non-deterministic branching to symbolically partition fair from unfair executions. We show the viability of our approach in practice using examples drawn from device drivers and algorithms utilizing shared resources.
Description: See also Research Note RN/14/11 UCL Department of Computer Science.
2015-04-08T09:51:07Z
From Communicating Machines to Graphical Choreographies
Lange, Julien
Tuosto, Emilio
Yoshida, Nobuko
http://hdl.handle.net/2381/31932
2015-03-28T03:00:22Z
2015-03-27T15:38:12Z
Title: From Communicating Machines to Graphical Choreographies
Authors: Lange, Julien; Tuosto, Emilio; Yoshida, Nobuko
Editors: Rajamani, S. K.; Walker, D.
Abstract: Graphical choreographies, or global graphs, are general multiparty session specifications featuring expressive constructs such as forking, merging, and joining for representing application-level protocols. Global graphs can be directly translated into modelling notations such as BPMN and UML. This paper presents an algorithm whereby a global graph can be constructed from asynchronous interactions represented by communicating finite-state machines (CFSMs). Our results include: a sound and complete characterisation of a subset of safe CFSMs from which global graphs can be constructed; an algorithm to translate CFSMs to global graphs; a time complexity analysis; and an implementation of our theory, as well as an experimental evaluation.
2015-03-27T15:38:12Z
Minimum Spanning Tree Verification under Uncertainty
Erlebach, Thomas R.
Hoffmann, Michael
http://hdl.handle.net/2381/31666
2015-10-23T08:45:37Z
2015-02-13T11:59:12Z
Title: Minimum Spanning Tree Verification under Uncertainty
Authors: Erlebach, Thomas R.; Hoffmann, Michael
Abstract: In the verification under uncertainty setting, an algorithm is given, for each input item, an uncertainty area that is guaranteed to contain the exact input value, as well as an assumed input value. An update of an input item reveals its exact value. If the exact value is equal to the assumed value, we say that the update verifies the assumed value. We consider verification under uncertainty for the minimum spanning tree (MST) problem for undirected weighted graphs, where each edge is associated with an uncertainty area and an assumed edge weight. The objective of an algorithm is to compute the smallest set of updates with the property that, if the updates of all edges in the set verify their assumed weights, the edge set of an MST can be computed. We give a polynomial-time optimal algorithm for the MST verification problem by relating the choices of updates to vertex covers in a bipartite auxiliary graph. Furthermore, we consider an alternative uncertainty setting where the vertices are embedded in the plane, the weight of an edge is the Euclidean distance between the endpoints of the edge, and the uncertainty is about the location of the vertices. An update of a vertex yields the exact location of that vertex. We prove that the MST verification problem in this vertex uncertainty setting is NP-hard. This shows a surprising difference in complexity between the edge and vertex uncertainty settings of the MST verification problem.
2015-02-13T11:59:12Z
Computational complexity of traffic hijacking under BGP and S-BGP
Chiesa, M.
Di Battista, G.
Patrignani, M.
Erlebach, Thomas
http://hdl.handle.net/2381/31661
2015-02-13T02:01:28Z
2015-02-12T15:21:43Z
Title: Computational complexity of traffic hijacking under BGP and S-BGP
Authors: Chiesa, M.; Di Battista, G.; Patrignani, M.; Erlebach, Thomas
Abstract: Harmful Internet hijacking incidents put in evidence how fragile the Border Gateway Protocol (BGP) is, which is used to exchange routing information between Autonomous Systems (ASes). As proved by recent research contributions, even S-BGP, the secure variant of BGP that is being deployed, is not fully able to blunt traffic attraction attacks. Given a traffic flow between two ASes, we study how difficult it is for a malicious AS to devise a strategy for hijacking or intercepting that flow. We show that this problem marks a sharp difference between BGP and S-BGP. Namely, while it is solvable, under reasonable assumptions, in polynomial time for the type of attacks that are usually performed in BGP, it is NP-hard for S-BGP. Our study has several by-products. E.g., we solve a problem left open in the literature, stating when performing a hijacking in S-BGP is equivalent to performing an interception.
2015-02-12T15:21:43Z
Approximation algorithms for disjoint st-paths with minimum activation cost
Alqahtani, Hasna Mohsen
Erlebach, Thomas
http://hdl.handle.net/2381/31648
2015-02-12T02:01:29Z
2015-02-11T13:28:34Z
Title: Approximation algorithms for disjoint st-paths with minimum activation cost
Authors: Alqahtani, Hasna Mohsen; Erlebach, Thomas
Abstract: In network activation problems we are given a directed or undirected graph G = (V,E) with a family {f (x, x) : (u,v) ∈ E} of monotone non-decreasing activation functions from D to {0,1}, where D is a constant-size domain. The goal is to find activation values x for all v ∈ V of minimum total cost Σ x such that the activated set of edges satisfies some connectivity requirements. Network activation problems generalize several problems studied in the network literature such as power optimization problems. We devise an approximation algorithm for the fundamental problem of finding the Minimum Activation Cost Pair of Node-Disjoint st-Paths (MA2NDP). The algorithm achieves approximation ratio 1.5 for both directed and undirected graphs. We show that a ρ-approximation algorithm for MA2NDP with fixed activation values for s and t yields a ρ-approximation algorithm for the Minimum Activation Cost Pair of Edge-Disjoint st-Paths (MA2EDP) problem. We also study the MA2NDP and MA2EDP problems for the special case |D| = 2.
2015-02-11T13:28:34Z
Establishing the Source Code Disruption Caused by Automated Remodularisation Tools
Hall, M.
Khojaye, Muhammad
Walkinshaw, Neil
McMinn, P.
http://hdl.handle.net/2381/31618
2015-02-06T02:01:58Z
2015-02-05T14:45:08Z
Title: Establishing the Source Code Disruption Caused by Automated Remodularisation Tools
Authors: Hall, M.; Khojaye, Muhammad; Walkinshaw, Neil; McMinn, P.
Editors: Poshyvanik, D.; Zaidman, A.
Abstract: Current software remodularisation tools only operate on abstractions of a software system. In this paper, we investigate the actual impact of automated remodularisation on source code using a tool that automatically applies remodularisations as refactorings. This shows us that a typical remodularisation (as computed by the Bunch tool) will require changes to thousands of lines of code, spread throughout the system (typically no code files remain untouched). In a typical multi-developer project this presents a serious integration challenge, and could contribute to the low uptake of such tools in an industrial context. We relate these findings with our ongoing research into techniques that produce iterative commit friendly code changes to address this problem.
2015-02-05T14:45:08Z
Minimum activation cost node-disjoint paths in graphs with bounded treewidth
Alqahtani, Hasna Mohsen
Erlebach, Thomas
http://hdl.handle.net/2381/31524
2015-01-31T02:01:32Z
2015-01-30T12:01:13Z
Title: Minimum activation cost node-disjoint paths in graphs with bounded treewidth
Authors: Alqahtani, Hasna Mohsen; Erlebach, Thomas
Abstract: In activation network problems we are given a directed or undirected graph G = (V,E) with a family {f uv : (u,v) ∈ E} of monotone non-decreasing activation functions from D2 to {0,1}, where D is a constant-size subset of the non-negative real numbers, and the goal is to find activation values xv for all v ∈ V of minimum total cost ∑ v ∈ V x v such that the activated set of edges satisfies some connectivity requirements. We propose algorithms that optimally solve the minimum activation cost of k node-disjoint st-paths (st-MANDP) problem in O(tw ((5 + tw)|D|)2tw + 2|V|3) time and the minimum activation cost of node-disjoint paths (MANDP) problem for k disjoint terminal pairs (s 1,t 1),…,(s k ,t k ) in O(tw ((4 + 3tw)|D|)2tw + 2|V|) time for graphs with treewidth bounded by tw.
2015-01-30T12:01:13Z
Lem : Reusable engineering of real-world semantics
Mulligan, Dominic P.
Gray, Kathryn E.
Sewell, Peter
Owens, Scott
Ridge, Tom
http://hdl.handle.net/2381/29328
2014-12-10T02:01:48Z
2014-12-09T10:33:34Z
Title: Lem : Reusable engineering of real-world semantics
Authors: Mulligan, Dominic P.; Gray, Kathryn E.; Sewell, Peter; Owens, Scott; Ridge, Tom
Abstract: Recent years have seen remarkable successes in rigorous engineering: using mathematically rigorous semantic models (not just idealised calculi) of real-world processors, programming languages, protocols, and security mechanisms, for testing, proof, analysis, and design. Building these models is challenging, requiring experimentation, dialogue with vendors or standards bodies, and validation; their scale adds engineering issues akin to those of programming to the task of writing clear and usable mathematics. But language and tool support for specification is lacking. Proof assistants can be used but bring their own difficulties, and a model produced in one, perhaps requiring many person-years effort and maintained over an extended period, cannot be used by those familiar with another. We introduce Lem, a language for engineering reusable large-scale semantic models. The Lem design takes inspiration both from functional programming languages and from proof assistants, and Lem definitions are translatable into OCaml for testing, Coq, HOL4, and Isabelle/HOL for proof, and LaTeX and HTML for presentation. This requires a delicate balance of expressiveness, careful library design, and implementation of transformations - akin to compilation, but subject to the constraint of producing usable and human-readable code for each target. Lem's effectiveness is demonstrated by its use in practice. © 2014 ACM.
2014-12-09T10:33:34Z
Simple, efficient, sound and complete combinator parsing for all context-free grammars, using an oracle
Ridge, Tom
http://hdl.handle.net/2381/29327
2015-10-01T01:45:07Z
2014-12-09T10:20:37Z
Title: Simple, efficient, sound and complete combinator parsing for all context-free grammars, using an oracle
Authors: Ridge, Tom
Abstract: Parsers for context-free grammars can be implemented directly and naturally in a functional style known as “combinator parsing”, using recursion following the structure of the grammar rules. Traditionally parser combinators have struggled to handle all features of context-free grammars, such as left recursion.
Previous work introduced novel parser combinators that could be used to parse all context-free grammars. A parser generator built using these combinators was proved both sound and complete in the HOL4 theorem prover. Unfortunately the performance was not as good as other parsing methods such as Earley parsing.
In this paper, we build on this previous work, and combine it in novel ways with existing parsing techniques such as Earley parsing. The result is a sound-and-complete combinator parsing library that can handle all context-free grammars, and has good performance.
Description: timestamp: Tue, 09 Sep 2014 10:57:11 +0200 biburl: http://dblp.uni-trier.de/rec/bib/conf/sle/Ridge14 bibsource: dblp computer science bibliography, http://dblp.org
2014-12-09T10:20:37Z
Succinct indices for range queries with applications to orthogonal range maxima
Farzan, Arash
Munro, J. Ian
Raman, Rajeev
http://hdl.handle.net/2381/29206
2014-10-29T02:01:32Z
2014-10-28T10:40:48Z
Title: Succinct indices for range queries with applications to orthogonal range maxima
Authors: Farzan, Arash; Munro, J. Ian; Raman, Rajeev
Abstract: We consider the problem of preprocessing N points in 2D, each endowed with a priority, to answer the following queries: given a axis-parallel rectangle, determine the point with the largest priority in the rectangle. Using the ideas of the effective entropy of range maxima queries and succinct indices for range maxima queries, we obtain a structure that uses O(N) words and answers the above query in O(logN loglogN) time. This a direct improvement of Chazelle's result from 1985 [10] for this problem - Chazelle required O(N/ε) words to answer queries in O((logN)[superscript 1+ε]) time for any constant ε > 0.
2014-10-28T10:40:48Z
Succinct representations of ordinal trees
Raman, Rajeev
Rao, S. Srinivasa
http://hdl.handle.net/2381/29205
2014-10-29T02:01:31Z
2014-10-28T10:33:36Z
Title: Succinct representations of ordinal trees
Authors: Raman, Rajeev; Rao, S. Srinivasa
Abstract: We survey succinct representations of ordinal, or rooted, ordered trees. Succinct representations use space that is close to the appropriate information-theoretic minimum, but support operations on the tree rapidly, usually in O(1) time.
2014-10-28T10:33:36Z
On probabilistic models for uncertain sequential pattern mining
Muzammal, Muhammad
Raman, Rajeev
http://hdl.handle.net/2381/29204
2015-08-07T15:51:50Z
2014-10-28T10:26:52Z
Title: On probabilistic models for uncertain sequential pattern mining
Authors: Muzammal, Muhammad; Raman, Rajeev
Editors: Cao, L.; Feng, Y.; Zhong, J.
Abstract: We study uncertainty models in sequential pattern mining. We consider situations where there is uncertainty either about a source or an event. We show that both these types of uncertainties could be modelled using probabilistic databases, and give possible-worlds semantics for both. We then describe ”interestingness” criteria based on two notions of frequentness (previously studied for frequent itemset mining) namely expected support [C. Aggarwal et al. KDD’09;Chui et al., PAKDD’07,’08] and probabilistic frequentness [Bernecker et al., KDD’09]. We study the interestingness criteria from a complexity-theoretic perspective, and show that in case of source-level uncertainty, evaluating probabilistic frequentness is #P-complete, and thus no polynomial time algorithms are likely to exist, but evaluate the interestingness predicate in polynomial time in the remaining cases.
2014-10-28T10:26:52Z
Encodings for range selection and top-k queries
Grossi, Roberto
Iacono, John
Navarro, Gonzalo
Raman, Rajeev
Rao, S. Srinivasa
http://hdl.handle.net/2381/29203
2014-10-29T02:01:30Z
2014-10-28T10:16:57Z
Title: Encodings for range selection and top-k queries
Authors: Grossi, Roberto; Iacono, John; Navarro, Gonzalo; Raman, Rajeev; Rao, S. Srinivasa
Abstract: We study the problem of encoding the positions the top-k elements of an array A[1..n] for a given parameter 1 ≤ k ≤ n. Specifically, for any i and j, we wish create a data structure that reports the positions of the largest k elements in A[i..j] in decreasing order, without accessing A at query time. This is a natural extension of the well-known encoding range-maxima query problem, where only the position of the maximum in A[i..j] is sought, and finds applications in document retrieval and ranking. We give (sometimes tight) upper and lower bounds for this problem and some variants thereof.
2014-10-28T10:16:57Z