DATAMOD 2019: 8TH INTERNATIONAL SYMPOSIUM "FROM DATA TO MODELS AND BACK (DATAMOD)
PROGRAM FOR MONDAY, OCTOBER 7TH
Days:
next day
all days

View: session overviewtalk overview

09:00-10:00 Session 1

No talks scheduled to allow for attendence of keynotes at other workshops.

10:30-12:30 Session 2: Verification

Invited speaker and accepted papers

10:30
Verification of Data in Space and Time

ABSTRACT. Research data can take very many forms, but in many cases there are interesting relations between elements of data. Such relations could be of various nature, for example causal relations, temporal relations, spatial relations or any combination thereof, to mention a few. Reasoning about time and space and their combination has a long history. Only more recently, reasoning about spatial aspects of systems, that is, the properties of entities that relate to their position, distance, connectivity and reachability in space, have received increasing attention in computer science. We present recent results in spatial and spatio-temporal logic, that have their origin in Modal logic and early work dating back to McKinsey and Tarksi, and their evolution into efficient spatial and spatio-temporal model checking methods. We illustrate these methods by their application to various domains ranging from smart public transportation to medical imaging. In the latter domain, data-analysis techniques, such as machine learning, provide a popular new area of research too, opening the way for an interesting discussion on how various methods could be used profitable in a complementary way.

11:30
Validation of a Simulation Algorithm for Safety-Critical Human Multitasking

ABSTRACT. Multitasking has become surprisingly present in our life. This is mostly due to the fact that nowadays most of our activities involve the interaction with one or more devices. In such a context the brain mechanism of \emph{selective attention} plays a key role in determining the success of a human's interaction with a device. Indeed, it is a resource to be shared among the concurrent tasks to be performed, and the sharing of attention turns out to be a process similar to process scheduling in operating systems. In order to study human multitasking situations in which a user interacts with more than one device at the same time, we proposed in a previous work an algorithm for simulating human selective attention. Our algorithm focuses, in particular, on safety-critical human multitasking, namely situations in which some of the tasks the user is involved in may lead to dangerous consequences if not executed properly. In this paper, we present the validation of such an algorithm against data gathered from an experimental study performed with real users involved concurrently in a ``main" task perceived as safety-critical and in a series of ``distractor" tasks having different levels of cognitive load.

12:00
An Ontology-based Approach to Support Formal Verification of Concurrent Systems

ABSTRACT. Formal verification ensures the absence of design errors in a system with respect to system's requirements. This is especially important for the control software of critical systems, ranging from automatic components of avionics and spacecrafts to modules of distributed banking transactions. In this paper, we present a verification support that automatically extracts a concurrent system's requirements from the technical documentation and formally verifies the system design using an external or built-in verification tool that checks whether the system meets the extracted requirements. Our support approach also provides visualization and editing options for both the system model and requirements. The key data components of our support are ontological descriptions of the verified system and its requirements. We describe the methods used by our system modules and we illustrate their work for the use case of an automatic control system.

14:00-15:00 Session 3: Data-driven Models

Accepted papers

14:00
How to look next? A data-driven approach for scanpath prediction

ABSTRACT. By and large, current visual attention models mostly rely, when considering static stimuli, on the following procedure. Given an image, a saliency map is computed, which, in turn, might serve the purpose of predicting a sequence of gaze shifts, namely a scanpath instantiating the dynamics of visual attention deployment. The temporal pattern of attention unfolding is thus confined to the scanpath generation stage, whilst salience is conceived as a static map, at best conflating a number of factors (bottom-up information, top-down, spatial biases, etc.). In this note we propose a novel sequential scheme that consists of a three-stage processing relying on a center-bias model, a context/layout model, and an object-based model, respectively. Each stage contributes, at different times, to the sequential sampling of the final scanpath. We compare the method against classic scanpath generation that exploits state-of-the-art static saliency model. Results show that accounting for the structure of the temporal unfolding leads to gaze dynamics close to human gaze behaviour.

14:30
"Know Thyself" How Personal Music Tastes Shape the Last.Fm Online Social Netwrok

ABSTRACT. As Nietzsche once wrote "Without music, life would be a mistake". The music we listen reflects our personality, our way to approach life. In order to enforce self-awareness we devised a Personal Listening Data Model that allow for capturing individual music preferences and patterns of music consumption. We applied our model to 30k users of Last.Fm for which we collected both friendship ties and multiple listening. Starting from such rich data we performed an analysis whose final aim was twofold: (i) capture, and characterize, the individual dimension of music consumption in order to identify clusters of like-minded Last.Fm users; (ii) analyze if, and how, such clusters relates to the social structure expressed by the users in the service. Do exist individuals having similar Personal Listening Data Models? If so, are they directly connected in the social graph or belong to a same community?

15:30-16:30 Session 4: Modelling

Invited speaker

15:30
Diagrammatic physical robot models in RoboSim

ABSTRACT. Simulation is a favoured technique for analysis of robotic systems. Lack of standardisation and portability between simulators, however, has impact on usability and cost of simulations. We present RoboSim, a diagrammatic tool-independent domain-specific language to model robotic platforms and their controllers. It can be regarded as a profile of UML/SysML enriched with time primitives, differential equations, and a formal process algebraic semantics. In RoboSim, a robotic platform is specified by a block diagram, which can be linked to a data model to characterise how events, variables, and operations of the software controller map to inputs and outputs of sensors and actuators. The behaviours of inputs, outputs, and joints are specified by systems of differential algebraic equations. Simulations and mathematical models for proof can be generated automatically from RoboSim models.