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
Sobre

Sobre

Short Bio (EN):

Alexandre Madeira é um membro do HASLab - INESC TEC que está  a desenvolver o projecto de pós-doutoramento  "dynamic logics for every season" suportado por uma bolsa individual BPD FCT (SFRH /BPD/103004/2014). O projecto é acolhido no HASLab - INESC TEC e no centro CIDMA sob orientação científica de Luís S. Barbosa (Dep. Informática, Univ. Minho) e Manuel A. Martins (Dep. Matemática da Univ. Aveiro).   O Alexandre é ainda o Investigador Responsável do projecto R&D da FCT "DaLí: Dynamic logics for cyber-physical systems: towards contract based design".   Interesses de Investigação:   - Fundamentos Matemáticos para a Engenharia de Software   - Métodos Lógicos e Algébricos para o Sesenvolvimento de Software   - Geração Paramétrica de Lógicas Modais/Hibridas/Dinamicas   - Algebra de Processos    

Tópicos
de interesse
Detalhes

Detalhes

  • Nome

    Alexandre Castro Madeira
  • Cargo

    Investigador Colaborador Externo
  • Desde

    01 novembro 2011
002
Publicações

2023

Paraconsistent Transition Systems

Autores
Cruz, A; Madeira, A; Barbosa, LS;

Publicação
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE

Abstract
Often in Software Engineering a modelling formalism has to support scenarios of inconsistency in which several requirements either reinforce or contradict each other. Paraconsistent transition systems are proposed in this paper as one such formalism: states evolve through two accessibility relations capturing weighted evidence of a transition or its absence, respectively. Their weights come from a specific residuated lattice. A category of these systems, and the corresponding algebra, is defined providing a formal setting to model different application scenarios. One of them, dealing with the effect of quantum decoherence in quantum programs, is used for illustration purposes.

2023

Stepwise Development of Paraconsistent Processes

Autores
Cunha, J; Madeira, A; Barbosa, LS;

Publicação
Theoretical Aspects of Software Engineering - 17th International Symposium, TASE 2023, Bristol, UK, July 4-6, 2023, Proceedings

Abstract

2023

Specifying Event/Data-based Systems

Autores
Knapp, A; Hennicker, R; Madeira, A;

Publicação
RELATIONAL AND ALGEBRAIC METHODS IN COMPUTER SCIENCE, RAMICS 2023

Abstract
Event/data-based systems are controlled by events, their local data state may change in reaction to events. Numerous methods and notations for specifying such reactive systems have been designed, though with varying focus on the different development steps and their refinement relations. We first briefly review some of such methods, like temporal/modal logic, TLA, UML state machines, symbolic transition systems, CSP, synchronous languages, and Event-B with their support for parallel composition and refinement. We then present E. -logic for covering a broad range of abstraction levels of event/data-based systems from abstract requirements to constructive specifications in a uniform foundation. E. -logic uses diamond and box modalities over structured events adopted from dynamic logic, for recursive process specifications it offers (control) state variables and binders from hybrid logic. The semantic interpretation relies on event/data transition systems; specification refinement is defined by model class inclusion. Constructive operational specifications given by state transition graphs can be characterised by a single E. -sentence. Also a variety of implementation constructors is available in E. -logic to support, among others, event refinement and parallel composition. Thus the whole development process can rely on E. -logic and its semantics as a common basis.

2023

Weighted synchronous automata

Autores
Gomes, L; Madeira, A; Barbosa, LS;

Publicação
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE

Abstract
This paper introduces a class of automata and associated languages, suitable to model a computational paradigm of fuzzy systems, in which both vagueness and simultaneity are taken as first-class citizens. This requires a weighted semantics for transitions and a precise notion of a synchronous product to enforce the simultaneous occurrence of actions. The usual relationships between automata and languages are revisited in this setting, including a specific Kleene theorem.

2023

idDL2DL - Interval Syntax to dL

Autores
Santos, J; Figueiredo, D; Madeira, A;

Publicação
Theoretical Aspects of Software Engineering - 17th International Symposium, TASE 2023, Bristol, UK, July 4-6, 2023, Proceedings

Abstract

Teses
supervisionadas

2018

Contracts on-demand

Autor
Leandro Rafael Moreira Gomes

Instituição
UA

2016

Contracts on-demand

Autor
Leandro Rafael Moreira Gomes

Instituição
FCT

0

Validação do IEC 61131-3 Programmable Logical Controllers em KeyMaera

Autor
Yoan David Ribeiro

Instituição
FCT