9 result(s)
Page Size: 10, 20, 50
Export: bibtex, xml, json, csv
Order by:

CNR Author operator: and / or
Typology operator: and / or
Language operator: and / or
Date operator: and / or
Rights operator: and / or
2022 Conference article Open Access OPEN

Formal modeling and initial analysis of the 4SECURail case study
Mazzanti F., Belli D.
We present the case study developed in the context of the 4SECURail project and the approach used for its formal modeling and analysis. Starting from a simple SysML/UML behavioral model of the system requirements, three formal models have been developed using three different frameworks, namely UMC, ProB, and CADP/LNT. The paper shows how the different ways to represent and analyze the system from the three different points of view allow us to take advantage of the resulting diversity.Source: MARS 2022 - Fifth Workshop on Models for Formal Analysis of Real Systems, pp. 118–144, Munich, DE, 01/04/2022
DOI: 10.4204/eptcs.355.6
Project(s): 4SECURAIL via OpenAIRE

See at: eptcs.web.cse.unsw.edu.au Open Access | ISTI Repository Open Access | CNR ExploRA Open Access


2022 Software Unknown

Multivariate time series dataset generator
Belli D., Miori V.
A Java class that provides constructors and methods to generate synthetic data sets of multi-variate time series with/without anomalies. The class Random is used to introduce the right percentage of aleatority to the generation of the signals. Temporal patterns have been modeled based on trigonometric functions, randomly selected feature by feature. To reproduce the anomalies, a little noise is added to the generated signals. The class has been designed to test machine learning algorithms developed for anomaly detection in multivariate time series data.

See at: github.com | CNR ExploRA


2021 Report Open Access OPEN

4SECURail - Technical Informative Note 15 - Progress Report: Formal development Demonstrator Prototype
Mazzanti F., Belli D.
This Technical Informative Note describes the progress of the activity of Work Package 2 / Task 2.3 in the months 12-17 of the project 4SECURail. The final results of Task 2.3 will be described in Deliverable 2.5, due at month 20 (end of July 2021). This Technical Informative Note is likely to already contain most of the interesting results that will appear in the final deliverable, together with other less important internal progress details that for readability issues will not appear in the final version. The overall final purpose of the whole experimentation is the observation of the impact, in our specific case, i.e. applying our specific tools and methodologies1 to our specific case study2, of the adoption of formal methods towards the improvement of the quality of the system specifications under construction.Source: Project report, 4SECURail, TIN-FM-15, pp.1–53, 2021
Project(s): 4SECURAIL via OpenAIRE

See at: ISTI Repository Open Access | CNR ExploRA Open Access


2021 Report Open Access OPEN

4SECURail - Revised requirements of the 4SECURail case study
Mazzanti F., Belli D.
The final version of the system requirements of the case study used in the 4SECURail demonstratorSource: ISTI Project report, 4SECURail, 2021
DOI: 10.5281/zenodo.5541217
Project(s): 4SECURAIL via OpenAIRE

See at: ISTI Repository Open Access | CNR ExploRA Open Access


2021 Software Unknown

Formal models of the SAI/CSL system of the 4SECURail case study
Mazzanti F., Belli D.
Formal models of 4SECURAIL case study in the notation accepted by UMC, ProB, CADP/LNTDOI: 10.5281/zenodo.5541307
Project(s): 4SECURAIL via OpenAIRE

See at: CNR ExploRA


2021 Software Unknown

The UMC2LNT and UMC2PROB model transformation tools
Mazzanti F., Belli D.
This documents contains the source code of two trasformation tools used in the 4SECURail project. The tools umc2lnt takes as argument the name of a file contining an UMC model and generates the corresponding CADP/LNT model.DOI: 10.5281/zenodo.5541350
Project(s): 4SECURAIL via OpenAIRE

See at: CNR ExploRA


2021 Journal article Open Access OPEN

How mobility and sociality reshape the context: a decade of experience in mobile crowdsensing
Girolami M., Belli D., Chessa S., Foschini L.
The possibility of understanding the dynamics of human mobility and sociality creates the opportunity to re-design the way data are collected by exploiting the crowd. We survey the last decade of experimentation and research in the field of mobile CrowdSensing, a paradigm centred on users' devices as the primary source for collecting data from urban areas. To this purpose, we report the methodologies aimed at building information about users' mobility and sociality in the form of ties among users and communities of users. We present two methodologies to identify communities: spatial and co-location-based. We also discuss some perspectives about the future of mobile CrowdSensing and its impact on four investigation areas: contact tracing, edge-based MCS architectures, digitalization in Industry 5.0 and community detection algorithms.Source: Sensors (Basel) 21 (2021). doi:10.3390/s21196397
DOI: 10.3390/s21196397

See at: ISTI Repository Open Access | CNR ExploRA Open Access | www.mdpi.com Open Access


2021 Report Open Access OPEN

4SECURail - Formal development demonstrator prototype, final release
Mazzanti F., Belli D.
This Deliverable describes the final results of Task 2.3 of 4SECURail project. The goal of Task 2.3 is to apply the formal development demonstrator process defined in Task 2.1 to the signalling case study defined in Task 2.2 and to describe the observed impact of the selected tools and methodologies for improving the quality of the system specifications under analysis.Source: ISTI Project report, 4SECURail, 2021
Project(s): 4SECURAIL via OpenAIRE

See at: ISTI Repository Open Access | CNR ExploRA Open Access


2020 Conference article Restricted

Impact of evolutionary community detection algorithms for edge selection strategies
Barsocchi P., Belli D., Chessa S., Foschini L., Girolami M.
The combination of the edge computing paradigm with Mobile CrowdSensing (MCS) is a promising approach. However, the selection of the proper edge nodes is a crucial aspect that greatly affects the performance of the extended architecture. This work studies the performance of an edge-based MCS architecture with ParticipAct, a real-word experimental dataset. We present a community-based edge selection strategy and we measure two key metrics, namely latency and the number of requests satisfied. We show how they vary by adopting three evolutionary community detection algorithms, TILES, Infomap and iLCD configured by changing several configuration settings. We also study the two metrics, by varying the number of edge nodes selected so that to show its benefit.Source: GLOBECOM 2020 - IEEE Global Communications Conference, Taipei, Taiwan, December 07-11, 2020
DOI: 10.1109/globecom42002.2020.9348085

See at: Archivio istituzionale della ricerca - Alma Mater Studiorum Università di Bologna Restricted | ieeexplore.ieee.org Restricted | CNR ExploRA Restricted | xplorestaging.ieee.org Restricted