Recent Publications

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.

Shoker A.  2017.  Sustainable Blockchain through Proof of eXercise. The 16th IEEE International Symposium on Network Computing and Applications (NCA 2017). PoX
Kassam Z, Shoker A, Almeida PS, Moreno CB.  2017.  Aggregation Protocols in Light of Reliable Communication. The 16th IEEE International Symposium on Network Computing and Applications (NCA 2017). Aggregation Protocols in Light of Reliable Communication
Machado M, Couto R, Campos JC.  2017.  MODUS: model-based user interfaces prototyping. Proceedings of the ACM SIGCHI Symposium on Engineering Interactive Computing Systems, EICS 2017, Lisbon, Portugal, June 26-29, 2017. :111–116. Abstractmain.pdf

n/a

Carvalho M, Belo O, Macedo N.  2017.  Checking the Correctness of What-If Scenarios. 11th IFIP WG 8.9 Working Conference (CONFENIS 2017).
Silva JMC, Bispo KA, Carvalho P, Lima SR.  2017.  LiteSense: An adaptive sensing scheme for WSNs. 2017 IEEE Symposium on Computers and Communications (ISCC). :1209-1212. Abstract
n/a
Almeida JB, Barbosa M, Barthe G, Blot A, Grégoire B, Laporte V, Oliveira T, Pacheco H, Schmidt B, - P.  2017.  Jasmin: High-Assurance and High-Speed Cryptography. Proceedings of the 2017 {ACM} {SIGSAC} Conference on Computer and Communications Security, {CCS} 2017, Dallas, TX, USA, October 30 - November 03, 2017. :1807–1823. Abstract
n/a
Macedo R, Paulo J, Pontes R, Portela B, Oliveira T, Matos M, Oliveira R.  2017.  A Practical Framework for Privacy-Preserving NoSQL Databases. 36th {IEEE} Symposium on Reliable Distributed Systems, {SRDS} 2017, Hong Kong, Hong Kong, September 26-29, 2017. :11–20. Abstract
n/a
Couto R, Campos JC, Ribeiro AN.  2017.  Usability evaluation of the uCat tool. EPCGI. usability_ucat.pdf
He M, Vafeiadis V, Qin S, Ferreira JF.  2016.  Reasoning about Fences and Relaxed Atomics. Search Results 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing. Abstract2016-pdp-gpsfences.pdf

For efficiency reasons, weak (or relaxed) memory is now the norm on modern architectures. To cater for this trend, modern programming languages are adapting their memory models. The new C11 memory model allows several levels of memory weakening, including non-atomics, relaxed atomics, release-acquire atomics, and sequentially consistent atomics. Under such weak memory models, multithreaded programs exhibit more behaviours, some of which would have been inconsistent under the traditional strong (i.e. sequentially consistent) memory model. This makes the task of reasoning about concurrent programs even more challenging. The GPS framework, recently developed by Turon et al., has made a step forward towards tackling this challenge. By integrating ghost states, per-location protocols and separation logic, GPS can successfully verify programs with release-acquire atomics. In this paper, we present a program logic, an enhancement of the GPS framework, that can support the verification of a bigger class of C11 programs, that is, programs with release-acquire atomics, relaxed atomics and release-acquire fences. Key elements of our proposed logic include two new types of assertions, a more expressive resource model and a set of newly-designed verification rules.

Even C, Bosser A-G, Ferreira JF, Buche C, Stéphan F, Cavazza M, Lisetti C.  2016.  Supporting Social Skills Rehabilitation with Virtual Storytelling. 29th International FLAIRS Conference. Abstract12953-57659-1-pb.pdf

Social skills training (SST) has recently emerged as a typical application for emotional conversational agents (ECA). While a number of prototypes have targeted the general population, fewer have been used for psychiatric patients despite the widely recognised potential of ECAs technologies in the field of mental health. Social cognition impairment is however a widely shared symptom in psychiatric patients suffering from pathologies such as schizophrenia. Going further than SST, rehabilitation programmes involving role-play, but also problem solving have been successfully used by clinicians, drastically improving the quality of life of patients suffering from such disabilities. One of the challenges of these programmes is to ensure that the patients will be able to adapt their behaviour when the situation varies, rather than training them with the appropriate behaviour for a set of specific situations.
In this paper, we describe a novel approach for the development of a serious game supporting rehabilitation programmes for social skills, which will primarily target schizophrenia patients. We propose to use an ECA in combination with a narrative generation engine issued from interactive storytelling research to provide varied situations. This approach reflects the combination of both role-play and problem solving exercises on which remediation therapies rely, and has the potential to support patient's progress and motivation through the rehabilitation programme.

Couto R, Ribeiro AN, Campos JC.  2016.  Validating an approach to formalize use cases with ontologies. Proceedings of the 13th International Workshop on Formal Engineering Approaches to Software Components and Architectures. 205:1-15. Abstract1603.08632v1.pdf

Use case driven development methodologies put use cases at the center of the software development process. However, in order to support automated development and analysis, use cases need to be appropriately formalized. This will also help guarantee consistency between requirements specifications and the developed solutions. Formal methods tend to suffer from take up issues, as they are usually hard to accept by industry. In this context, it is relevant not only to produce languages and approaches to support formalization, but also to perform their validation. In previous works we have developed an approach to formalize use cases resorting to ontologies. In this paper we present the validation of one such approach. Through a three stage study, we evaluate the acceptance of the language and supporting tool. The first stage focusses on the acceptance of the process and language, the second on the support the tool provides to the process, and finally the third one on the tool's usability aspects. Results show test subjects found the approach feasible and useful and the tool easy to use.