HASLab

Permanent URI for this community

http://localhost:4000/handle/123456789/30
This service produces reliable software systems in contexts where correctness, responsiveness, robustness and security are essential. It develops integrated research in three lines: formal methods for software development, reliable distributed systems and information security.

Browse

Browsing HASLab by Title

  • Item
    Accelerating Deep Learning Training Through Transparent Storage Tiering
    ( 2022) Dantas,M ; Leitao,D ; Cui,P ; Ricardo Gonçalves Macedo ; Liu,XL ; Xu,WJ ; João Tiago Paulo ; 5621 ; 6941
  • Item
    Adaptive Broadcast Cancellation Query Mechanism for Unstructured Networks
    ( 2015) Lima,R ; Carlos Baquero ; Miranda,H
    The availability of cheap wireless sensors boosted the emergence of unstructured networks using wireless technologies with decentralised administration. However, a simple task such as learning the temperature needs a discovery service to find a thermometer among all the sensors. In general, resource discovery relies on flooding mechanisms that waste energy and compromises system availability. Energy efficient strategies limit the exploration area, but with a significant impact on latency. The paper proposes ABC (Adaptive Broadcast Cancellation), a new algorithm that uses the knowledge acquired in previous discoveries to accelerate queries towards the resource. Knowledge is stored in a variation of Bloom filters, thus contributing for an efficient utilization of the sensors limited memory.
  • Item
    Adaptive database synchronization for an online analytical cioud-to-edge continuum
    ( 2022) Costa,D ; José Orlando Pereira ; Ricardo Pereira Vilaça ; Faria,N ; 5635 ; 5602
  • Item
    Addressing Interactive Computing Systems' Concerns in Software Engineering Degrees
    ( 2021) José Creissac Campos ; António Nestor Ribeiro ; 5599 ; 5639
    This paper arises from experience by the authors in teaching software engineering courses. It discusses the need for adequate coverage of Human-Computer Interaction topics in these courses and the challenges faced when addressing them. Three courses, at both licentiate and master’s levels, are used as triggers for the discussion. The paper argues that the lack of relevant Human-Computer Interaction concepts creates challenges when teaching and learning requirements analysis, design, and implementation of software systems. The approaches adopted to address these challenges are described. © 2022, IFIP International Federation for Information Processing.
  • Item
    Addressing Interactive Computing Systems' Concerns in Software Engineering Degrees
    ( 2021) José Creissac Campos ; António Nestor Ribeiro ; 5599 ; 5639
    This paper arises from experience by the authors in teaching software engineering courses. It discusses the need for adequate coverage of Human-Computer Interaction topics in these courses and the challenges faced when addressing them. Three courses, at both licentiate and master’s levels, are used as triggers for the discussion. The paper argues that the lack of relevant Human-Computer Interaction concepts creates challenges when teaching and learning requirements analysis, design, and implementation of software systems. The approaches adopted to address these challenges are described. © 2022, IFIP International Federation for Information Processing.
  • Item
    An Adequate While-Language for Hybrid Computation
    ( 2019) Renato Jorge Neves ; Goncharov,S ; 6181
    Hybrid computation harbours discrete and continuous dynamics in the form of an entangled mixture, inherently present in various natural phenomena and in applications ranging from control theory to microbiology. The emergent behaviours bear signs of both computational and physical processes, and thus present difficulties not only in their analysis, but also in describing them adequately in a structural, well-founded way. In order to tackle these issues and, more generally, to investigate hybridness as a dedicated computational phenomenon, we introduce a while-language for hybrid computation inspired by the fine-grain call-by-value paradigm. We equip it with operational and computationally adequate denotational semantics. The latter crucially relies on a hybrid monad supporting an (Elgot) iteration operator that we developed elsewhere. As an intermediate step, we introduce a more lightweight duration semantics furnished with analogous results and based on a new duration monad that we introduce as a lightweight counterpart to the hybrid monad.
  • Item
    An Adequate While-Language for Hybrid Computation
    ( 2019) Renato Jorge Neves ; Goncharov,S ; 6181
  • Item
    ADSNARK: Nearly Practical and Privacy-Preserving Proofs on Authenticated Data
    ( 2015) Backes,M ; Manuel Barbosa ; Fiore,D ; Reischuk,RM
    We study the problem of privacy-preserving proofs on authenticated data, where a party receives data from a trusted source and is requested to prove computations over the data to third parties in a correct and private way, i.e., the third party learns no information on the data but is still assured that the claimed proof is valid. Our work particularly focuses on the challenging requirement that the third party should be able to verify the validity with respect to the specific data authenticated by the source - even without having access to that source. This problem is motivated by various scenarios emerging from several application areas such as wearable computing, smart metering, or general business-to-business interactions. Furthermore, these applications also demand any meaningful solution to satisfy additional properties related to usability and scalability. In this paper, we formalize the above three-party model, discuss concrete application scenarios, and then we design, build, and evaluate ADSNARK, a nearly practical system for proving arbitrary computations over authenticated data in a privacy-preserving manner. ADSNARK improves significantly over state-of-the-art solutions for this model. For instance, compared to corresponding solutions based on Pinocchio (Oakland' 13), ADSNARK achieves up to 25x improvement in proof-computation time and a 20x reduction in prover storage space.
  • Item
    Aggregation protocols in light of reliable communication
    ( 2017) Kassam,Z ; Ali Shoker ; Paulo Sérgio Almeida ; Carlos Baquero
  • Item
    AI for the Win: Improving Spectrum-based Fault Localization
    ( 2012) Birgit Hofer ; Franz Wotawa ; Rui Maranhão
    A considerable amount of time in software engineering is spent in debugging. In practice, mainly debugging tools which allow for executing a program step-by-step and setting break points are used. This debugging method is however very time consuming and cumbersome. There is a need for tools which undertake the task of narrowing down the most likely fault locations. These tools must complete this task with as little user interaction as possible and the results computed must be beneficial so that such tools appeal to programmers. In order to come up with such tools, we present three variants of the well-known spectrum-based fault localization technique that are enhanced by using methods from Artificial Intelligence. Each of the three combined approaches outperforms the underlying basic method concerning diagnostic accuracy. Hence, the presented approaches support the hypothesis that combining techniques from different areas is beneficial. In addition to the introduction of these techniq
  • Item
    AIDA-DB: A Data Management Architecture for the Edge and Cloud Continuum
    ( 2022) Faria,N ; Costa,D ; José Orlando Pereira ; Ricardo Pereira Vilaça ; Ferreira,L ; Fábio André Coelho ; 6059 ; 5635 ; 5602
  • Item
    AJITTS: Adaptive just-in-time transaction scheduling
    ( 2013) Alonso,A ; Rui Carlos Oliveira ; José Orlando Pereira
    Distributed transaction processing has benefited greatly from optimistic concurrency control protocols thus avoiding costly fine-grained synchronization. However, the performance of these protocols degrades significantly when the workload increases, namely, by leading to a substantial amount of aborted transactions due to concurrency conflicts. Our approach stems from the observation that when the abort rate increases with the load as already executed transactions queue for longer periods of time waiting for their turn to be certified and committed. We thus propose an adaptive algorithm for judiciously scheduling transactions to minimize the time during which these are vulnerable to being aborted by concurrent transactions, thereby reducing the overall abort rate. We do so by throttling transaction execution using an adaptive mechanism based on the locally known state of globally executing transactions, that includes out-of-order execution. Our evaluation using traces from the industry standard TPC-E workload shows that the amount of aborted transactions can be kept bounded as system load increases, while at the same time fully utilizing system resources and thus scaling transaction processing throughput. © 2013 IFIP International Federation for Information Processing.
  • Item
    Alloy Meets the Algebra of Programming: A Case Study
    ( 2013) José Nuno Oliveira ; Ferreira,MA
    Relational algebra offers to software engineering the same degree of conciseness and calculational power as linear algebra in other engineering disciplines. Binary relations play the role of matrices with similar emphasis on multiplication and transposition. This matches with Alloy's lemma "everything is a relation" and with the relational basis of the Algebra of Programming (AoP). Altogether, it provides a simple and coherent approach to checking and calculating programs from abstract models. In this paper, we put Alloy and the Algebra of Programming together in a case study originating from the Verifiable File System mini-challenge put forward by Joshi and Holzmann: verifying the refinement of an abstract file store model into a journaled (FLASH) data model catering to wear leveling and recovery from power loss. Our approach relies on diagrams to graphically express typed assertions. It interweaves model checking (in Alloy) with calculational proofs in a way which offers the best of both worlds. This provides ample evidence of the positive impact in software verification of Alloy's focus on relations, complemented by induction-free proofs about data structures such as stores and lists.
  • Item
    Analysing interactive devices based on information resource constraints
    ( 2014) José Creissac Campos ; Doherty,G ; Michael Douglas Harrison
    Analysis of the usability of an interactive system requires both an understanding of how the system is to be used and a means of assessing the system against that understanding. Such analytic assessments are particularly important in safety-critical systems as latent vulnerabilities may exist which have negative consequences only in certain circumstances. Many existing approaches to assessment use tasks or scenarios to provide explicit representation of their understanding of use. These normative user behaviours have the advantage that they clarify assumptions about how the system will be used but have the disadvantage that they may exclude many plausible deviations from these norms. Assessments of how a design fails to support these user behaviours can be a matter of judgement based on individual experience rather than evidence. We present a systematic formal method for analysing interactive systems that is based on constraints rather than prescribed behaviour. These constraints capture precise assumptions about what information resources are used to perform action. These resources may either reside in the system itself or be external to the system. The approach is applied to two different medical device designs, comparing two infusion pumps currently in common use in hospitals. Comparison of the two devices is based on these resource assumptions to assess consistency of interaction within the design of each device.
  • Item
    Analysis of FLOSS communities as learning contexts
    ( 2012) Luís Soares Barbosa ; António Cerone ; Sara Santos Fernandes
    It can be argued that participating in Free/Libre Open Source Software (FLOSS) projects can have a positive effect in the contributor's learning process. The need to collaborate with other contributors and to contribute to a project can motivate and implicitly foster learning. In order to validate such statements, it is necessary to (1) study the interactions between FLOSS projects' participants, and (2) explore the didactical value of participating in FLOSS projects, designing an appropriate questionnaire asking FLOSS contributors about their experience in FLOSS projects. In this paper, we illustrate how this questionnaire was designed and disseminated. We conclude the paper with results from 27 FLOSS projects contributors, determining that, not only they contribute and collaborate to the project and its community, but also that FLOSS contributors see that this type of activity can be regarded as a complement to formal education.
  • Item
    Anomaly Detection and Modeling in 802.11 Wireless Networks
    ( 2019) Anisa Allahdadidastjerdi ; Ricardo Morla ; 3645 ; 5587
  • Item
    The ANTAREX approach to autotuning and adaptivity for energy efficient HPC systems
    ( 2016) Silvano,C ; Agosta,G ; Cherubin,S ; Gadioli,D ; Palermo,G ; Bartolini,A ; Benini,L ; Martinovic,J ; Palkovic,M ; Slaninová,K ; João Bispo ; João Paiva Cardoso ; Rui Maranhão ; Pinto,P ; Cavazzoni,C ; Sanna,N ; Beccari,AR ; Cmar,R ; Rohou,E
    The ANTAREX 1 project aims at expressing the application selfadaptivity through a Domain Specific Language (DSL) and to runtime manage and autotune applications for green and heterogeneous High Performance Computing (HPC) systems up to Exascale. The DSL approach allows the definition of energy-efficiency, performance, and adaptivity strategies as well as their enforcement at runtime through application autotuning and resource and power management. We show through a mini-App extracted from one of the project application use cases some initial exploration of application precision tuning by means enabled by the DSL. © 2016 Copyright held by the owner/author(s).
  • Item
    Application of ontologies in identifying requirements patterns in use cases
    ( 2014) Rui Miguel Couto ; António Nestor Ribeiro ; José Creissac Campos
    Use case specifications have successfully been used for requirements description. They allow joining, in the same modeling space, the expectations of the stakeholders as well as the needs of the software engineer and analyst involved in the process. While use cases are not meant to describe a system's implementation, by formalizing their description we are able to extract implementation relevant information from them. More specifically, we are interested in identifying requirements patterns (common requirements with typical implementation solutions) in support for a requirements based software development approach. In the paper we propose the transformation of Use Case descriptions expressed in a Controlled Natural Language into an ontology expressed in the Web Ontology Language (OWL). OWL's query engines can then be used to identify requirements patterns expressed as queries over the ontology. We describe a tool that we have developed to support the approach and provide an example of usage. © 2014 R. Couto, A.N. Ribeiro & J.C. Campos.
  • Item
    Applying the 3C Model to FLOSS Communities
    ( 2016) Fernandes,S ; Luís Soares Barbosa
    How learning occurs within Free/LibreOpen Source (FLOSS) communities and what is the dynamics of such projects (e.g. the life cycle of such projects) are very relevant questions when considering the use of FLOSS projects in a formal education setting. This paper introduces an approach based on the 3C collaboration model (communication, coordination and cooperation) to represent the collaborative learning dynamics within FLOSS communities. To explore the collaborative learning potential of FLOSS communities a number of questionnaires and interviews to selected FLOSS contributors were run. From this study a 3C collaborative model applicable to FLOSS communities was designed and discussed.
  • Item
    An Approach for Graphical User Interface External Bad Smells Detection
    ( 2014) Silva,JC ; José Creissac Campos ; João Alexandre Saraiva ; José Luís Silva
    In the context of an effort to develop methodologies to support the evaluation of interactive system, this paper investigates an approach to detect graphical user interface external bad smells. Our approach consists in detecting user interface external bad smells through model-based reverse engineering from source code. Models are used to define which widgets are present in the interface, when can particular graphical user interface (GUI) events occur, under which conditions, which system actions are executed, and which GUI state is generated next. From these models we obtain metrics that can later be used to identify the smells.