Abstract
This paper explores the role of formal methods as part of the user-centred design of interactive systems. An iterative process is described, developing prototypes incrementally, proving user-centred requirements while at the same time evaluating the prototypes that are executable forms of the developed models using 'traditional' techniques for user evaluation. A formal analysis complements user evaluations. This approach enriches user-centred design that typically focuses understanding on context and producing sketch designs. These sketches are often non-functional (e.g. paper) prototypes. They provide a means of exploring candidate design possibilities using techniques such as cooperative evaluation. This paper describes a further step in the process using formal analysis techniques. The use of formal methods provides a systematic approach to checking plausibility and consistency during early design stages, while at the same time enabling the generation of executable prototypes. The technique is illustrated through an example based on a pill dispenser.

Abstract
Index structures were often used to optimise fetch operations to external storage devices (secondary memory). Nowadays, this also holds for increasingly large amounts of data residing in main-memory (primary memory). Within this scope, this work focuses on index structures that efficiently insert, query and delete valid-time data from very large datasets. This work performs a comparative study on the performance of the Interval B+ tree (IB+ tree) and the Improved Interval B+ tree (I2B+ tree): a variant that improves the time-efficiency of the deletion operation by reducing the number of traversed nodes to access siblings. We performed an extensive analysis of the performance of two operations: insertions and deletions, on both index structures, using multiple datasets with growing volumes of data, distinct temporal distributions and tree parameters (time-split alpha and node order). Results confirm that the I2B+ tree globally outperforms the IB+ tree, since, on average, deletion operations are 7% faster, despite insertions requiring 2% more time. Furthermore, results also allowed to determine the key factors that augment the performance difference on deletions between both trees. Copyright © 2021 by Author/s and Licensed by Veritas Publications Ltd., UK.

Abstract
Public spaces like concert stadiums and sporting arenas are ideal venues for AR content delivery to crowds of mobile phone users. Unfortunately, these environments tend to be some of the most challenging in terms of lighting and dynamic staging for vision-based relocalization. In this paper, we introduce FLASH1, a system for delivering AR content within challenging lighting environments that uses active tags (i.e., blinking) with detectable features from passive tags (quads) for marking regions of interest and determining pose. This combination allows the tags to be detectable from long distances with significantly less computational overhead per frame, making it possible to embed tags in existing video displays like large jumbotrons. To aid in pose acquisition, we implement a gravity-assisted pose solver that removes the ambiguous solutions that are often encountered when trying to localize using standard passive tags. We show that our technique outperforms similarly sized passive tags in terms of range by 20-30% and is fast enough to run at 30 FPS even within a mobile web browser on a smartphone.

Abstract

Abstract
Deepfake in multimedia content is being increasingly used in a plethora of cybercrimes, namely those related to digital kidnap, and ransomware. Criminal investigation has been challenged in detecting manipulated multimedia material, by applying machine learning techniques to distinguish between fake and genuine photos and videos. This paper aims to present a Support Vector Machines (SVM) based method to detect tampered photos. The method was implemented in Python and integrated as a new module in the widely used digital forensics application Autopsy. The method processes a set of features resulting from the application of a Discrete Fourier Transform (DFT) in each photo. The experiments were made in a new and large dataset of classified photos containing both legitimate and manipulated photos, and composed of objects and faces. The results obtained were promising and reveal the appropriateness of using this method embedded in Autopsy, to help in criminal investigation activities and digital forensics.

Abstract
Virtual Reality could be useful for heritage management and preservation by complementing or, even, by replacing the ‘real’ visitation to more threatened destinations. The objective of this study was to empirically test the level of similarity perceived by a group of students between VR experience and the ‘real’ visit in a UNESCO World Heritage Cultural attraction in order to assess the capacity of VR to act as a substitute of the ‘real’ visit. Ridit analysis was conducted in order to rank the level of agreement perceived by respondents concerning to similarity between the VR experience and the ‘real’ visit. Results revealed that VR experience could act as a complement, rather than a substitute of the ‘real’ visitation. This is, the feelings and emotions derived from the ‘real’ visit could not be replaced by the VR experience. VR could be an effective marketing tool to encourage sustainable tourism behaviors, rather than to substitute the ‘real’ visit. © 2021, The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.