HASLab - Indexed Articles in Journals

Permanent URI for this collection

http://localhost:4000/handle/123456789/167

Browse

Browsing HASLab - Indexed Articles in Journals by Title

  • 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
    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
    Anomaly Detection and Modeling in 802.11 Wireless Networks
    ( 2019) Anisa Allahdadidastjerdi ; Ricardo Morla ; 3645 ; 5587
  • 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
    Balancing the formal and the informal in user-centred design
    ( 2021) José Creissac Campos ; Harrison,MD ; Masci,P ; 5599
  • Item
    The benefits of formalising design guidelines: a case study on the predictability of drug infusion pumps
    ( 2015) Paolo Masci ; Ruksenas,Rimvydas ; Oladimeji,Patrick ; Cauchi,Abigail ; Gimblett,Andy ; Li,KarenYunqiu ; Curzon,Paul ; Thimbleby,HaroldW.
    A demonstration is presented of how automated reasoning tools can be used to check the predictability of a user interface. Predictability concerns the ability of a user to determine the outcomes of their actions reliably. It is especially important in situations such as a hospital ward where medical devices are assumed to be reliable devices by their expert users (clinicians) who are frequently interrupted and need to quickly and accurately continue a task. There are several forms of predictability. A definition is considered where information is only inferred from the current perceptible output of the system. In this definition, the user is not required to remember the history of actions that led to the current state. Higher-order logic is used to specify predictability, and the Symbolic Analysis Laboratory is used to automatically verify predictability on real interactive number entry systems of two commercial drug infusion pumps—devices used in the healthcare domain to deliver fluids (e.g., medications, nutrients) into a patient’s body in controlled amounts. Areas of unpredictability are precisely identified with the analysis. Verified solutions that make an unpredictable system predictable are presented through design modifications and verified user strategies that mitigate against the identified issues. © 2013, Springer-Verlag London.
  • Item
    Boolean Searchable Symmetric Encryption with Filters on Trusted Hardware
    ( 2020) Portela,B ; Leitao,J ; Domingos,HJ ; Borges,G ; Tiago Filipe Oliveira ; Ferreira,B ; 6207
  • Item
    A Calculus for Generic, QoS-Aware Component Composition
    ( 2012) Luís Soares Barbosa ; Sun Meng
    Software QoS properties, such as response time, availability, bandwidth requirement, memory usage, among many others, play a major role in the processes of selecting and composing software components. This paper extends a component calculus to deal, in an effective way, with them. The calculus models components as gener- alised Mealy machines, i.e., state-based entities interacting along their life time through well defined interfaces of observers and actions. QoS is introduced through an algebraic structure specifying the relevant QoS domain and how its values are composed under different disciplines. A major effect of introducing QoS-awareness is that a number of equivalences holding in the plain calculus become refinement laws. The paper also introduces a prototyper for the calculus developed as a 'proof-of-concept' implementation
  • Item
    CAOVerif: An open-source deductive verification platform for cryptographic software implementations
    ( 2014) José Bacelar Almeida ; Manuel Barbosa ; Filliatre,JC ; Jorge Sousa Pinto ; Vieira,B
    CAO is a domain-specific imperative language for cryptography, offering a rich mathematical type system and crypto-oriented language constructions. We describe the design and implementation of a deductive verification platform for CAO and demonstrate that the development time of such a complex verification tool could be greatly reduced by building on the Jessie plug-in included in the Frama-C framework. We discuss the interesting challenges raised by the domain-specific characteristics of CAO, and describe how we tackle these problems in our design. We base our presentation on real-world examples of CAO code, extracted from the open-source code of the NaCl cryptographic library, and illustrate how various cryptography-relevant security properties can be verified.
  • Item
    A Case for Partitioned Bloom Filters
    ( 2022) Paulo Sérgio Almeida ; 5607
  • Item
    Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations
    ( 2013) Manuel Barbosa ; José Bacelar Almeida ; Barthe,G ; Dupressoir,F ; 5604 ; 5598
  • Item
    CloudMdsQL: querying heterogeneous cloud data stores with a common language
    ( 2016) Kolev,B ; Valduriez,P ; Bondiombouy,C ; Jimenez Peris,R ; Pau,R ; José Orlando Pereira
    The blooming of different cloud data management infrastructures, specialized for different kinds of data and tasks, has led to a wide diversification of DBMS interfaces and the loss of a common programming paradigm. In this paper, we present the design of a cloud multidatastore query language (CloudMdsQL), and its query engine. CloudMdsQL is a functional SQL-like language, capable of querying multiple heterogeneous data stores (relational and NoSQL) within a single query that may contain embedded invocations to each data store's native query interface. The query engine has a fully distributed architecture, which provides important opportunities for optimization. The major innovation is that a CloudMdsQL query can exploit the full power of local data stores, by simply allowing some local data store native queries (e.g. a breadth-first search query against a graph database) to be called as functions, and at the same time be optimized, e.g. by pushing down select predicates, using bind join, performing join ordering, or planning intermediate data shipping. Our experimental validation, with three data stores (graph, document and relational) and representative queries, shows that CloudMdsQL satisfies the five important requirements for a cloud multidatastore query language.
  • Item
    Coalgebra for the working software engineer
    ( 2022) Luís Soares Barbosa ; 5603
    Often referred to as ‘the mathematics of dynamical, state-based systems’, Coalgebra claims to provide a compositional and uniform framework to specify, analyse and reason about state and behaviour in computing. This paper addresses this claim by discussing why Coalgebra matters for the design of models and logics for computational phenomena. To a great extent, in this domain one is interested in properties that are preserved along the system’s evolution, the so-called ‘business rules’ or system’s invariants, as well as in liveness requirements, stating that e.g. some desirable outcome will be eventually produced. Both classes are examples of modal assertions, i.e. properties that are to be interpreted across a transition system capturing the system’s dynamics. The relevance of modal reasoning in computing is witnessed by the fact that most university syllabi in the area include some incursion into modal logic, in particular in its temporal variants. The novelty is that, as it happens with the notions of transition, behaviour, or observational equivalence, modalities in Coalgebra acquire a shape. That is, they become parametric on whatever type of behaviour, and corresponding coinduction scheme, seems appropriate for addressing the problem at hand. In this context, the paper revisits Coalgebra from a computational perspective, focussing on three topics central to software design: how systems are modelled, how models are composed, and finally, how properties of their behaviours can be expressed and verified. © 2022, College Publications. All rights reserved.
  • 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
    A Coalgebraic Perspective on Logical Interpretations
    ( 2013) Martins,MA ; Alexandre Castro Madeira ; Luís Soares Barbosa
    In Computer Science stepwise refinement of algebraic specifications is a well-known formal methodology for rigorous program development. This paper illustrates how techniques from Algebraic Logic, in particular that of interpretation, understood as a multifunction that preserves and reflects logical consequence, capture a number of relevant transformations in the context of software design, reuse, and adaptation, difficult to deal with in classical approaches. Examples include data encapsulation and the decomposition of operations into atomic transactions. But if interpretations open such a new research avenue in program refinement, (conceptual) tools are needed to reason about them. In this line, the paper's main contribution is a study of the correspondence between logical interpretations and morphisms of a particular kind of coalgebras. This opens way to the use of coalgebraic constructions, such as simulation and bisimulation, in the study of interpretations between (abstract) logics.
  • Item
    A component-based framework for certification of components in a cloud of HPC services
    ( 2020) de Carvalho Junior,FH ; de Oliveira Dantas,ABD ; Luís Soares Barbosa ; 5603
    HPC Shelf is a proposal of a cloud computing platform to provide component-oriented services for High Performance Computing (HPC) applications. This paper presents a Verification-as-a-Service (VaaS) framework for component certification on HPC Shelf. Certification is aimed at providing higher confidence that components of parallel computing systems of HPC Shelf behave as expected according to one or more requirements expressed in their contracts. To this end, new abstractions are introduced, starting with certifier components. They are designed to inspect other components and verify them for different types of functional, non-functional and behavioral requirements. The certification framework is naturally based on parallel computing techniques to speed up verification tasks. © 2019
  • Item
    Composing Least-change Lenses
    ( 2013) Nuno Moreira Macedo ; Hugo Pereira Pacheco ; Alcino Cunha ; Oliveira,JN
  • Item
    Computer Aided Verification of Relational Models by Strategic Rewriting
    ( 2017) Visser,J ; Uzal,R ; Necco,CM ; José Nuno Oliveira ; 5601
    Binary relational algebra provides semantic foundations for major areas of computing, such as database design, state-based modeling and functional programming. Remarkably, static checking support in these areas fails to exploit the full semantic content of relations. In particular, properties such as the simplicity or injectivity of relations are not statically enforced in operations such as database queries, state transitions, or composition of functional components. When data models, their constraints and operations are represented by point-free binary relational expressions, proof obligations can be expressed as inclusions between relational expressions. We developed a type-directed, strategic term rewriting system that can be used to simplify relational proof obligations and ultimately reduce them to tautologies. Such reductions can be used to provide extended static checking for design contraints commonly found in software modeling and development.
  • Item
    Concurrency Debugging with Differential Schedule Projections
    ( 2016) Nuno Almeida Machado ; Quinta,Daniel ; Lucia,Brandon ; Rodrigues,LuisE.T.
    We present Symbiosis: a concurrency debugging technique based on novel differential schedule projections (DSPs). A DSP shows the small set of memory operations and dataflows responsible for a failure, as well as a reordering of those elements that avoids the failure. To build a DSP, Symbiosis first generates a full, failing, multithreaded schedule via thread path profiling and symbolic constraint solving. Symbiosis selectively reorders events in the failing schedule to produce a nonfailing, alternate schedule. A DSP reports the ordering and dataflow differences between the failing and nonfailing schedules. Our evaluation on buggy real-world software and benchmarks shows that, in practical time, Symbiosis generates DSPs that both isolate the small fraction of event orders and dataflows responsible for the failure and report which event reorderings prevent failing. In our experiments, DSPs contain 90% fewer events and 96% fewer dataflows than the full failure-inducing schedules. We also conducted a user study that shows that, by allowing developers to focus on only a few events, DSPs reduce the amount of time required to understand the bug's root cause and find a valid fix. © 2016 ACM.