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
Publicações

Publicações por Luís Soares Barbosa

2013

Hybridisation at work

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

Publicação
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Abstract
This paper presents the encoding of the hybridisation method proposed in [MMDB11, DM13] into the Hets platform. © 2013 Springer-Verlag Berlin Heidelberg.

2014

Paradigm integration in a specification course

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

Publicação
2014 IEEE 15TH INTERNATIONAL CONFERENCE ON INFORMATION REUSE AND INTEGRATION (IRI)

Abstract
As a complex artefact, software has to meet requirements formulated and verified at different levels of abstraction. A basic distinction is drawn between behavioural (dynamic) and data (static) aspects. From an educational point of view, although disguised under a number of different designations, both issues are usually present, but kept separated, in typical Computer Science undergraduate curricula. It is often argued that they tackle orthogonal problems through essentially different methods. This paper explores an alternative path in which students progress from equational to hybrid specifications in a uniform setting, integrating paradigms, combining data and behaviour, and dealing appropriately with systems evolution and reconfiguration.

2013

An Institution for Alloy and Its Translation to Second-Order Logic

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

Publicação
Integration of Reusable Systems [extended versions of the best papers which were presented at IEEE International Conference on Information Reuse and Integration and IEEE International Workshop on Formal Methods Integration, San Francisco, CA, USA, August 2013]

Abstract
Lightweight formal methods, of which Alloy is a prime example, combine the rigour of mathematics without compromising simplicity of use and suitable tool support. In some cases, however, the verification of safety or mission critical software entails the need formore sophisticated technologies, typically based on theorem provers. This explains a number of attempts to connect Alloy to specific theorem provers documented in the literature. This chapter, however, takes a different perspective: instead of focusing on one more combination of Alloy with still another prover, it lays out the foundations to fully integrate this system in the Hets platform which supports a huge network of logics, logic translators and provers. This makes possible for Alloy specifications to “borrow” the power of several, non dedicated proof systems. The chapter extends the authors’ previous work on this subject by developing in full detail the semantical foundations for this integration, including a formalisation of Alloy as an institution, and introducing a new, more general translation of the latter to second-order logic.

2013

When even the interface evolves ...

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

Publicação
2013 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE)

Abstract
This paper extends the authors' previous work on a formal approach to the specification of reconfigurable systems, introduced in [7], in which configurations are taken as local states in a suitable transition structure. The novelty is the explicit consideration that not only the realisation of a service may change from a configuration to another, but also the set of services provided and even their functionality, may themselves vary. In other words, interfaces may evolve, as well.

2013

Boilerplates for Reconfigurable Systems: A Language and Its Semantics

Autores
Madeira, A; Martins, MA; Barbosa, LS;

Publicação
PROGRAMMING LANGUAGES, SBLP 2013

Abstract
Boilerplates are simplified, normative English texts, intended to capture software requirements in a controlled way. This paper proposes a pallet of boilerplates as a requirements modelling language for reconfigurable systems, i.e., systems structured in different modes of execution among which they can dynamically commute. The language semantics is given as an hybrid logic, in an institutional setting. The mild use made of the theory of institutions, which, to a large extent, may be hidden from the working software engineer, not only provides a rigorous and generic semantics, but also paves the way to tool-supported validation.

2015

A logic for n-dimensional hierarchical refinement

Autores
Madeira, A; Martins, MA; Barbosa, LS;

Publicação
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE

Abstract
Hierarchical transition systems provide a popular mathematical structure to represent state-based software applications in which different layers of abstraction are represented by inter-related state machines. The decomposition of high level states into inner sub-states, and of their transitions into inner sub-transitions is common refinement procedure adopted in a number of specification formalisms. This paper introduces a hybrid modal logic for k-layered transition systems, its first-order standard translation, a notion of bisimulation, and a modal invariance result. Layered and hierarchical notions of refinement are also discussed in this setting.

  • 3
  • 31