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 Renato Jorge Neves

2013

Giving Alloy a family

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

Publicação
Proceedings of the 2013 IEEE 14th International Conference on Information Reuse and Integration, IEEE IRI 2013

Abstract
Lightweight formal methods ought to provide to the end user the rigorousness of mathematics, without compromising simplicity and intuitiveness. Alloy is a powerful tool, particularly successful on this mission. Limitations on the verification side, however, are known to prevent its wider use in the development of safety or mission critical applications. A number of researchers proposed ways to connect Alloy to other tools in order to meet such challenges. This paper's proposal, however, is not establishing a link from Alloy to another single tool, but rather to 'plunge' it into the Hets network of logics, logic translators and provers. This makes possible for Alloy specifications to 'borrow' the power of several, non dedicated proof systems. Semantical foundations for this integration are discussed in detail. © 2013 IEEE.

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
Proceedings of the 2014 IEEE 15th International Conference on Information Reuse and Integration, IEEE IRI 2014

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. © 2014 IEEE.

2013

An institution for Alloy and its translation to second-order logic

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

Publicação
Advances in Intelligent Systems and Computing

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.

2016

Continuity as a computational effect

Autores
Neves, R; Barbosa, LS; Hofmann, D; Martins, MA;

Publicação
CoRR

Abstract

  • 2
  • 4