HASLab
Permanent URI for this community
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
Results Per Page
Sort Options
-
ItemWorldwide Consensus( 2011) José Orlando Pereira ; Francisco Almeida Maia ; Miguel Marques Matos ; Rui Carlos OliveiraConsensus 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.
-
ItemVerification Conditions for Source-level Imperative Programs( 2011) Jorge Sousa Pinto ; Maria João Frade
-
ItemMarkov random walk under constraint for discovering overlapping communities in complex networks( 2011) Carlos Baquero ; Bo Yang ; Di Jin ; Jie Liu ; Dongxiao He ; Dayou Liu
-
ItemFast Distributed Estimation of Sums and Network Sizes( 2011) Raquel Menezes ; Carlos Baquero ; Paulo Sérgio Almeida
-
ItemPrioritizing Tests for Software Fault Diagnosis( 2011) Arjan J.C. van Gemund ; Alberto Gonzalez-Sanchez ; Éric Piel ; Rui Maranhão ; Hans-Gerhard Gross
-
ItemTransformation of Structure-Shy Programs with Application to XPath Queries and Strategic Functions, I( 2011) Alcino Cunha ; Joost Visser
-
ItemSimultaneous Debugging of Software Faults( 2011) Rui Maranhão ; Arjan J.C. van Gemund ; Peter Zoeteweij
-
ItemTime Series Motifs Statistical Signi cance( 2011) Paulo Jorge Azevedo ; Nuno Constantino Castro
-
ItemConvergent and Commutative Replicated Data Types( 2011) Nuno Preguiça ; Carlos Baquero ; Marek Zawirski ; Marc Shapiro
-
ItemSafe Controllers Design for Industrial Automation Systems( 2011) Celina Leão ; José Machado ; Eurico Seabra ; José Creissac Campos ; Filomena SoaresThe 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
-
ItemA coalgebraic perspective on linear weighted automata( 2012) Filippo Bonchi ; Alexandra Silva ; Jan Rutten ; Michele Boreale ; Marcello BonsangueWeighted 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
-
ItemSignificant Motifs in Time Series( 2012) Nuno Constantino Castro ; Paulo Jorge Azevedo
-
ItemAssertion-based Slicing and Slice Graphs( 2012) Daniela Cruz ; José Bernardo Barros ; Jorge Sousa Pinto ; Pedro Rangel HenriquesThis 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.
-
ItemOnline 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
-
ItemProgramming from Galois connections( 2012) José Nuno Oliveira ; Shin-Cheng Mu
-
ItemShortcut Fusion Rules for the Derivation of Circular and Higher-order Programs( 2012) João Alexandre Saraiva ; João Paulo Fernandes ; Alberto PardoFunctional 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:
-
ItemBRISA: Combining Efficiency and Reliability in Epidemic Data Dissemination( 2012) Valerio Schiavoni ; Rui Carlos Oliveira ; Etienne Riviere ; Miguel Marques Matos ; Pascal Felber
-
ItemMapIt: A Model Based Pattern Recovery Tool( 2012) José Creissac Campos ; António Nestor Ribeiro ; Rui Miguel CoutoDesign 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.
-
ItemAI for the Win: Improving Spectrum-based Fault Localization( 2012) Birgit Hofer ; Franz Wotawa ; Rui MaranhãoA 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
-
ItemA literature review about usability evaluation methods for e-learning platforms( 2012) NomeLuciana Lopes Freire ; José Creissac Campos ; Pedro Miguel ArezesThe 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,