Cookies
O website necessita de alguns cookies e outros recursos semelhantes para funcionar. Caso o permita, o INESC TEC irá utilizar cookies para recolher dados sobre as suas visitas, contribuindo, assim, para estatísticas agregadas que permitem melhorar o nosso serviço. Ver mais
Aceitar Rejeitar
  • Menu
    Factos & Números
    000
    Apresentação

    Laboratório de Software Confiável

    O HASLab dedica-se à criação e à implementação de sistemas de software confiável, i.e., software correto e resiliente perante falhas e ataques.

    De forma a cumprir este grande objetivo, o HASLab opera em três grandes áreas - Cibersegurança, Sistemas Distribuídos e Engenharia de Software.

    Engenharia de Software - são explorados métodos, técnicas e ferramentas para o desenvolvimento de software, podendo este ser integrado nas funcionalidades internas de determinados componentes, na sua configuração junto de outros componentes, e também na interação com o utilizador.

    Sistemas Distribuídos - com vista a melhorar a confiabilidade e a escalabilidade de software, explorando as propriedades inerentes à distribuição e à replicação de sistemas computacionais.

    Cibersegurança - de forma a minimizar a vulnerabilidade dos componentes de software a ataques, com recurso à implementação de estruturas e de protocolos criptográficos com propriedades de segurança formalmente comprovadas.

    Através de uma abordagem multidisciplinar que assenta em princípios teóricos comprovados, o HASLab visa disponibilizar soluções - fundamentos teóricos, métodos, linguagens, ferramentas - para o desenvolvimento de sistemas TIC abrangentes, dando garantias aos seus proprietários e utilizadores. Os grandes domínios de aplicação da investigação desenvolvida no HASLab incluem o desenvolvimento de sistemas de software cruciais para garantir a segurança e a proteção, a operacionalização de infraestruturas da nuvem seguras, e a gestão e o tratamento de big data, tendo em conta as questões da privacidade.

    006

    Projetos Selecionados

    BringTrust

    Strengthening CI/CD Pipeline Cybersecurity and Safeguarding the Intellectual Property

    2025-2028

    DisaggregatedHPC

    Towards energy-efficient, software-managed resource disaggregation in HPC infrastructures

    2025-2026

    InfraGov

    InfraGov: A Public Framework for Reliable and Secure IT Infrastructure

    2025-2026

    ENSCOMP4

    Ensino de Ciência da Computação nas Escolas 4

    2024-2025

    PFAI4_5eD

    Programa de Formação Avançada Industria 4 - 5a edição

    2024-2024

    QuantELM

    QuantELM: from Ultrafast optical processors to Quantum Extreme Learning Machines with integrated optics

    2023-2024

    Equipa
    Alcino Cunha

    Coordenador de Centro

    António Luís Sousa

    Coordenador de Centro

    Catarina Leones Fernandes

    Adjunto da Coordenação de Centro

    ViewClose Alphabet
    • a
    • b
    • c
    • d
    • e
    • f
    • g
    • h
    • i
    • j
    • k
    • l
    • m
    • n
    • o
    • p
    • q
    • r
    • s
    • t
    • u
    • v
    • w
    • x
    • y
    • z
    001

    Laboratório

    CLOUDinha

    Publicações

    HASLab Publicações

    Ler todas as publicações

    2020

    Quantum Bayesian decision-making

    Autores
    Oliveira, Md; Barbosa, LS;

    Publicação
    CoRR

    Abstract

    2020

    Sequence Mining for Automatic Generation of Software Tests from GUI Event Traces

    Autores
    Oliveira, A; Freitas, R; Jorge, A; Amorim, V; Moniz, N; Paiva, ACR; Azevedo, PJ;

    Publicação
    Intelligent Data Engineering and Automated Learning - IDEAL 2020 - 21st International Conference, Guimaraes, Portugal, November 4-6, 2020, Proceedings, Part II

    Abstract
    In today’s software industry, systems are constantly changing. To maintain their quality and to prevent failures at controlled costs is a challenge. One way to foster quality is through thorough and systematic testing. Therefore, the definition of adequate tests is crucial for saving time, cost and effort. This paper presents a framework that generates software test cases automatically based on user interaction data. We propose a data-driven software test generation solution that combines the use of frequent sequence mining and Markov chain modeling. We assess the quality of the generated test cases by empirically evaluating their coverage with respect to observed user interactions and code. We also measure the plausibility of the distribution of the events in the generated test sets using the Kullback-Leibler divergence. © 2020, Springer Nature Switzerland AG.

    FecharLer Abstract

    2020

    Validating the Hybrid ERTMS/ETCS Level 3 concept with Electrum

    Autores
    Cunha, A; Macedo, N;

    Publicação
    Int. J. Softw. Tools Technol. Transf.

    Abstract
    This paper reports on the development of a formal model for the Hybrid ERTMS/ETCS Level 3 concept in Electrum, a lightweight formal specification language that extends Alloy with mutable relations and temporal logic operators. We show how Electrum and its Analyzer can be used to perform scenario exploration to validate this model, namely to check that all the operational scenarios described in the reference document are admissible, and to reason about expected safety properties, which can be easily specified and model checked for arbitrary track configurations. We also show how the Analyzer can be used to depict scenarios (and counter-examples) in a graphical notation that is logic-agnostic, making them understandable by stakeholders without expertise in formal specification. © 2019, Springer-Verlag GmbH Germany, part of Springer Nature.

    FecharLer Abstract

    2020

    Validating Multiple Variants of an Automotive Light System with Electrum

    Autores
    Cunha, A; Macedo, N; Liu, C;

    Publicação
    Rigorous State-Based Methods - 7th International Conference, ABZ 2020, Ulm, Germany, May 27-29, 2020, Proceedings

    Abstract
    This paper reports on the development and validation of a formal model for an automotive adaptive exterior lights system (ELS) with multiple variants in Electrum, a lightweight formal specification language that extends Alloy with mutable relations and temporal logic. We explore different strategies to address variability, one in pure Electrum and another through an annotative language extension. We then show how Electrum and its Analyzer can be used to validate systems of this nature, namely by checking that the reference scenarios are admissible, and to automatically verify whether the established requirements hold. A prototype was developed to translate the provided validation sequences into Electrum and back to further automate the validation process. The resulting ELS model was validated against the provided validation sequences and verified for most of requirements for all variants. © Springer Nature Switzerland AG 2020.

    FecharLer Abstract

    2020

    Verification of system-wide safety properties of ROS applications

    Autores
    Carvalho, R; Cunha, A; Macedo, N; Santos, A;

    Publicação
    2020 IEEE/RSJ INTERNATIONAL CONFERENCE ON INTELLIGENT ROBOTS AND SYSTEMS (IROS)

    Abstract
    Robots are currently deployed in safety-critical domains but proper techniques to assess the functional safety of their software are yet to be adopted. This is particularly critical in ROS, where highly configurable robots are built by composing third-party modules. To promote adoption, we advocate the use of lightweight formal methods, automatic techniques with minimal user input and intuitive feedback. This paper proposes a technique to automatically verify system-wide safety properties of ROS-based applications at static time. It is based in the formalization of ROS architectural models and node behaviour in Electrum, over which system-wide specifications are subsequently model checked. To automate the analysis, it is deployed as a plug-in for HAROS, a framework for the assessment of ROS software quality aimed at the ROS community. The technique is evaluated in a real robot, AgRob V16, with positive results.

    FecharLer Abstract

    Factos & Números

    4Artigos em revistas indexadas

    2020

    14Artigos em conferências indexadas

    2020

    16Docentes do Ensino Superior

    2020

    Ver todos os Factos & Números
    Contactos
    António Luís Sousa

    -

    +351253604440

    antonio.l.sousa@inesctec.pt

    Alcino Cunha

    Coordenado de Centro

    +351253604440

    alcino.cunha@inesctec.pt