Journal Articles

Almeida PS, Shoker A, Moreno CB.  2018.  Delta state replicated data types. Journal of Parallel and Distributed Computing. 111:162-173. AbstractDeltaCRDTJournalWebsite

n/a

Cledou G, Estevez E, Barbosa LS.  2018.  A taxonomy for planning and designing smart mobility services. Government Information Quarterly. :-. Abstractgiq2017.pdfWebsite

Abstract The development of smart mobility initiatives requires specialized and contextualized policies addressing the needs and interests of many stakeholders involved. Since the development of such policies is challenging, there is a need to learn from the experience of many cities around the world offering efficient and successfully adopted smart mobility services. However, in practice, the information provided about such initiatives is shallow and unstructured. To address this issue, we study the state of the art in mobility services, reviewing scientific publications and 42 smart mobility services delivered by nine smart cities around the world, and we propose a taxonomy for planning and designing smart mobility services. The taxonomy provides a common vocabulary to discuss and share information about such services. It comprises eight dimensions: type of services, maturity level, users, applied technologies, delivery channels, benefits, beneficiaries, and common functionality. The contribution of the proposed taxonomy is to serve as a tool for guiding policy makers by identifying a spectrum of mobility services that can be provided, to whom, what technologies can be used to deliver them, and what is the delivered public value so to justify their implementation. In addition, the taxonomy can also assist researchers in further developing the domain. By identifying common functionality, it could also help Information Technology (IT) teams in building and maintaining smart mobility services. Finally, we further discuss usage scenarios of the taxonomy by policy makers, İT\} staff and researchers.

Gonçalves RC, Batory D, Sobral JL, Riché TL.  2017.  From software extensions to product lines of dataflow programs. Software and Systems Modeling. 16(4):929-947. Abstract

Dataflow programs are widely used. Each program is a directed graph where nodes are computations and edges indicate the flow of data. In prior work, we reverse-engineered legacy dataflow programs by deriving their optimized implementations from a simple specification graph using graph transformations called refinements and optimizations. In MDE-speak, our derivations were PIM-toPSM mappings. In this paper, we show how extensions complement refinements, optimizations, and PIM-to-PSM derivations to make the process of reverse engineering complex legacy dataflow programs tractable. We explain how optional functionality in transformations can be encoded, thereby enabling us to encode product lines of transformations as well as product lines of dataflow programs. We describe the implementation of extensions in the ReFlO tool and present two non-trivial case studies as evidence of our work’s generality.

Silva JMC, Carvalho P, Lima SR.  2017.  A Modular Traffic Sampling Architecture: Bringing Versatility and Efficiency to Massive Traffic Analysis. Journal of Network and Systems Management. :1–26. AbstractWebsite
n/a
Bernardeschi C, Domenici A, Masci P.  2017.  A PVS-Simulink Integrated Environment for Model-Based Analysis of Cyber-Physical Systems. IEEE Transactions on Software Engineering. (In Press) Abstract07900400.pdfhttps://doi.org/10.1109/TSE.2017.2694423

This paper presents a methodology, with supporting tool, for formal modeling and analysis of software components in cyber-physical systems. Using our approach, developers can integrate a simulation of logic-based specifications of software components and Simulink models of continuous processes. The integrated simulation is useful to validate the characteristics and functionalities of discrete system components early in the development process. The same logic-based specifications can also be formally verified using the Prototype Verification System (PVS), to gain additional confidence that the software design is compliant with specific safety requirements. Modeling patterns are defined for generating the logic-based specifications from the more familiar automata-based formalism. The ultimate aim of this work is to facilitate the introduction of formal verification technologies in the software development process of cyber-physical systems, which typically requires the integrated use of different formalisms and tools. A case study from the medical domain is used throughout the paper to illustrate the approach. A PVS model of a pacemaker is interfaced with a Simulink model of the human heart. The overall cyber-physical system is co-simulated to validate design requirements through exploration of relevant test scenarios. Formal verification with the PVS theorem prover is demonstrated for the pacemaker model for specific safety aspects of the pacemaker design.

Harrison MD, Masci P, Campos JC, Curzon P.  2017.  Verification of User Interface Software: the Example of Use-Related Safety Requirements and Programmable Medical Devices. IEEE Transactions on Human-Machine Systems. Abstractmedthmsv10.pdfhttps://doi.org/10.1109/THMS.2017.2717910

One part of demonstrating that a device is acceptably safe, often required by regulatory standards, is to show that it satisfies a set of requirements known to mitigate hazards. This paper is concerned with how to demonstrate that a user interface software design is compliant with use-related safety requirements. A methodology is presented based on the use of formal methods technologies to provide guidance to developers about addressing three key verification challenges: 1) how to validate a model, and show that it is a faithful representation of the device; 2) how to formalize requirements given in natural language, and demonstrate the benefits of the formalization process; and 3) how to prove requirements of a model using readily available formal verification tools. A model of a commercial device is used throughout the paper to demonstrate the methodology. A representative set of requirements are considered. They are based on US Food and Drug Administration (FDA) draft documentation for programmable medical devices, and on best practice in user interface design illustrated in relevant international standards. The methodology aims to demonstrate how to achieve the FDA’s agenda of using formal methods to support the approval process for medical devices.

Proença J, Clarke D.  2017.  Typed Connector Families and their semantics. Science of Computer Programming. 115-116:47-78.scp-cfam.pdf
Machado N, Romano P, Rodrigues L.  2017.  CoopREP: Cooperative record and replay of concurrency bugs. Journal of Software Testing, Verification and Reliability.
Oliveira JN.  2017.  Programming from Metaphorisms. Journal of Logical and Algebraic Methods in Programming. AbstractWebsite

Abstract This paper presents a study of the metaphorism pattern of relational specification, showing how it can be refined into recursive programs. Metaphorisms express input-output relationships which preserve relevant information while at the same time some intended optimization takes place. Text processing, sorting, representation changers, etc., are examples of metaphorisms. The kind of metaphorism refinement studied in this paper is a strategy known as change of virtual data structure. By framing metaphorisms in the class of (inductive) regular relations, sufficient conditions are given for such implementations to be calculated using relation algebra. The strategy is illustrated with examples including the derivation of the quicksort and mergesort algorithms, showing what they have in common and what makes them different from the very start of development.

Harrison MD, Masci P, Campos JC, Curzon P.  2017.  Verification of User Interface Software: the Example of Use-Related Safety Requirements and Programmable Medical Devices. IEEE Transactions on Human-Machine Systems. 47:834-846. Abstractmedthmsv9-author_version.pdf

One part of demonstrating that a device is acceptably safe, often required by regulatory standards, is to show that it satisfies a set of requirements known to mitigate hazards. This paper is concerned with how to demonstrate that a user interface software design is compliant with use-related safety requirements. A methodology is presented based on the use of formal methods technologies to provide guidance to developers about addressing three key verification challenges: (i) how to validate a model, and show that it is a faithful representation of the device;
(ii) how to formalize requirements given in natural language, and demonstrate the benefits of the formalization process; (iii) how to prove requirements of a model using readily available formal verification tools. A model of a commercial device is used throughout the paper to demonstrate the methodology. A representative set of requirements are considered. They are based on US Food and Drug Administration (FDA) draft documentation
for programmable medical devices, and on best practice in user interface design illustrated in relevant international standards. The methodology aims to demonstrate how to achieve the FDA’s agenda of using formal methods to support the approval process for medical devices.

Campos JC, Fayollas C, Gonçalves M, Martinie C, Navarre D, Palanque P, Pinto M.  2017.  A ``More Intelligent'' Test Case Generation Approach through Task Models Manipulation. Proceedings of the ACM on Human-Computer Interaction – EICS. 1:Article9. Abstractpacmhci-eics17-accepted.pdf

Ensuring that an interactive application allows users to perform their activities and reach their goals is critical to the overall usability of the interactive application. Indeed, the effectiveness factor of usability directly refers to this capability. Assessing effectiveness is a real challenge for usability testing as usability tests only cover a very limited number of tasks and activities. This paper proposes an approach towards automated testing of effectiveness of interactive applications. To this end we resort to two main elements: an exhaustive description of users’ activities and goals using task models, and the generation of scenarios (from the task models) to be tested over the application. However, the number of scenarios can be very high (beyond the computing capabilities of machines) and we might end up testing multiple similar scenarios. In order to overcome these problems, we propose strategies based on task models manipulations (e.g., manipulating task nodes, operator nodes, information...) resulting in a more intelligent test case generation approach. For each strategy, we investigate its relevance
(both in terms of test case generation and in terms of validity compared to the original task models) and we illustrate it with a small example. Finally, the proposed strategies are applied on a real-size case study demonstrating their relevance and validity to test interactive applications.

Campos JC, Abade T, Silva JL, Harrison MD.  2017.  Don't Go In There! Using the APEX framework in the design of Ambient Assisted Living Systems. Journal of Ambient Intelligence and Humanized Computing. 8:551-566. Abstract17-jaihc-author-2.pdf

An approach to design Ambient Assisted Living systems is presented, which is based on APEX, a framework for prototyping ubiquitous environments. The approach is illustrated through the design of a smart environment within a care home for older people. Prototypes allow participants in the design process to experience the proposed design and enable developers to explore design alternatives rapidly. APEX provides the means to explore alternative environment designs virtually. The prototypes developed with APEX offered a mediating representation, allowing users to be involved in the design process. A group of residents in a city-based care home were involved in the design. The paper describes the design process as well as lessons learned for the future design of AAL systems.

Zan T, Pacheco H, Ko H, Hu Z.  2017.  BiFluX: A Bidirectional Functional Update Language for XML. 12(Information and Media Technologies):1-23.biflux.pdf
Campos JC, Sousa M, Alves M, Harrison M.  2016.  Formal Verification of a Space System's User Interface with the IVY workbench. IEEE Transactions on Human-Machine Systems. 46(2):303-316. Abstractthms-paper-author_version.pdf

This paper describes the application of the IVY workbench to the formal analysis of a user interface for a safety-critical aerospace system. The operation manual of the system was used as a requirement document, and this made it possible to build a reference model of the user interface, focusing on navigation between displays, the information provided by each display, and how they are interrelated. Usability-related property specification patterns were then used to derive relevant properties for verification. This paper discusses both the modeling strategy and the analytical results found using the IVY workbench. The purpose of the reference model is to provide a standard against which future versions of the interface may be assessed.

Gonçalves RC, Batory D, Sobral JL.  2016.  ReFlO: an interactive tool for pipe-and-filter domain specification and program generation. Software and Systems Modeling. 15(2):377-395. Abstract22.pdf

ReFlO is a framework and interactive tool to record and systematize domain knowledge used by experts to derive complex pipe-and-filter (PnF) applications. Domain knowledge is encoded as transformations that alter PnF graphs by refinement (adding more details), flattening (removing modular boundaries), and optimization (substituting inefficient PnF graphs with more efficient ones). All three kinds of transformations arise in reverse-engineering legacy PnF applications. We present the conceptual foundation and tool capabilities of ReFlO, illustrate how parallel PnF applications are designed and generated, and how domain-specific libraries of transformations are developed.

Jongmans S-STQ, Clarke D, Proença J.  2016.  A procedure for splitting data-aware processes and its application to coordination. Science of Computer Programming. 115-116:47-78. Abstractsplitreo-scp.pdfWebsite

n/a

J P, JO P.  2016.  Efficient Deduplication in a Distributed Primary Storage Infrastructure. ACM Transactions on Storage (TOS). 12(4):35.pp16.pdf
Lourenço CB, Frade MJ, Pinto JS.  2016.  A Single-Assignment Translation for Annotated Programs. CoRR. abs/1601.00584 Abstractsatranslation.pdfWebsite

We present a translation of While programs annotated with loop invariants into a dynamic single-assignment language with a dedicated iterating construct. We prove that the translation is sound and complete. This is a companion report to our paper Formalizing Single-assignment Program Verification: an Adaptation-complete Approach.

Machado N, Quinta D, Lucia B, Rodrigues L.  2016.  Concurrency Debugging with Differential Schedule Projections. ACM Transactions on Software Engineering and Methodology (TOSEM). 25(2)17.pdfWebsite
Macedo N, Jorge T, Cunha A.  2016.  A feature-based classification of model repair approaches. IEEE Transactions on Software Engineering. repair16.pdf
Almeida JB, Barbosa M, Pacheco H, Pereira V.  2016.  A Tool-Chain for High-Assurance Cryptographic Software. ERCIM News. 2016 Abstract16ercimnews.pdfWebsite

Cryptography is an inherently interdisciplinary area and the development of high-quality cryptographic software is a time-consuming task drawing on skills from mathematics, computer science and electrical engineering, only achievable by highly skilled programmers. The challenge is to map high-level cryptographic specifications phrased using mathematical abstractions into efficient implementations at the level of C or assembly that can be deployed on a target computational platform, whilst adhering to the specification both in terms of correctness and security. The High Assurance Software Laboratory at INESC-TEC maintains a domain-specific toolchain for the specification, implementation and verification of cryptographic software centred on CAO, a cryptography analyses and operations-aware language.

Fontaínhas EG, Andrade F, Almeida JB.  2016.  Do consentimento para a utilização de testemunhos de conexão (cookies). SCIENTIA IVRIDICA. 65(341):173-206. Abstract16scientiaivridica.pdf

O n.º 3 do artigo 5.º da Diretiva da Privacidade Eletrónica ( Directiva 2002/58/CE) estabelece os requisitos para o armazenamento e acesso a informação armazenada no terminal do utilizador ou assinante. Esta norma aplica-se à utilização de testemunhos de conexão (cookies), entendidos na aceção da definição dada pela norma RFC 6265 da Internet Engineering Task Force (IETF).

Na sua versão original, a Diretiva da Privacidade Eletrónica permitia a utilização de redes de comunicações eletrónicas para a armazenagem de informações ou para obter acesso à informação armazenada no equipamento terminal de um assinante ou utilizador, na condição de serem prestadas ao assinante ou utilizador informações claras e completas, nomeadamente sobre as finalidades do processamento e de, cumulativamente, lhe ser garantido o direito de recusar o tratamento (direito de autoexclusão ou direito de opt-out). Em 2009, a Diretiva dos Cidadãos (Diretiva 2009/136/CE) veio dar uma nova redação ao n.º 3 do artigo 5.º da Diretiva da Privacidade Eletrónica e passou a fazer depender a utilização de cookies da prévia obtenção do consentimento da pessoa em causa (direito de opt-in).

O novo requisito de consentimento veio abalar as práticas correntes no que respeita à utilização de cookies e está na base de um aceso debate sustentado pelas dúvidas acerca da sua interpretação e condições de implementação prática.

Procuramos, com este trabalho, contribuir para o esclarecimento dos conceitos de cookies e de consentimento enquanto fundamento legitimante para a sua utilização.

Ramos MVM, Almeida JB, Moreira N, de Queiroz RJGB.  2016.  Formalization of the Pumping Lemma for Context-Free Languages. Journal of Formalized Reasoning. 9(2):53-68. Abstract16jfr.pdfWebsite

Context-free languages are highly important in computer language processing technology as well as in formal language theory. The Pumping Lemma is a property that is valid for all context-free languages, and is used to show the existence of non context-free languages. This paper presents a formalization, using the Coq proof assistant, of the Pumping Lemma for context-free languages.

Madeira A, Neves R, Martins MA.  2016.  An exercise on the generation of many-valued dynamic logics. J. Log. Algebr. Meth. Program.. 85:1011–1037. Abstract8.pdfWebsite

n/a

Neves R, Madeira A, Martins MA, Barbosa L{\'ı}s S.  2016.  Proof theory for hybrid(ised) logics. Sci. Comput. Program.. 126:73–93. AbstractWebsite
n/a