Cledou G, Proença J, Barbosa L.  2017.  Composing Families of Timed Automata. 7th IPM International Conference on Fundamentals of Software Engineering. Abstractifta.pdf


Proença J, Moreno CB.  2017.  Quality-Aware Reactive Programming for the Internet of Things. 7th IPM International Conference on Fundamentals of Software Engineering. quarp.pdf
Halder R, Proença J, Macedo N, Santos A.  2017.  Formal Verification of ROS-based Robotic Applications using Timed-Automata. FME Workshop on Formal Methods In Software Engineering. ros-formalise17.pdf
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.

Daniels W, Proença J, Clarke D, Joosen W, Hughes D.  2015.  Refraction: Low-Cost Management of Reflective Meta-Data in Pervasive Component-Based Applications. Proceedings of the 18th International Symposium on Component-Based Software Engineering - CBSE. :27–36. Abstractrefraction.pdf

This paper proposes the concept of refraction, a principled means to lower the cost of managing reflective meta-data for pervasive systems. While prior work has demonstrated the benefits of reflective component-based middleware for building open and reconfigurable applications, the cost of using remote reflective operations remains high. Refractive components address this problem by selectively augmenting application data flows with their reflective meta-data, which travels at low cost to refractive pools, which serve as loci of inspection and control for the distributed application. Additionally reactive policies are introduced, providing a mechanism to trigger reconfigurations based on incoming reflective meta-data. We evaluate the performance of refraction in a case-study of automatic configuration repair for a real-world pervasive application. We show that refraction reduces network overhead in comparison to the direct use of reflective operations while not increasing development overhead. To enable further experimentation with the concept of refraction, we provide RxCom, an open-source refractive component model and supporting runtime environment.

Ramachandran GS, Daniels W, Proença J, Michiels S, Joosen W, Hughes D, Porter B.  2015.  Hitch Hiker: A Remote Binding Model with Priority Based Data Aggregation for Wireless Sensor Networks. Proceedings of the 18th International Symposium on Component-Based Software Engineering, CBSE. :43–48. Abstracthitchhiker.pdf

The aggregation of network traffic has been shown to enhance the performance of wireless sensor networks. By reducing the number of packets that are transmitted, energy consumption, collisions and congestion are minimised. However, current data aggregation schemes restrict developers to a specific network structure or cannot handle multi-hop data aggregation. In this paper, we propose Hitch Hiker, a remote component binding model that provides support for multi-hop data aggregation. Hitch Hiker uses component meta-data to discover remote component bindings and to construct a multi-hop overlay network within the free payload space of existing traffic flows. This overlay network provides end-to-end routing of low-priority traffic while using only a small fraction of the energy of standard communication. We have developed a prototype implementation of Hitch Hiker for the LooCI component model. Our evaluation shows that Hitch Hiker consumes minimal resources and that using Hitch Hiker to deliver low-priority traffic reduces energy consumption by up to 15%.

Daniels W, Proença J, Matthys N, Joosen W, Hughes D.  2015.  Tomography: lowering management overhead for distributed component-based applications. Proceedings of the 2nd Workshop on Middleware for Context-Aware Applications in the IoT, M4IoT@Middleware 2015, Vancouver, BC, Canada, December 7-11, 2015. :13–18. Abstracttomography.pdf


Proença J, Clarke D.  2015.  Typed Connector Families. Formal Aspects of Component Software - 12th International Conference, FACS 2015, Niterói, Brazil, October 14-16, 2015, Revised Selected Papers. 9539:294–311. Abstractcfam.pdf


Proença J, Clarke D.  2013.  Interactive Interaction Constraints. Proceedings of 15th International Conference on Coordination Models and Languages Florence. :211–225. Abstractinteractivechannels.pdf

Interaction constraints are an expressive formalism for describing coordination patterns, such as those underlying the coordination language Reo, that can be efficiently implemented using constraint satisfaction technologies such as SAT and SMT solvers. Existing implementations of interaction constraints interact with external components only in a very simple way: interaction occurs only between rounds of constraint satisfaction. What is missing is any means for the constraint solver to interact with the external world during constraint satisfaction. This paper introduces interactive interaction constraints which enable interaction during constraint satisfaction, and in turn increase the expressiveness of coordination languages based on interaction constraints by allowing a larger class of operations to be considered to occur atomically. We describe how interactive interaction constraints are implemented and detail a number of strategies for guiding constraint solvers. The benefit of interactive interaction constraints is illustrated using two examples, a hotel booking system and a system of transactions with compensations. From a general perspective, our work describes how to open up and exploit constraint solvers as the basis of a coordination engine.

Proença J, Clarke D.  2013.  Data Abstraction in Coordination Constraints. Advances in Service-Oriented and Cloud Computing - Workshops - ESOCC . :159–173. Abstractdata-abstraction.pdf

This paper studies complex coordination mechanisms based on constraint satisfaction. In particular, it focuses on data-sensitive connectors from the Reo coordination language. These connectors restrict how and where data can flow between loosely-coupled components taking into account the data being exchanged. Existing engines for Reo provide a very limited support for data-sensitive connectors, even though data constraints are captured by the original semantic models for Reo. When executing data-sensitive connectors, coordination constraints are not exhaustively solved at compile time but at runtime on a per-need basis, powered by an existing SMT (satisfiability modulo theories) solver.To deal with a wider range of data types and operations, we abstract data and reduce the original constraint satisfaction problem to a SAT problem, based on a variation of predicate abstraction. We show soundness and completeness of the abstraction mechanism for well-defined constraints, and validate our approach by evaluating the performance of a prototype implementation with different test cases, with and without abstraction.

Muschevici R, Clarke D, Proença J.  2013.  Executable modelling of dynamic software product lines in the ABS language. 5th International Workshop on Feature-Oriented Software Development - FOSD. :17–24. Abstractfosd2013.pdf

Dynamic software product lines (DSPLs) combine the advantages of traditional SPLs, such as an explicit variability model connected to an integrated repository of reusable code artefacts, with the ability to exploit a system's variability at runtime. When a system needs to adapt, for example to changes in operational environment or functional requirements, DSPL systems are capable of adapting their behaviour dynamically, thus avoiding the need to halt, recompile and redeploy. The eld of DSPL engineering is still in formation and general-purpose DSPL development languages and tools are rare. In this paper we introduce a language and execution environment for developing and running dynamic SPLs. Our work builds on ABS, a language and integrated development environment with dedicated support for implementing static software product lines. Our ABS extension advances the scope of ABS to dynamic SPL engineering. Systems developed using ABS are compiled to Java, and are thus executable on a wide range of platforms.

Proença J, Clarke D, de Vink EP, Arbab F.  2012.  Dreams: a framework for distributed synchronous coordination. Proceedings of the ACM Symposium on Applied Computing - SAC. :1510–1515. Abstractsac2012.pdf

Synchronous coordination systems, such as Reo, exchange data via indivisible actions, while distributed systems are typically asynchronous and assume that messages can be delayed or get lost. To combine these seemingly contradictory notions, we introduce the Dreams framework. Coordination patterns in Dreams are described using a synchronous model based on the Reo language, whereas global system behaviour is given by the runtime composition of autonomous actors communicating asynchronously. Dreams also exploits the use of actors in the composition of coordination patterns to allow asynchronous communication whenever possible, increasing the scalability of the implementation.

Clarke D, Proença J.  2012.  Partial Connector Colouring. Proceedings of 14th International Conference on Coordination Models and Languages . :59–73. Abstractmain.pdf

Connector colouring provided an intuitive semantics of Reo connectors which lead to e ective implementation techniques, rst based on computing colouring tables directly, and later on encodings of colouring into constraints. One weakness of the framework is that it operates globally, giving a colouring to all primitives of the connector in lock-step, including those not involved in the interaction. This global approach limits both scalability and the available concurrency. This paper addresses these problems by introducing partiality into the connector colouring model. Partial colourings allow parts of a connector to operate independently and in isolation, increasing scalability and concurrency.

Jongmans S-STQ, Clarke D, Proença J.  2012.  A Procedure for Splitting Processes and its Application to Coordination. Proceedings 11th International Workshop on Foundations of Coordination Languages and Self Adaptation - FOCLASA . :79–96. Abstract1209.1422.pdf

We present a procedure for splitting processes in a process algebra with multi-actions (a subset of the
specification language mCRL2). This splitting procedure cuts a process into two processes along a
set of actions A: roughly, one of these processes contains no actions from A, while the other process
contains only actions from A. We state and prove a theorem asserting that the parallel composition
of these two processes equals the original process under appropriate synchronization.
We apply our splitting procedure to the process algebraic semantics of the coordination language
Reo: using this procedure and its related theorem, we formally establish the soundness of splitting
Reo connectors along the boundaries of their (a)synchronous regions in implementations of Reo.
Such splitting can significantly improve the performance of connectors.

Patrignani M, Matthys N, Proença J, Hughes D, Clarke D.  2012.  Formal analysis of policies in wireless sensor network applications. Proceedings of Third International Workshop on Software Engineering for Sensor Network Applications - SESENA . :15–21. Abstractnls-plc-6pp.pdf

Since wireless sensor network applications are ever growing in scale and complexity, managers require strong formal guarantees that any changes done to the system can be enacted safely. This paper presents the formalisation and analysis of the semantics of policies, tiny software artefacts used to orchestrate wireless sensor network applications. The semantics of policies is formalised in terms of traces augmented with information concerning the constraints under which traces are executed. These traces are composed according to the network topology and subsequently analysed using them CRL2 model-checking tool. The analysis allows for the detection of semantical inconsistencies that may lead to dangerous or unwanted behaviour of the application based on the policy configuration. An analysis of policies in a real-world system is provided, showing how to verify security and resource usage properties.