Recent Publications

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
Harrison MD, Drinnan M, Campos JC, Masci P, Freitas L, Di Maria C, Whitaker M.  2017.  Safety analysis of software components of a dialysis machine using model checking. 14th International Conference on Formal Aspects of Component Software. Springer Lecture Notes in Computer Science (LNCS) vol. 10487 Abstractpaper_7.pdf

The paper describes the practical use of a model checking technique to contribute to the risk analysis of a new paediatric dialysis machine. The formal analysis focuses on one component of the system, namely the table-driven software controller which drives the dialysis cycle and deals with error management. The analysis provided evidence of the verification of risk control measures relating to the software component. The paper describes the productive dialogue between the developers of the device, who had no experience or knowledge of formal methods, and an analyst who had experience of using the formal analysis tools. There were two aspects to this dialogue. The first concerned the translation of safety requirements so that they preserved the meaning of the requirement. The second involved understanding the relationship between the software component under analysis and the broader concern of the system as a whole. The paper focuses on the process, highlighting how the team recognised the advantages over a more traditional testing approach.

Palmieri M, Bernardeschi C, Masci P.  2017.  Co-simulation of semi-autonomous systems: the Line Follower Robot case study. 1st Workshop on Formal Co-Simulation of Cyber-Physical Systems (CoSim-CPS), LNCS Springer. 10729 Abstractcosim-cps-17_paper_4.pdf

Semi-autonomous systems are capable of sensing their environment and perform their tasks autonomously, but they may also be supervised by humans. The shared manual/automatic control makes the dynamics of such systems more complex, and undesirable and hardly predictable behaviours can arise from human-machine interaction. When these systems are used in critical applications, such as autonomous driving or robotic surgery, the identification of conditions that may lead the system to violate safety requirements is of main concern, since people actually entrust their life on them. In this paper, we extend an FMI-based co-simulation framework for cyber-physical systems with the possibility of modelling semi-autonomous robots. Co-simulation can be used to gain more insights on the system under analysis at early stages of system development, and to highlight the impact of human interaction on safety. This approach is applied to the Line Follower Robot case study, available in the INTO-CPS project.

Pinto M, Goncalves M, Masci P, Campos JC.  2017.  TOM: a Model-Based GUI Testing framework. 14th International Conference on Formal Aspects of Component Software. 10487 Abstractpaper_25.pdf

Applying model-based testing to interactive systems enables the systematic testing of the system by automatically simulating user actions on the user interface. It reduces the cost of (expensive) user testing by identifying implementations errors without the involvement of human users, but raises a number of specific challenges, such as how to achieve good coverage of the actual use of the system during the testing process. This paper describes TOM, a model-based testing framework that uses a combination of tools and mutation testing techniques to maximize testing of user interface behaviors

Oliveira JN, Macedo H.  2017.  The Data Cube As a Typed Linear Algebra Operator. Proc. of the 16th Int. Symposium on Database Programming Languages. :6:1–6:11. Abstract
Santos A, Cunha A, Macedo N, Arrais R, dos Santos FN.  2017.  Mining the Usage Patterns of ROS Primitives. Abstractros_patterns.pdf

The Robot Operating System (ROS) is nowadays one of the most popular frameworks for developing robotic
applications. To ensure the (much needed) dependability and safety of such applications we forecast an increasing demand for ROS-specific coding standards, static analyzers, and tools alike. Unfortunately, the development of such standards and tools can be hampered by ROS modularity and configurability, namely the substantial number of primitives (and respective variants) that must, in principle, be considered.
To quantify the severity of this problem, we have mined a large number of existing
ROS packages to understand how its primitives are used in practice, and to determine which combinations of primitives are most popular. This paper presents and discusses the results of this study, and hopefully provides some guidance for future standardization efforts and tool developers.

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


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