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

CNR Author operator: and / or
more
Typology operator: and / or
Language operator: and / or
Date operator: and / or
more
Rights operator: and / or
2021 Contribution to journal Open Access OPEN

Preface. Fundamentals of Software Engineering (extended versions of selected papers of FSEN 2019)
Hojjat H., Massink M.
Source: Science of computer programming (Print) 206 (2021). doi:10.1016/j.scico.2021.102626
DOI: 10.1016/j.scico.2021.102626

See at: ISTI Repository Open Access | Science of Computer Programming Restricted | Science of Computer Programming Restricted | CNR ExploRA Restricted | www.sciencedirect.com Restricted


2021 Conference article Open Access OPEN

Feasibility of Spatial Model Checking for Nevus Segmentation
Belmonte G., Broccia G., Ciancia V., Latella D., Massink M.
Recently developed spatial and spatio-temporal model checking techniques have a wide range of application domains, among which large scale distributed systems as well as signal and image analysis. In the latter domain, automatic and semi-automatic contouring in Medical Imaging has shown to be a very promising and versatile application that may facilitate the work of professionals in this domain, while supporting explainability, easy replicability and exchange of medical image analysis methods. In recent work, spatial model-checking has been applied to the 3D contouring of brain tumours and related oedema in magnetic resonance images of the brain. In the present paper we address the contouring of 2D images of nevi. One of the challenges of contouring nevi is that they show considerable inhomogeneity in shape, colour, texture and size. In addition these images often include also extraneous elements such as hairs, patches and rulers. To deal with this challenge we explore the use of a texture similarity operator in combination with spatial logic operators. We investigate the feasibility of our technique on images of a large public database. We compare the results with associated ground truth segmentation provided by domain experts; the results are very promising, both from the quality and from the performance point of view.Source: FormaliSE: International Conference on Formal Methods in Software Engineering, pp. 1–12, 18-21/05/2021
DOI: 10.1109/formalise52586.2021.00007

See at: ISTI Repository Open Access | CNR ExploRA Restricted | www.computer.org Restricted


2021 Report Open Access OPEN

Geometric Model Checking of Continuous Space
Bezhanishvili N., Ciancia V., Gabelaia D., Grilletti G., Latella D., Massink M.
Topological Spatial Model Checking is a recent paradigm that combines Model Checking with the topological interpretation of Modal Logic. The Spatial Logic of Closure Spaces, SLCS, extends Modal Logic with reachability connectives that, in turn, can be used for expressing interesting spatial properties, such as "being near to" or "being surrounded by". SLCS constitutes the kernel of a solid logical framework for reasoning about discrete space, such as graphs and digital images, interpreted as quasi discrete closure spaces. In particular, the spatial model checker VoxLogicA, that uses an extended version of SLCS, has been used successfully in the domain of medical imaging. However, SLCS is not restricted to discrete space. Following a recently developed geometric semantics of Modal Logic, we show that it is possible to assign an interpretation to SLCS in continuous space, admitting a model checking procedure, by resorting to models based on polyhedra. In medical imaging such representations of space are increasingly relevant, due to recent developments of 3D scanning and visualisation techniques that exploit mesh processing. We demonstrate feasibility of our approach via a new tool, PolyLogicA, aimed at ecient verication of SLCS formulas on polyhedra, while inheriting some well-established optimization techniques already adopted in VoxLogicA. Finally, we cater for a geometric definition of bisimilarity, proving that it characterises logical equivalence.Source: Research report, IT- MaTTerS, PRIN 2017FTXR7S, 2021

See at: arxiv.org Open Access | ISTI Repository Open Access | CNR ExploRA Open Access


2021 Report Open Access OPEN

On Bisimilarities for Closure Spaces - Preliminary Version
Ciancia V., Latella D., Massink M., De Vink E.
Closure spaces are a generalisation of topological spaces obtained by removing the idempotence requirement on the closure operator. We adapt the standard notion of bisimilarity for topological models, namely Topo-bisimilarity, to closure models|we call the resulting equivalence CM-bisimilarity|and rene it for quasi-discrete closure models. We also dene two additional notions of bisimilarity that are based on paths on space, namely Path-bisimilarity and Compatible Path-bisimilarity, CoPa-bisimilarity for short. The former expresses (unconditional) reachability, the latter renes it in a way that is reminishent of Stuttering Equivalence on transition systems. For each bisimilarity we provide a logical characterisation, using variants of SLCS.We also address the issue of (space) minimisation via the three equivalences.Source: Research report, ITMaTTerS, PRIN 2017FTXR7S, 2021

See at: arxiv.org Open Access | ISTI Repository Open Access | CNR ExploRA Open Access


2021 Conference article Closed Access

A hands-on introduction to spatial model checking using VoxLogicA
Ciancia V., Belmonte G., Latella D., Massink M.
This paper provides a tutorial-style introduction, and a guide, to the recent advancements in spatial model checking that have made some relevant results possible. Among these, we mention fully automated segmentation of regions of interest in medical images by short, unambiguous spatial-logical specifications. This tutorial is aimed both at domain experts in medical imaging who would like to learn simple (scripting-alike) techniques for image analysis, making use of a modern, declarative language, and at experts in Formal Methods in Computer Science and Model Checking who would like to grasp how the theory of Spatial Logic and Model Checking has been turned into logic-based, dataset-oriented imaging techniques.Source: SPIN 2021 - 27th International Symposium on Model Checking Software, pp. 22–41, Online conference, 12/07/2021
DOI: 10.1007/978-3-030-84629-9_2

See at: link.springer.com Restricted | CNR ExploRA Restricted


2021 Conference article Open Access OPEN

Spatial Model Checking for Smart Stations: Research Challenges
Ter Beek M. H., Ciancia V., Latella D., Massink M., Spagnolo G. O.
In this position paper, we discuss the introduction of spatial verification techniques in an application scenario from smart stations, viz. analysing the user experience with respect to the lighting conditions of station areas. This is a case study in industrial projects. We discuss three challenging use cases for the application of spatial model checking in this setting. First, we envision how to use the spatial model checker VoxLogicA, which can analyse both 2D and 3D voxel-based maps, to explore the areas that users can visit in a station area and to characterise them with respect to their illumination conditions. This is aimed at monitoring a smart station. We also ideate statistical spatio-temporal model checking of the design of energy-saving protocols, exploiting the modelling of user preferences. Finally, we discuss the idea of quantifying the impact of design changes, based on the logs of smart stations, to identify and measure the incidence of undesired events (e.g. non-illuminated platforms where a train is passing by) before and after each change.Source: FMICS 2021 - 26th International Conference on Formal Methods for Industrial Critical Systems, pp. 39–47, Online conference, 24-26/08/2021
DOI: 10.1007/978-3-030-85248-1_3

See at: ISTI Repository Open Access | link.springer.com Restricted | CNR ExploRA Restricted


2020 Conference article Open Access OPEN

Refined mean field analysis: the gossip shuffle protocol revisited
Gast N., Latella D., Massink M.
Gossip protocols form the basis of many smart collective adaptive systems. They are a class of fully decentralised, simple but robust protocols for the distribution of information throughout large scale networks with hundreds or thousands of nodes. Mean field analysis methods have made it possible to approximate and analyse performance aspects of such large scale protocols in an efficient way that is independent of the number of nodes in the network. Taking the gossip shuffle protocol as a benchmark, we evaluate a recently developed refined mean field approach. We illustrate the gain in accuracy this can provide for the analysis of medium size models analysing two key performance measures: replication and coverage. We also show that refined mean field analysis requires special attention to correctly capture the coordination aspects of the gossip shuffle protocol.Source: COORDINATION 2020 - 22nd IFIP WG 6.1 International Conference, held as part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15-19, 2020, Proceedings, pp. 230–239, Valletta, Malta, 15-19 June 2020
DOI: 10.1007/978-3-030-50029-0_15

See at: Europe PubMed Central Open Access | link.springer.com Open Access | ISTI Repository Open Access | academic.microsoft.com Restricted | Hal-Diderot Restricted | Hal-Diderot Restricted | Hal-Diderot Restricted | link.springer.com Restricted | link.springer.com Restricted | CNR ExploRA Restricted | rd.springer.com Restricted | www.scilit.net Restricted


2020 Report Open Access OPEN

Towards Spatial Bisimilarity for Closure Models: Logical and Coalgebraic Characterisations
Ciancia V., Latella D., Massink M., De Vink E.
The topological interpretation of modal logics provides descriptive languages and proof systems for reasoning about points of topological spaces. Recent work has been devoted to model checking of spatial logics on discrete spatial structures, such as finite graphs and digital images, with applications in various case studies including medical image analysis. These recent developments required a generalisation step, from topological spaces to closure spaces. In this work we initiate the study of bisimilarity and minimisation algorithms that are consistent with the closure spaces semantics. For this purpose we employ coalgebraic models. We present a coalgebraic definition of bisimilarity for quasi-discrete models, which is adequate with respect to a spatial logic with reachability operators, complemented by a free and open-source minimisation tool for finite models. We also discuss the non-quasi-discrete case, by providing a generalisation of the well-known set-theoretical notion of topo-bisimilarity, and a categorical definition, in the same spirit as the coalgebraic rendition of neighbourhood frames, but employing the covariant power set functor, instead of the contravariant one. We prove its adequacy with respect to infinitary modal logic.Source: ISTI Technical Reports 015/2020, 2020, 2020
DOI: 10.32079/isti-tr-2020/015

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


2020 Report Open Access OPEN

Using Spatial Logic and Model Checking for Nevus Segmentation
Belmonte G., Broccia G., Ciancia V., Latella D., Massink M.
Spatial and spatio-temporal model checking techniques have a wide range of application domains, among which large scale distributed systems and signal and image analysis. In the latter domain, automatic and semi-automatic contouring in Medical Imaging has shown to be a very promising and versatile application that can greatly facilitate the work of professionals in this domain, while supporting explainability, easy replicability and exchange of medical image analysis methods. In recent work we have applied this model-checking technique to the (3D) contouring of tumours and related oedema in magnetic resonance images of the brain. In the current work we address the contouring of (2D) images of nevi. One of the challenges of treating nevi images is their considerable inhomogeneity in shape, colour, texture and size. To deal with this challenge we use a texture similarity operator, in combination with spatial logic operators. We apply our technique on images of a large public database and compare the results with associated ground truth segmentation provided by domain experts.Source: ISTI Technical Reports 2020/017, 2020, 2020
DOI: 10.32079/isti-tr-2020/017

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


2020 Report Open Access OPEN

Refined Mean Field Analysis of the Gossip Shuffle Protocol -- extended version --
Gast N., Latella D., Massink M.
Gossip protocols form the basis of many smart collective adaptive systems. They are a class of fully decentralised, simple but robust protocols for the distribution of information throughout large scale networks with hundreds or thousands of nodes. Mean field analysis methods have made it possible to approximate and analyse performance aspects of such large scale protocols in an efficient way. Taking the gossip shuffle protocol as a benchmark, we evaluate a recently developed refined mean field approach. We illustrate the gain in accuracy this can provide for the analysis of medium size models analysing two key performance measures. We also show that refined mean field analysis requires special attention to correctly capture the coordination aspects of the gossip shuffle protocol.Source: ISTI Technical Reports 2020/018, 2020, 2020
DOI: 10.32079/isti-tr-2020/018

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


2019 Conference article Open Access OPEN

VoxLogicA: a spatial model checker for declarative image analysis
Belmonte G., Ciancia V., Latella D., Massink M.
Spatial and spatio-temporal model checking techniques have a wide range of application domains, among which large scale distributed systems and signal and image analysis.We explore a new domain, namely (semi-)automatic contouring in Medical Imaging, introducing the tool VoxLogicA which merges the state-of-the-art library of computational imaging algorithms ITK with the unique combination of declarative specification and optimised execution provided by spatial logic model checking. The result is a rapid, logic based analysis development methodology. The analysis of an existing benchmark of medical images for segmentation of brain tumours shows that simple VoxLogicA analysis can reach state-of-the-art accuracy, competing with best-in-class algorithms, with the advantage of explainability and easy replicability. Furthermore, due to a two-orders-of-magnitude speedup compared to the existing generalpurpose spatio-temporal model checker topochecker, VoxLogicA enables interactive development of analysis of 3D medical images, which can greatly facilitate the work of professionals in this domain.Source: TACAS 2019 - 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 281–298, Prague, Czech Republic, 06-11 April 2019
DOI: 10.1007/978-3-030-17462-0_16

See at: link.springer.com Open Access | link.springer.com Open Access | ISTI Repository Open Access | CNR ExploRA Open Access | academic.microsoft.com Restricted | dblp.uni-trier.de Restricted | link.springer.com Restricted | link.springer.com Restricted | rd.springer.com Restricted


2019 Contribution to book Open Access OPEN

Embedding RCC8D in the collective spatial logic CSLCS
Ciancia V., Latella D., Massink M.
Discrete mereotopology is a logical theory for the specification of qualitative spatial functions and relations defined over a discrete space, intended as a set of basic elements, the pixels, with an adjacency relation defined over it. The notions of interest are that of region, intended as an arbitrary aggregate of pixels, and of specific relations between regions. The mereotopological theory RCC8D extends the mereological theory RCC5D--a theory of region parthood for discrete spaces--with the topological notion of connection and the remaining relations (disconnection, external connection, tangential and nontangential proper parthood and their inverses). In this paper, we propose an encoding of RCC8D into CSLCS, the collective extension of the Spatial Logic of Closure Spaces SLCS. We show how topochecker, a model-checker for CSLCS, can be used for effectively checking the existence of a RCC8D relation between two given regions of a discrete space.Source: Models, Languages, and Tools for Concurrent and Distributed Programming - Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday, edited by Michele Boreale; Flavio Corradini; Michele Loreti; Rosario Pugliese, pp. 260–277. Cham Heidelberg New York Dordrecht London: Springer, 2019
DOI: 10.1007/978-3-030-21485-2_15

See at: ISTI Repository Open Access | academic.microsoft.com Restricted | dblp.uni-trier.de Restricted | link.springer.com Restricted | link.springer.com Restricted | CNR ExploRA Restricted


2019 Contribution to conference Open Access OPEN

Fundamentals of Software Engineering
Hojjat H., Massink M.
This book constitutes the thoroughly refereed post-conference proceedings of the 8th International Conference on Fundamentals of Software Engineering, FSEN 2019, held in Tehran, Iran, in May 2019. The 14 full papers and 3 short papers presented in this volume were carefully reviewed and selected from 47 submissions. The topics of interest in FSEN span over all aspects of formal methods, especially those related to advancing the application of formal methods in the software industry and promoting their integration with practical engineering techniques. The papers are organized in topical sections on agent based systems, theorem proving, learning, verification, distributed algorithms, and program analysis.Source: Cham, Heidelberg, New York, Dordrecht, London: Springer, 2019
DOI: 10.1007/978-3-030-31517-7

See at: ISTI Repository Open Access | link.springer.com Restricted | CNR ExploRA Restricted


2019 Contribution to book Open Access OPEN

Innovating Medical Image Analysis via Spatial Logics
Belmonte G., Ciancia V., Latella D., Massink M.
Current computer-assisted medical imaging for the planning of radiotherapy requires high-level mathematical and computational skills. These are often paired with the case-by-case integration of highly specialised technologies. The lack of modularity at the right level of abstraction in this field hinders research, collaboration and transfer of expertise among medical physicists, engineers and technicians. The longer term aim of the introduction of spatial logics and spatial model checking in medical imaging is to provide an open platform introducing declarative medical image analysis. This will provide domain experts with a convenient and very concise way to specify contouring and segmentation operations, grounded on the solid mathematical foundations of Topological Spatial Logics. We show preliminary results, obtained using the spatial model checker VoxLogicA, for the automatic identification of specific brain tissues in a healthy brain and we discuss a selection of challenges for spatial model checking for medical imaging.Source: From Software Engineering to Formal Methods and Tools, and Back, edited by ter Beek M.H.; Fantechi A.; Semini L. (eds.), pp. 85–109. Berlin: Springer, 2019
DOI: 10.1007/978-3-030-30985-5_7

See at: ISTI Repository Open Access | academic.microsoft.com Restricted | dblp.uni-trier.de Restricted | link.springer.com Restricted | link.springer.com Restricted | CNR ExploRA Restricted | www.scilit.net Restricted


2019 Journal article Open Access OPEN

Spatial logics and model checking for medical imaging
Banci Buonamici F., Belmonte G., Ciancia V., Latella D., Massink M.
Recent research on spatial and spatio-temporal model checking provides novel image analysis methodologies, rooted in logical methods for topological spaces. Medical imaging (MI) is a field where such methods show potential for ground-breaking innovation. Our starting point is SLCS, the Spatial Logic for Closure Spaces--closure spaces being a generalisation of topological spaces, covering also discrete space structures--and topochecker, a model checker for SLCS (and extensions thereof). We introduce the logical language ImgQL ("Image Query Language"). ImgQL extends SLCS with logical operators describing distance and region similarity. The spatio-temporal model checker topochecker is correspondingly enhanced with state-of-the-art algorithms, borrowed from computational image processing, for efficient implementation of distance-based operators, namely distance transforms. Similarity between regions is defined by means of a statistical similarity operator, based on notions from statistical texture analysis. We illustrate our approach by means of an example of analysis of Magnetic Resonance images: segmentation of glioblastoma and its oedema.Source: International journal on software tools for technology transfer (Internet) 22 (2019): 195–217. doi:10.1007/s10009-019-00511-9
DOI: 10.1007/s10009-019-00511-9

See at: ISTI Repository Open Access | International Journal on Software Tools for Technology Transfer Restricted | International Journal on Software Tools for Technology Transfer Restricted | International Journal on Software Tools for Technology Transfer Restricted | International Journal on Software Tools for Technology Transfer Restricted | International Journal on Software Tools for Technology Transfer Restricted | CNR ExploRA Restricted


2019 Contribution to conference Restricted

VoxLogicA: Voxel-based Logical Analyser
Belmonte G., Ciancia V., Latella D., Massink M.
VoxLogicA [1] is a free and open source, multi-platform tool, catering for a novel approach to image segmentation, bringing in ideas from formal methods in software engineering, rapid-development, and declarative programming languages, that have been successful in other domains. In a few lines of code, complex analyses can be specified, translating domain knowledge into logical properties. For instance, in brain tumor segmentation, logical properties encode facts such as ''the oedema touches the tumor'', or ''the tumor contains hyperintense areas; furthermore, very intense areas that are very close to hyperintense ones, are part of the tumor''. Such constraints are extremely effective at filtering noise in automated analysis. The logical core is extended by including imaging primitives, e.g., texture similarity or image normalisation. The language is ''a query language for image analysis''. Its innovation potential can be compared to that of the ''Structured Query Language'' SQL, that revolutionised automated data analysis, by permitting queries on large datasets to be designed by experts of the domain to which the data belongs, instead of computer programmers.Source: ESMRMB 2019, 36th Annual Scientific Meeting, pp. 417–418, Rotterdam, 3/10/2019-5/10/2019
DOI: 10.1007/s10334-019-00756-0

See at: Magnetic Resonance Materials in Physics Biology and Medicine Restricted | link.springer.com Restricted | Magnetic Resonance Materials in Physics Biology and Medicine Restricted | Magnetic Resonance Materials in Physics Biology and Medicine Restricted | CNR ExploRA Restricted | Magnetic Resonance Materials in Physics Biology and Medicine Restricted


2019 Contribution to journal Open Access OPEN

Preface to the special issue on Coordination Models and Languages (COORDINATION 2017)
Jacquet J. M., Massink M.
Source: Science of computer programming (Print) 180 (2019): 16–17. doi:10.1016/j.scico.2019.04.005
DOI: 10.1016/j.scico.2019.04.005

See at: ISTI Repository Open Access | Science of Computer Programming Restricted | Science of Computer Programming Restricted | Science of Computer Programming Restricted | Science of Computer Programming Restricted | CNR ExploRA Restricted | www.sciencedirect.com Restricted


2019 Journal article Open Access OPEN

VoxLogicA: a Spatial-Logic based tool for Declarative Image Analysis
Belmonte G., Ciancia V., Latella D., Massink M.
Glioblastomas are among the most common malignant intracranial tumours. Neuroimaging protocols are used before and after treatment to evaluate its effect and to monitor the evolution of the disease. In clinical studies and routine treatment, magnetic resonance images (MRI) are evaluated, largely manually, and based on qualitative criteria such as the presence of hyper-intense tissue in the image. VoxLogicA is an image analysis tool, designed to perform tasks such as identifying brain tumours in 3D magneto-resonance scans. The aim is to have a system that is portable, predictable and reproducible, and requires minimal computing expertise to operate.Source: ERCIM news 118 (2019): 12–13.
Project(s): QUANTICOL via OpenAIRE

See at: ercim-news.ercim.eu Open Access | ISTI Repository Open Access | CNR ExploRA Open Access


2018 Journal article Open Access OPEN

Spatio-temporal model checking of vehicular movement in public transport systems
Ciancia V., Gilmore S., Grilletti G., Latella D., Loreti M., Massink M.
We present the use of a novel spatio-temporal model checker to detect problems in the data and operation of a collective adaptive system. Data correctness is important to ensure operational correctness in systems which adapt in response to data. We illustrate the theory with several concrete examples, addressing both the detection of errors in vehicle location data for buses in the city of Edinburgh and the undesirable phenomenon of ``clumping'' which occurs when there is not enough separation between subsequent buses serving the same route. Vehicle location data are visualised symbolically on a street map, and categories of problems identified by the spatial part of the model checker are rendered by highlighting the symbols for vehicles or other objects that satisfy a property of interest. Behavioural correctness makes use of both the spatial and temporal aspects of the model checker to determine from a series of observations of vehicle locations whether the system is failing to meet the expected quality of service demanded by system regulators.Source: International journal on software tools for technology transfer (Internet) 20 (2018): 289–311. doi:10.1007/s10009-018-0483-8
DOI: 10.1007/s10009-018-0483-8
Project(s): QUANTICOL via OpenAIRE

See at: Archivio istituzionale della ricerca - Università di Camerino Open Access | ISTI Repository Open Access | International Journal on Software Tools for Technology Transfer Open Access | International Journal on Software Tools for Technology Transfer Restricted | International Journal on Software Tools for Technology Transfer Restricted | International Journal on Software Tools for Technology Transfer Restricted | International Journal on Software Tools for Technology Transfer Restricted | International Journal on Software Tools for Technology Transfer Restricted | International Journal on Software Tools for Technology Transfer Restricted | International Journal on Software Tools for Technology Transfer Restricted | CNR ExploRA Restricted | International Journal on Software Tools for Technology Transfer Restricted | International Journal on Software Tools for Technology Transfer Restricted | International Journal on Software Tools for Technology Transfer Restricted


2018 Journal article Open Access OPEN

A refined mean field approximation of synchronous discrete-time population models
Gast N., Latella D., Massink M.
Mean field approximation is a popular method to study the behaviour of stochastic models composed of a large number of interacting objects. When the objects are asynchronous, the mean field approximation of a population model can be expressed as an ordinary differential equation. When the objects are (clock-) synchronous the mean field approximation is a discrete time dynamical system. We focus on the latter. We study the accuracy of mean field approximation when this approximation is a discrete-time dynamical system. We extend a result that was shown for the continuous time case and we prove that expected performance indicators estimated by mean field approximation are O(1/N)-accurate. We provide simple expressions to effectively compute the asymptotic error of mean field approximation, for finite time-horizon and steady-state, and we use this computed error to propose what we call a refined mean field approximation. We show, by using a few numerical examples, that this technique improves the quality of approximation compared to the classical mean field approximation, especially for relatively small population sizes.Source: Performance evaluation 126 (2018): 1–21. doi:10.1016/j.peva.2018.05.002
DOI: 10.1016/j.peva.2018.05.002

See at: arXiv.org e-Print Archive Open Access | Performance Evaluation Open Access | ISTI Repository Open Access | Performance Evaluation Restricted | Performance Evaluation Restricted | Performance Evaluation Restricted | Performance Evaluation Restricted | Performance Evaluation Restricted | Performance Evaluation Restricted | Performance Evaluation Restricted | INRIA a CCSD electronic archive server Restricted | CNR ExploRA Restricted | Performance Evaluation Restricted | www.sciencedirect.com Restricted