Cookies Policy
We use cookies to improve our site and your experience. By continuing to browse our site you accept our cookie policy. Find out More
Close
  • Menu
About

About

Alexandre is a member  HASLab INESC TEC currently developing the postdoc project "dynamic logics for every season" supported by the FCT (Portuguese Foundation for Science and technology) with the individual grant SFRH /BPD/103004/2014. The project is hosted in HASLab INESC TEC and CIDMA over the scientific supervision of Luís S. Barbosa (Informatics Dep. of Univ. Minho) and Manuel A. Martins(Mathematics Dep. of Univ. Aveiro).

Alexandre is also coordinating the FCT R&D project DaLí: Dynamic logics for cyber-physical systems: towards contract based design.

Research interest:

- Mathematical Foundations of Software Engineering

- Algebraic and logical methods for software development

- Parametric generation of Modal/Hybrid/Dynamic Logics

- Process Algebra 

Interest
Topics
Details

Details

  • Name

    Alexandre Castro Madeira
  • Cluster

    Computer Science
  • Role

    Researcher
  • Since

    01st November 2011
Publications

2016

A method for rigorous design of reconfigurable systems

Authors
Madeira, A; Neves, R; Barbosa, LS; Martins, MA;

Publication
SCIENCE OF COMPUTER PROGRAMMING

Abstract
Reconfigurability, understood as the ability of a system to behave differently in different modes of operation and commute between them along its lifetime, is a cross-cutting concern in modern Software Engineering. This paper introduces a specification method for reconfigurable software based on a global transition structure to capture the system's reconfiguration space, and a local specification of each operation mode in whatever logic (equational, first-order, partial, fuzzy, probabilistic, etc.) is found expressive enough for handling its requirements. In the method these two levels are not only made explicit and juxtaposed, but formally interrelated. The key to achieve such a goal is a systematic process of hybridisation of logics through which the relationship between the local and global levels of a specification becomes internalised in the logic itself.

2016

An exercise on the generation of many-valued dynamic logics

Authors
Madeira, A; Neves, R; Martins, MA;

Publication
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING

Abstract
In the last decades, dynamic logics have been used in different domains as a suitable formalism to reason about and specify a wide range of systems. On the other hand, logics with many-valued semantics are emerging as an interesting tool to handle devices and scenarios where uncertainty is a prime concern. This paper contributes towards the combination of these two aspects through the development of a method for the systematic construction of many-valued dynamic logics. Technically, the method is parameterised by an action lattice that defines both the computational paradigm and the truth space (corresponding to the underlying Kleene algebra and residuated lattices, respectively).

2016

Dynamic Logic with Binders and Its Application to the Development of Reactive Systems

Authors
Madeira, A; Barbosa, LS; Hennicker, R; Martins, MA;

Publication
THEORETICAL ASPECTS OF COMPUTING - ICTAC 2016

Abstract
This paper introduces a logic to support the specification and development of reactive systems on various levels of abstraction, from property specifications, concerning e.g. safety and liveness requirements, to constructive specifications representing concrete processes. This is achieved by combining binders of hybrid logic with regular modalities of dynamic logics in the same formalism, which we call D-down arrow-logic. The semantics of our logic focuses on effective processes and is therefore given in terms of reachable transition systems with initial states. The second part of the paper resorts to this logic to frame stepwise development of reactive systems within the software development methodology proposed by Sannella and Tarlecki. In particular, we instantiate the generic concepts of constructor and abstractor implementations by using standard operators on reactive components, like relabelling and parallel composition, as constructors, and bisimulation for abstraction. We also study vertical composition of implementations which relies on the preservation of bisimularity by the constructions on labeleld transition systems.

2016

Encoding hybridized institutions into first-order logic

Authors
Diaconescu, R; Madeira, A;

Publication
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE

Abstract
A 'hybridization' of a logic, referred to as the base logic, consists of developing the characteristic features of hybrid logic on top of the respective base logic, both at the level of syntax (i.e. modalities, nominals, etc.) and of the semantics (i.e. possible worlds). By 'hybridized institutions' we mean the result of this process when logics are treated abstractly as institutions (in the sense of the institution theory of Goguen and Burstall). This work develops encodings of hybridized institutions into (many-sorted) first-order logic (abbreviated FOL) as a 'hybridization' process of abstract encodings of institutions into FOL, which may be seen as an abstraction of the well-known standard translation of modal logic into FOL. The concept of encoding employed by our work is that of comorphism from institution theory, which is a rather comprehensive concept of encoding as it features encodings both of the syntax and of the semantics of logics/institutions. Moreover, we consider the so-called theoroidal version of comorphisms that encode signatures to theories, a feature that accommodates a wide range of concrete applications. Our theory is also general enough to accommodate various constraints on the possible worlds semantics as well a wide variety of quantifications. We also provide pragmatic sufficient conditions for the conservativity of the encodings to be preserved through the hybridization process, which provides the possibility to shift a formal verification process from the hybridized institution to FOL.

2015

Refinement in hybridised institutions

Authors
Madeira, A; Martins, MA; Barbosa, LS; Hennicker, R;

Publication
FORMAL ASPECTS OF COMPUTING

Abstract
Hybrid logics, which add to the modal description of transition structures the ability to refer to specific states, offer a generic framework to approach the specification and design of reconfigurable systems, i.e., systems with reconfiguration mechanisms governing the dynamic evolution of their execution configurations in response to both external stimuli or internal performance measures. A formal representation of such systems is through transition structures whose states correspond to the different configurations they may adopt. Therefore, each node is endowed with, for example, an algebra, or a first-order structure, to precisely characterise the semantics of the services provided in the corresponding configuration. This paper characterises equivalence and refinement for these sorts of models in a way which is independent of (or parametric on) whatever logic (propositional, equational, fuzzy, etc) is found appropriate to describe the local configurations. A Hennessy-Milner like theorem is proved for hybridised logics.

Supervised
thesis

2016

Contracts on-demand

Author
Leandro Rafael Moreira Gomes

Institution
UM

2015

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

Author
Yoan David Ribeiro

Institution
UM