HASLab - Indexed Articles in Journals

Permanent URI for this collection

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

Browse

Browsing HASLab - Indexed Articles in Journals by Author "5603"
  • 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 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
    Data governance: Organizing data for trustworthy Artificial Intelligence
    ( 2020) Brous,P ; Janssen,M ; Janowski,T ; Luís Soares Barbosa ; Estevez,E ; 5603
    The rise of Big, Open and Linked Data (BOLD) enables Big Data Algorithmic Systems (BDAS) which are often based on machine learning, neural networks and other forms of Artificial Intelligence (AI). As such systems are increasingly requested to make decisions that are consequential to individuals, communities and society at large, their failures cannot be tolerated, and they are subject to stringent regulatory and ethical requirements. However, they all rely on data which is not only big, open and linked but varied, dynamic and streamed at high speeds in real-time. Managing such data is challenging. To overcome such challenges and utilize opportunities for BDAS, organizations are increasingly developing advanced data governance capabilities. This paper reviews challenges and approaches to data governance for such systems, and proposes a framework for data governance for trustworthy BDAS. The framework promotes the stewardship of data, processes and algorithms, the controlled opening of data and algorithms to enable external scrutiny, trusted information sharing within and between organizations, risk-based governance, system-level controls, and data control through shared ownership and self-sovereign identities. The framework is based on 13 design principles and is proposed incrementally, for a single organization and multiple networked organizations.
  • Item
    Generalising KAT to Verify Weighted Computations
    ( 2019) HASLab INESC TEC,Universidade do Minho,R. da Universidade,4710-057 Braga,Portugal, ; CIDMA,Universidade de Aveiro,Campus Universitario de Santiago,3810-193 Aveiro,Portugal, ; Luís Soares Barbosa ; Madeira,A ; Leandro Rafael Gomes ; Universidade do Minho,R. da Universidade,4710-057 Braga,Portugal & Quantum Software Engineering Group,INL, ; 6759 ; 5603
    Kleene algebra with tests (KAT) was introduced as an algebraic structure to model and reason about classic imperative programs, i.e. sequences of discrete transitions guarded by Boolean tests. This paper introduces two generalisations of this structure able to express programs as weighted transitions and tests with outcomes in non necessarily bivalent truth spaces: graded Kleene algebra with tests (GKAT) and a variant where tests are also idempotent (I-GKAT). In this context, and in analogy to Kozen's encoding of Propositional Hoare Logic (PHL) in KAT we discuss the encoding of a graded PHL in I-GKAT and of its while-free fragment in GKAT. Moreover, to establish semantics for these structures four new algebras are defined: FSET(T), FREL(K,T) and FLANG(K,T) over complete residuated lattices K and T, and M (n, A) over a GKAT or I-GKAT A. As a final exercise, the paper discusses some program equivalence proofs in a graded context.
  • Item
    Hierarchical Hybrid Logic
    ( 2018) Renato Jorge Neves ; Luís Soares Barbosa ; Martins,MA ; Alexandre Castro Madeira ; 5603 ; 5620 ; 6181
    We introduce HHL, a hierarchical variant of hybrid logic. We study first order correspondence results and prove a Hennessy-Milner like theorem relating (hierarchical) bisimulation and modal equivalence for HHL. Combining hierarchical transition structures with the ability to refer to specific states at different levels, this logic seems suitable to express and verify properties of hierarchical transition systems, a pervasive semantic structure in Computer Science.
  • Item
    Languages and models for hybrid automata: A coalgebraic perspective
    ( 2018) Luís Soares Barbosa ; Renato Jorge Neves ; 6181 ; 5603
    We study hybrid automata from a coalgebraic point of view. We show that such a perspective supports a generic theory of hybrid automata with a rich palette of definitions and results. This includes, among other things, notions of bisimulation and behaviour, state minimisation techniques, and regular expression languages.
  • Item
    Simulation of Nonradiative Energy Transfer in Photosynthetic Systems Using a Quantum Computer
    ( 2020) Carlos Eduardo Tavares ; Guimaraes,JD ; Luís Soares Barbosa ; Vasilevskiy,MI ; 4852 ; 5603
    Photosynthesis is an important and complex physical process in nature, whose comprehensive understanding would have many relevant industrial applications, for instance, in the field of energy production. In this paper, we propose a quantum algorithm for the simulation of the excitonic transport of energy, occurring in the first stage of the process of photosynthesis. The algorithm takes in account the quantum and environmental effects (pure dephasing), influencing the quantum transport. We performed quantum simulations of such phenomena, for a proof of concept scenario, in an actual quantum computer, IBM Q, of 5 qubits. We validate the results with the Haken-Ströbl model and discuss the influence of environmental parameters on the efficiency of the energy transport.
  • Item
    A taxonomy for planning and designing smart mobility services
    ( 2018) Estevez,E ; Guillermina Cledou ; Luís Soares Barbosa ; 5603 ; 6193