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
    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
    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
    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
    Simultaneous Debugging of Software Faults
    ( 2011) Rui Maranhão ; Arjan J.C. van Gemund ; Peter Zoeteweij
  • 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
    A Patterns Based Reverse Engineering Approach for Java Source Code
    ( 2012) José Creissac Campos ; Rui Miguel Couto ; António Nestor Ribeiro
    The ever increasing number of platforms and languages available to software developers means that the software industry is reaching high levels of complexity. Model Driven Architecture (MDA) presents a solution to the problem of improving software development processes in this changing and complex environment. MDA driven development is based on models definition and transformation. Design patterns provide a means to reuse proven solutions during development. Identifying design patterns in the models of a MDA approach helps their understanding, but also the identification of good practices during analysis. However, when analyzing or maintaining code that has not been developed according to MDA principles, or that has been changed independently from the models, the need arises to reverse engineer the models from the code prior to patterns' identification. The approach presented herein consists in transforming source code into models, and infer design patterns from these models. Erich Gamma's cataloged patterns provide us a starting point for the pattern inference process. MapIt, the tool which implements these functionalities is described.
  • 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,
  • Item
    WIKI::SCORE - A collaborative environment for music transcription and publishing
    ( 2012) José Nuno Oliveira ; José João Almeida ; Nuno Ramos Carvalho
    Music sources are most commonly shared in music scores scanned or printed on paper sheets. These artifacts are rich in information, but since they are images it is hard to re-use and share their content in todays' digital world. There are modern languages that can be used to transcribe music sheets, this is still a time consuming task, because of the complexity involved in the process and the typical huge size of the original documents. WIKI::SCORE is a collaborative environment where several people work together to transcribe music sheets to a shared medium, using the notation. This eases the process of transcribing huge documents, and stores the document in a well known notation, that can be used later on to publish the whole content in several formats, such as a PDF document, images or audio files for example.
  • Item
    Optimal leverage association rules with numerical interval conditions
    ( 2012) Alípio Jorge ; Paulo Jorge Azevedo
  • Item
    Towards a Linear Algebra of Programming
    ( 2012) José Nuno Oliveira