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 Issue Date

Jump to a point in the index:
  • Item
    Worldwide Consensus
    ( 2011) José Orlando Pereira ; Francisco Almeida Maia ; Miguel Marques Matos ; Rui Carlos Oliveira
    Consensus is an abstraction of a variety of important challenges in dependable distributed systems. Thus a large body of theoretical knowledge is focused on modeling and solving consensus within diff erent system assumptions. However, moving from theory to practice imposes compromises and design decisions that may impact the elegance, trade-o ffs and correctness of theoretical appealing consensus protocols. In this paper we present the implementation and detailed analysis, in a real environment with a large number of nodes, of mutable consensus, a theoretical appealing protocol able to o ffer a wide range of trade-o ffs (called mutations) between decision latency and message complexity. The analysis sheds light on the fundamental behavior of the mutations, and leads to the identi cation of problems related to the real environment. Such problems are addressed without ever a ffecting the correctness of the theoretical proposal.
  • Item
    Verification Conditions for Source-level Imperative Programs
    ( 2011) Jorge Sousa Pinto ; Maria João Frade
  • Item
    Markov random walk under constraint for discovering overlapping communities in complex networks
    ( 2011) Carlos Baquero ; Bo Yang ; Di Jin ; Jie Liu ; Dongxiao He ; Dayou Liu
  • Item
    Fast Distributed Estimation of Sums and Network Sizes
    ( 2011) Raquel Menezes ; Carlos Baquero ; Paulo Sérgio Almeida
  • Item
    Prioritizing Tests for Software Fault Diagnosis
    ( 2011) Arjan J.C. van Gemund ; Alberto Gonzalez-Sanchez ; Éric Piel ; Rui Maranhão ; Hans-Gerhard Gross
  • Item
  • Item
    Simultaneous Debugging of Software Faults
    ( 2011) Rui Maranhão ; Arjan J.C. van Gemund ; Peter Zoeteweij
  • Item
    Time Series Motifs Statistical Signi cance
    ( 2011) Paulo Jorge Azevedo ; Nuno Constantino Castro
  • Item
    Convergent and Commutative Replicated Data Types
    ( 2011) Nuno Preguiça ; Carlos Baquero ; Marek Zawirski ; Marc Shapiro
  • Item
    Safe Controllers Design for Industrial Automation Systems
    ( 2011) Celina Leão ; José Machado ; Eurico Seabra ; José Creissac Campos ; Filomena Soares
    The design of safe industrial controllers is one of the most important domains related to Automation Systems research. To support it, synthesis and analysis techniques are available. Among the analysis techniques, two of the most important are Simulation and Formal Verification. In this paper these two techniques are used together in a complementary way. Understanding plant behaviour is essential for obtaining safe industrial systems controllers; hence, plant modelling is crucial to the success of these techniques. A two step approach is presented: first, the use of Simulation and, second, the use of Formal Verification of Industrial Systems Specifications. The specification and plant models used for each technique are described. Simulation and Formal Verification results are presented and discussed. The approach presented in the paper can be applied to real industrial systems, and obtain safe controllers for hybrid plants. The Modelica modelling language and Dymola simulation environm
  • Item
    A coalgebraic perspective on linear weighted automata
    ( 2012) Filippo Bonchi ; Alexandra Silva ; Jan Rutten ; Michele Boreale ; Marcello Bonsangue
    Weighted automata are a generalisation of non-deterministic automata where each transition, in addition to an input letter, has also a quantity expressing the weight (e.g. cost or probability) of its execution. As for non-deterministic automata, their behaviours can be expressed in terms of either (weighted) bisimilarity or (weighted) language equivalence. Coalgebras provide a categorical framework for the uniform study of state-based systems and their behaviours. In this work, we show that coalgebras can suitably model weighted automata in two different ways: coalgebras on SetSet (the category of sets and functions) characterise weighted bisimilarity, while coalgebras on VectVect (the category of vector spaces and linear maps) characterise weighted language equivalence. Relying on the second characterisation, we show three different procedures for computing weighted language equivalence. The first one consists in a generalisation of the usual partition refinement algorithm for ordi
  • Item
    Significant Motifs in Time Series
    ( 2012) Nuno Constantino Castro ; Paulo Jorge Azevedo
  • Item
    Assertion-based Slicing and Slice Graphs
    ( 2012) Daniela Cruz ; José Bernardo Barros ; Jorge Sousa Pinto ; Pedro Rangel Henriques
    This paper revisits the idea of slicing programs based on their axiomatic semantics, rather than using criteria based on control/data dependencies. We show how the forward propagation of preconditions and the backward propagation of post conditions can be combined in a new slicing algorithm that is more precise than the existing specification-based algorithms. The algorithm is based on (i) a precise test for removable statements, and (ii) the construction of a slice graph, a program control flow graph extended with semantic labels. It improves on previous approaches in two aspects: it does not fail to identify removable commands; and it produces the smallest possible slice that can be obtained (in a sense that will be made precise). The paper also reviews in detail, through examples, the ideas behind the use of preconditions and post conditions for slicing programs.
  • Item
    Online Spectrum-based Fault Localization for Health Monitoring and Fault Recovery of Self-Adaptive Systems
    ( 2012) Alberto Gonzalez-Sanchez ; Éric Piel ; Rui Maranhão ; Arjan J. C. van Gemund ; Hans-Gerhard Gross
  • Item
    Programming from Galois connections
    ( 2012) José Nuno Oliveira ; Shin-Cheng Mu
  • Item
    Shortcut Fusion Rules for the Derivation of Circular and Higher-order Programs
    ( 2012) João Alexandre Saraiva ; João Paulo Fernandes ; Alberto Pardo
    Functional programs often combine separate parts using interme- diate data structures for communicating results. These programs are modular, easier to understand and maintain, but suffer from in- efficiencies due to the generation of those gluing data structures. To eliminate such redundant data structures, some program trans- formation techniques have been proposed. One such technique is shortcut fusion, and has been studied in the context of both pure and monadic functional programs. Recently, we have extended standard shortcut fusion: in addition to intermediate structures, the program parts may now communi- cate context information, and it still is possible to eliminate those structures. This is achieved by transforming the original function composition into a circular program. This new technique, however, has been studied in the context of purely functional programs only. In this paper, we propose an extension to this new form of fusion, but in the context of monadic programming:
  • Item
    BRISA: Combining Efficiency and Reliability in Epidemic Data Dissemination
    ( 2012) Valerio Schiavoni ; Rui Carlos Oliveira ; Etienne Riviere ; Miguel Marques Matos ; Pascal Felber
  • Item
    MapIt: A Model Based Pattern Recovery Tool
    ( 2012) José Creissac Campos ; António Nestor Ribeiro ; Rui Miguel Couto
    Design patterns provide a means to reuse proven solutions during development, but also to identify good practices during analysis. These are particularly relevant in complex and critical software, such as is the case of ubiquitous and pervasive systems. Model Driven Engineering (MDE) presents a solution for this problem, with the usage of high level models. As part of an effort to develop approaches to the migration of applications to mobile contexts, this paper reports on a tool that identifies design patterns in source code. Code is transformed into both platform specific and independent models, and from these design patterns are inferred. MapIt, the tool which implements these functionalities is described.
  • 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
    A literature review about usability evaluation methods for e-learning platforms
    ( 2012) NomeLuciana Lopes Freire ; José Creissac Campos ; Pedro Miguel Arezes
    The usability analysis of information systems has been the target of several research studies over the past thirty years. These studies have highlighted a great diversity of points of view, including researchers from different scientific areas such as Ergonomics, Computer Science, Design and Education. Within the domain of information ergonomics, the study of tools and methods used for usability evaluation dedicated to E-learning presents evidence that there is a continuous and dynamic evolution of E-learning systems, in many different contexts -academics and corporative. These systems, also known as LMS (Learning Management Systems), can be classified according to their educational goals and their technological features. However, in these systems the usability issues are related with the relationship/interactions between user and system in the user's context. This review is a synthesis of research project about Information Ergonomics and embraces three dimensions, namely the methods,