Barbosa LS, Martins MA, Madeira A, Neves R.  2016.  Reuse and Integration of Specification Logics: The Hybridisation Perspective. Theoretical Information Reuse and Integration. 446:1–30. Abstractbmmn16.pdf

Hybridisation is a systematic process along which the characteristic features of hybrid logic, both at the syntactic and the semantic levels, are developed on top of an arbitrary logic framed as an institution. It also captures the construction of first-order encodings of such hybridised institutions into theories in first-order logic. The method was originally developed to build suitable logics for the specification of reconfigurable software systems on top of whatever logic is used to describe local requirements of each system’s configuration. Hybridisation has, however, a broader scope, providing a fresh example of yet another development in combining and reusing logics driven by a problem from Computer Science. This paper offers an overview of this method, proposes some new extensions, namely the introduction of full quantification leading to the specification of dynamic modalities, and exemplifies its potential through a didactical application. It is discussed how hybridisation can be successfully used in a formal specification course 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.

Sanchez A, Barbosa LS, Madeira A.  2015.  Modelling and Verifying Smell-Free Architectures with the Archery Language. Software Engineering and Formal Methods. :147-163. Abstractsmellfreearch2014.pdf

Architectural (bad) smells are design decisions found in software architectures that degrade the ability of systems to evolve. This paper presents an approach to verify that a software architecture is smell-free using the Archery architectural description language. The language provides a core for modelling software architectures and an extension for specifying constraints. The approach consists in precisely specifying architectural smells as constraints, and then verifying that software architectures do not satisfy any of them. The constraint language is based on a propositional modal logic with recursion that includes: a converse operator for relations among architectural concepts, graded modalities for describing the cardinality in such relations, and nominals referencing architectural elements. Four architectural smells illustrate the approach.

Ferreira JF, Mendes A, Cunha A, Moreno CB, Silva P, Barbosa LS, Oliveira JN.  2011.  Logic Training through Algorithmic Problem Solving. Tools for Teaching Logic. 6680:62-69. Abstractticttl11.pdf

Although much of mathematics is algorithmic in nature, the skills needed to formulate and solve algorithmic problems do not form an integral part of mathematics education. In particular, logic, which is central to algorithm development, is rarely taught explicitly at pre university level, under the justi cation that it is implicit in mathematics and therefore does not need to be taught as an independent topic. This paper argues in the opposite direction, describing a one week workshop done at the University of Minho, in Portugal, whose goal was to introduce to high-school students calculational principles and techniques of algorithmic problem solving supported by calculational logic. The work shop resorted to recreational problems to convey the principles and to software tools, the Alloy Analyzer and Netlogo, to animate models.

Madeira A, Martins M, Barbosa LS.  2011.  Models as arrows: the role of dialgebras. Models of Computation in Context. :144–153. Abstract

A large number of computational processes can suitably be described as a combination of construction, i.e. algebraic, and observation, i.e. coalgebraic, structures. This paper suggests dialgebras as a generic model in which such structures can be combined and proposes a small calculus of dialgebras including a wrapping combinator and se- quential composition. To take good care of invariants in software design, the paper also discusses how dialgebras can be typed by predicates and proves that invariants are preserved through composition. This lays the foundations for a full calculus of invariant proof-obligation discharge for dialgebraic models.

Meng S, Barbosa LS.  2009.  A Coalgebraic Semantic Framework for Reasoning about Interaction Designs. UML Semantics and Applications. :249–279. Abstract

If, as a well-known aphorism states, modelling is for reasoning, this chapter is an attempt to define and apply a formal semantics to interaction patterns captured by UML 2.0 sequence diagrams in order to enable rigourous reasoning about them. Actually, model transformation plays a fundamental role in the process of software development, in general, and in model driven engineering in particular. Being a de facto standard in this area, UML is no exception, even if the number and diversity of diagrams expressing UML models makes it difficult to base its semantics on a single framework. This chapter argues for the use of coalgebra theory, as the mathematics of state-based designs, to give a precise semantics to sequence diagrams with coercions. In particular, it illustrates how an algebra for constructing and reasoning about them can be made explicit and useful for the working software architect.

Ferreira JF, Mendes A, Backhouse R, Barbosa LS.  2009.  Which Mathematics for the Information Society? Teaching Formal Methods. Abstract

MathIS is a new project that aims to reinvigorate secondary-school mathematics by exploiting insights of the dynamics of algorithmic problem solving. This paper describes the main ideas that underpin the project. In summary, we propose a central role for formal logic, the development of a calculational style of reasoning, the emphasis on the algorithmic nature of mathematics, and the promotion of self-discovery by the students. These ideas are discussed and the case is made, through a number of examples that show the teaching style that we want to introduce, for their relevance in shaping mathematics training for the years to come. In our opinion, the education of software engineers that work effectively with formal methods and mathematical abstractions should start before university and would benefit from the ideas discussed here.

Barbosa LS, Martinho M.  2007.  Modelling is for reasoning. Mathematical Modelling (ICTMA 12): Education, Engineering and Economics. :480-490. Abstract

In a broad sense, computing is an area of knowledge from which a popular and effective technology emerged long before a solid, specific, scientific methodology, let alone formal foundations, had been put forward. This might explain some of the weaknesses in the software industry, on the one hand, as well as an excessively technology-oriented view which dominates computer science training at pre-university and even undergraduate teaching, on the other. Modelling, understood as the ability to choose the right abstractions for a problem domain, is consensually recognised as essential for the development of true engineering skills in this area, as it is in all other engineering disciplines. But, how can the basic problem-solving strategy, one gets used to from school physics: understand the problem, build a mathematical model, reason within the model, calculate a solution, be taken (and taught) as the standard way of dealing with software design problems? This paper addresses this question, illustrating and discussing the interplay between modelling and reasoning.

Barbosa LS, Sun M, Aichernig B, Rodrigues N.  2006.  On the Semantics of Componentware: a Coalgebraic Perspective. Mathematical Frameworks for Component Software: Models for Analysis and Synthesis. :69–117. Abstract

In this chapter we present a coalgebraic semantics for components. Our semantics forms the basis for a family of operators for combining components. These operators together with their algebraic laws establish a calculus for software components. We present two applications of our semantics: a coalgebraic interpretation of UML diagrams and the design of a component repository.

Barbosa LS.  2005.  A Perspective on Component Refinement. Formal Methods for Components and Objects, Third International Symposium, FMCO 2004, Leiden, The Netherlands, November 2 - 5, 2004, Revised Lectures. 3657:23–48. Abstract

This paper provides an overview of an approach to coalgebraic modelling and refinement of state-based software components, summing up some basic results and introducing a discussion on the interplay between behavioural and classical data refinement. The approach builds on coalgebra theory as a suitable tool to capture observational semantics and to base an abstract characterisation of possible behaviour models for components (from partiality to different degrees of non-determinism).

Cledou G, Proença J, Barbosa LS.  2017.  A Refinement Relation for Families of Timed Automata. XX Brazilian Symposium on Formal Methods. Abstractiftarefinement.pdf

Software Product Lines (SPLs) are families of systems that share a high number of common assets while differing in others. In component-based systems, components themselves can be SPLs, i.e., each component can be seen as a family of variations, with different interfaces and functionalities, typically parameterized by a set of features and a feature model that specifies the valid combinations of features. This paper explores how to safely replace such families of components with more refined ones. We propose a notion of refinement for Interface Featured Timed Automata (IFTA), a formalism to model families of timed automata with support for multi-action transitions. We separate the notion of IFTA refinement into behavioral and variability refinement, i.e., the refinement of the underlying timed automata and feature model. Furthermore, we define behavioral refinement for the semantic level, i.e., transition systems, as an alternating simulation between systems, and lift this definition to IFTA refinement. We illustrate this notion with examples throughout the text and show that refinement is a pre-order and compositional.

Cledou MG, Barbosa LS.  2016.  An Ontology for Licensing Public Transport Services. Proceedings of the 9th International Conference on Theory and Practice of Electronic Governance. :230–239. Abstractan_ontology_for_licensing_public_transport_services.pdf

By 2050 it is expected that 66% of the world population will reside in cities, compared to 54% in 2014. One particular challenge associated to urban population growth refers to transportation systems, and as an approach to face it, governments are investing significant efforts enhancing public transport services. An important aspect of public transport is ensuring that licensing of such services fulfill existing government regulations. Due to the differences in government regulations, and to the difficulties in ensuring the fulfillment of their specific features, many local governments develop tailored Information and Communication Technology (ICT) solutions to automate the licensing of public transport services. In this paper we propose an ontology for licensing such services following the REFSENO methodology. In particular, the ontology captures common concepts involved in the application and processing stage of licensing public bus passenger services. The main contribution of the proposed ontology is to define a common vocabulary to share knowledge between domain experts and software engineers, and to support the definition of a software product line for families of public transport licensing services.

Madeira A, Martins MA, Barbosa LS.  2016.  A logic for n-dimensional hierarchical refinement. Proceedings 17th International Workshop on Refinement, Refine@FM 2015, Oslo, Norway, 22nd June 2015. 209:40–56.2.pdf
Madeira A, Barbosa LS, Hennicker R, Martins MA.  2016.  Dynamic Logic with Binders and Its Application to the Development of Reactive Systems. Theoretical Aspects of Computing - ICTAC 2016 - 13th International Colloquium, Taipei, Taiwan, ROC, October 24-31, 2016, Proceedings. 9965:422–440. Abstractmbhm16.pdf

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↓-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.

Neves R, Barbosa LS.  2016.  Hybrid Automata as Coalgebras. Theoretical Aspects of Computing - ICTAC 2016 - 13th International Colloquium, Taipei, Taiwan, ROC, October 24-31, 2016, Proceedings. 9965:385–402. Abstractnb16.pdf

Able to simultaneously encode discrete transitions and continuous behaviour, hybrid automata are the de facto framework for the formal specification and analysis of hybrid systems. The current paper revisits hybrid automata from a coalgebraic point of view. This allows to interpret them as state-based components, and provides a uniform theory to address variability in their definition, as well as the corresponding notions of behaviour, bisimulation, and observational semantics.

Fernandes S, Barbosa LS.  2016.  Applying the 3C Model to FLOSS Communities. Collaboration and Technology - 22nd International Conference, CRIWG 2016, Kanazawa, Japan, September 14-16, 2016, Proceedings. 9848:139–150. Abstractfb16a.pdf

How learning occurs within Free/Libre Open Source (FLOSS) communities and what is the dynamics such projects (e.g. the life cycle of such projects) are very relevant questions when considering the use of FLOSS projects in a formal education setting. This paper introduces an approach based on the 3C collaboration model (communication, coordination and cooperation) to represent the collaborative learning dynamics within FLOSS communities. To explore the collaborative learning potential of FLOSS communities a number of questionnaires and interviews to selected FLOSS contributors were run. From this study a 3C collaborative model applicable to FLOSS communities was designed and discussed.