Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
Publications

Publications by Luís Soares Barbosa

2016

Asymmetric Combination of Logics is Functorial: A Survey

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

Publication
Recent Trends in Algebraic Development Techniques - 23rd IFIP WG 1.3 International Workshop, WADT 2016, Gregynog, UK, September 21-24, 2016, Revised Selected Papers

Abstract
Asymmetric combination of logics is a formal process that develops the characteristic features of a specific logic on top of another one. Typical examples include the development of temporal, hybrid, and probabilistic dimensions over a given base logic. These examples are surveyed in the paper under a particular perspective—that this sort of combination of logics possesses a functorial nature. Such a view gives rise to several interesting questions. They range from the problem of combining translations (between logics), to that of ensuring property preservation along the process, and the way different asymmetric combinations can be related through appropriate natural transformations.

2016

Quien sabe por Algebra, sabe scientificamente: A tribute to José Nuno Oliveira

Authors
Barbosa, LS; Cunha, A; Silva, A;

Publication
J. Log. Algebr. Meth. Program.

Abstract

2017

Composing Families of Timed Automata

Authors
Cledou, G; Proenca, J; Barbosa, LS;

Publication
FUNDAMENTALS OF SOFTWARE ENGINEERING, FSEN 2017

Abstract
Featured Timed Automata (FTA) is a formalism that enables the verification of an entire Software Product Line (SPL), by capturing its behavior in a single model instead of product-by-product. However, it disregards compositional aspects inherent to SPL development. This paper introduces Interface FTA (IFTA), which extends FTA with variable interfaces that restrict the way automata can be composed, and with support for transitions with atomic multiple actions, simplifying the design. To support modular composition, a set of Reo connectors are modelled as IFTA. This separation of concerns increases reusability of functionality across products, and simplifies modelling, maintainability, and extension of SPLs. We show how IFTA can be easily translated into FTA and into networks of Timed Automata supported by UPPAAL. We illustrate this with a case study from the electronic government domain.

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.

2017

On Kleene Algebras for Weighted Computation

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

Publication
FORMAL METHODS: FOUNDATIONS AND APPLICATIONS, SBMF 2017

Abstract
Kleene algebra with tests (KAT) was introduced as an algebraic structure to model and reason about classic imperative programs, i.e. sequences of discrete actions guarded by Boolean tests. This paper introduces two generalisations of this structure able to express programs as weighted transitions and tests with outcomes in a not necessary bivalent truth space, namely graded Kleene algebra with tests (GKAT) and Heyting Kleene algebra with tests (HKAT). On these contexts, in analogy to Kozen's encoding of Propositional Hoare Logic (PHL) in KAT [10], we discuss the encoding of a graded PHL in HKAT and of its while-free fragment in GKAT.

2014

Quantitative analysis of Reo-based service coordination

Authors
Oliveira, N; Silva, A; Barbosa, LS;

Publication
Symposium on Applied Computing, SAC 2014, Gyeongju, Republic of Korea - March 24 - 28, 2014

Abstract

  • 5
  • 31