32 pubblicazioni classificate nel seguente modo:

A Holonic Construction Management System for the Efficient Implementation of Building Energy Renovation Actions
SUSTAINABILITY
Autore/i: Messi, Leonardo; Carbonari, Alessandro; Franco, Carlos; Spegni, Francesco; Vaccarini, Massimo; Naticchia, Berardo
Classificazione: 1 Contributo su Rivista
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/327411

APPLICATION OF DIMINISHED REALITY FOR CONSTRUCTION SITE SAFETY MANAGEMENT
Proceedings of the 23rd International Conference on Construction Applications of Virtual Reality
Autore/i: Corneli, Alessandra; Naticchia, Berardo; Vaccarini, Massimo; Carbonari, Alessandro; Spegni, Francesco
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/325621

Seamless indoor/outdoor marker-less augmented reality registration supporting facility management operations
Proceedings of the 23rd International Conference on Construction Applications of Virtual Reality
Autore/i: Messi, Leonardo; Spegni, Francesco; Vaccarini, Massimo; Corneli, Alessandra; Binni, Leonardo
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Abstract: Augmented reality (AR) still struggles to be widely used in real processes in the construction industry despite its great potential. This is partly due to the difficulties that exist in aligning holograms and maintaining their stability, especially for outdoor applications. In addition, being indoor-outdoor interactions crucial for built environment management, it would be important that AR apps can work seamlessly. Alignment in indoor environments cannot make use of methods such as GNSS, nor can all environments be assumed to have been previously initialized with AR tools. Thus, marker-less AR registration is crucial for indoor applications. This paper presents an approach for marker-less AR registration seamlessly in both outdoor and indoor environments. Real-time kinematic positioning (RTK) and Inertial Measurement Units (IMU) technologies have been chosen for outdoor registration, while image comparison based on convolutional neural networks (CNN) for indoor registration. In this research, the application of these two technologies and their integration have been studied and tested on site on a real Facility Management use case related to a university campus. The proposed approach has shown very promising results in displaying BIM elements of the electrical system seamlessly superimposed through AR to their physical counterparts in mixed indoor-outdoor environments.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/325396

ChoEn: A Smart Contract Based Choreography Enforcer
2023 IEEE International Conference on Pervasive Computing and Communications Workshops and other Affiliated Events, PerCom Workshops
Autore/i: Spegni, Francesco; Fratini, Lorenzo; Pirani, Massimiliano; Spalazzi, Luca
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Abstract: This work deals with the automatic generation of smart contracts to enforce compliance to a given BPMN choreography of requests sent by a set of independent actors. The choice of smart contracts is justified by the desire not to centralize the enforcement process when there are multiple independent actors characterized by low mutual trust. The choice of BPMN choreographies as an alternative to BPMN processes and collaborations is instead justified by the desire to leave the actors free to dynamically organize their internal processes in the way they prefer, provided that the interactions with the other actors respect some agreed protocol. This work proposes a formal framework to interpret choreographies and translate them onto smart contract enforcers. The framework has been implemented on a free open-source tool named ChoEn and tested by means of a running example
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/321231

A Precision Cybersecurity Workflow for Cyber-physical Systems: The IoT Healthcare Use Case
Computer Security. ESORICS 2022 International Workshops
Autore/i: Spegni, F.; Sabatelli, A.; Merlo, A.; Pepa, L.; Spalazzi, L.; Verderame, L.
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/314968

Natural Language Processing For Construction Sites Management
Proceedings of the 2023 European Conference on Computing in Construction and the 40th International CIB W78 Conference
Autore/i: Corneli, Alessandra; Binni, Leonardo; Spegni, Francesco; Naticchia, Berardo; Messi, Leonardo
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/321034

Enhancing BIM through Mixed Reality for Facility Management
Building Information Modeling - A Sustainable Approach and Emerging Technologies
Autore/i: Vaccarini, Massimo; Carbonari, Alessandro; Spegni, Francesco; Giretti, Alberto
Classificazione: 2 Contributo in Volume
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/307041

Project Information Model resulting from the on-site survey
Autore/i: Spegni, Francesco; Vaccarini, Massimo; Carbonari, Alessandro
Classificazione: 5 Altro
Abstract: The On-site Analysis and Verification Service (ODAVS) is a service developed within the Encore project. It allows users to check any constructability issues regarding renovation projects of residential buildings by means of surveys facilitated by a mixed reality tool. This dataset includes two IFC files of the renovation studies developed by Univpm and JEA (both partners of Encore project) at JEA experimental building in Caceres, and assessed on-site on 2021 December 14th and 15th. The dataset also includes an XML file containing the list of 33 URLS pointing to audio files previously published on a different Zenodo dataset [1]. Note that the access to the Zenodo dataset [1] is restricted. The interested users must ask the dataset authors for permission to access the dataset itself. In the XML file, for each comment, the GUID of the IFC object referred by the audio comment itself is given.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/312710

A Mixed Reality Application for the On-Site Assessment of Building Renovation: Development and Testing
SUSTAINABILITY
Autore/i: Carbonari, Alessandro; Franco, Carlos; Naticchia, Berardo; Spegni, Francesco; Vaccarini, Massimo
Classificazione: 1 Contributo su Rivista
Abstract: This paper contributes to a sustainable construction design management approach to increase the successful renovation rate of existing residential building stock. Indeed, coupling BIM with mixed reality can speed up and improve the quality of the renovation design processes, because it can display virtual models of alternative design scenarios superimposed over the existing physical facility. To this purpose, a sample of technicians was enrolled to test the reliability of this technology. A prototype was developed that enables cooperation among stakeholders and the implementation of an efficient workflow. The volunteers carried out real-life tests in a building demonstrator in Caceres (Spain) and filled in two questionnaires with their feedback. The results showed that an MR-based platform can involve interested stakeholders in the assessment of renovation design projects, that speeds up the decision-making process and increases the quality of those projects. Moreover, technicians can master the technology quickly, provided that it is included in the current renovation workflow and some technology gaps are covered. However, the main limitations of this study are that these findings are valid for building renovation design only, and the tests were performed in a controlled, yet full scale, experimental environment. Finally, this paper deals with a few open technical issues, such as the efficient alignment of holograms, transformation of BIM models into a format suitable for mixed reality applications and sharing feedbacks in an on-line repository to foster collaboration.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/312714

Process-based simulation models using BPMN for construction management at runtime
Proceedings of the 38th International Conference of CIB W78
Autore/i: Messi, Leonardo; Spegni, Francesco; Carbonari, Alessandro; Ridolfi, Luigi; Vaccarini, Massimo
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Abstract: In this paper, we present a platform to develop smart and flexible simulation models, based on the notation known as Business Process Modelling Notation, in support of construction management. They are generated in a way that supports effective re-planning at runtime. They merge information about the product model, construction processes and associated resources. Thanks to the notation used, that information can be properly re-arranged in order to generate the work plan even automatically, e.g. by means of search algorithms. At runtime, the business process models are used to monitor work progress and re-instantiate search algorithms for rapid update of work plans. This notation facilitates construction managers who develop work plans taking into account the usage of resources and of the intrinsic dynamics of construction projects. Finally, the application in the energy retrofit of a residential building is showcased.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/299244

Combining Blockchain and BPMN Choreographies for Construction Management
Proceedings of the 2021 European Conference on Computing in Construction. European Council on Computing in Construction (EC3)
Autore/i: Corneli, Alessandra; Naticchia, Berardo; Spegni, Francesco; Spalazzi, Luca
Editore: University College Dublin
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Abstract: Blockchain is considered a key technology of the current digital revolution and its application is spreading from cryptocurrencies to disparate processes requiring notarization. The well-known independence and contraposition of stakeholders in the AECO sector made DLT applications the hoped-for means to trust each other. Construction site management due to its complexity and the pluralism of the actors involved can be modelled as a BPMN coreography of intra-organizational processes. This aims of the work here presented is the exploitation of blockchains and smart contracts as tools to notarize the state of each intra-organizational process and to enforce compliance with the choreography
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/299867

A Smart Contract-based BPMN Choreography Execution for Management of Construction Processes
Proceedings of the 38th International Symposium on Automation and Robotics in Construction (ISARC)
Autore/i: Corneli, Alessandra; Spegni, Francesco; Bragadin, Marco Alvise; Vaccarini, Massimo
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Abstract: Construction management can be grouped into two different levels: strategic early planning, that provides the baseline for project monitoring, and short time initiatives, based on objectives and self-organization from actors who are involved in on-site processes. The latter can be considered as a complex system management issue since it presents emergent behaviors thus it can not be handled in a traditional way. The passage from project scheduling to on site operations management requires a change of perspective. On site short time planning is a process of forecasting future outcomes therefore it deals with uncertainty and indeterminacy. At present this is managed through the representation of many separate orchestrations and this does not allow to eliminate the inefficiencies that arise at the level of synchronization of the individual tasks performed by organizations with contractually separate management. Efficiency in construction management implies to take into consideration choreographies because they better reflect synchronization of different organizations management processes. On the other hand, information processed as a trigger for distributed activities on different management does not guarantee process traceability while smart contracts linked to single task execution assure both promptness and irreversible tracking at single task level. The actual execution of the processes depends both on what happens and on the information that flows between the subjects who actually carry out processes asynchronous to each other, so the only possibility to synchronize them is information. This research aims to describe a framework for applying BPMN choreographies to construction site processes in order to better modeling processes for smart contracts application. The choice of applying BPMN instead of CPM lays in the fact that it allows to model the information flows as well as the preparatory aspects and in addition it allows to represent decision-making moments. Every single activity in the baseline can be modelled as a choreography at a lower level. On the other hand, process performance monitoring can be performed thanks to blockchain tasks notarization. Concrete casting quality assessment process has been chosen as use case. BPMN choreography of this process has been modelled and blockchain application for tasks and information notarization has been development and tested on a construction site.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/299248

Blockchain based choreographies: The construction industry case study
CONCURRENCY AND COMPUTATION
Autore/i: Spalazzi, L.; Spegni, F.; Corneli, A.; Naticchia, B.
Classificazione: 1 Contributo su Rivista
Abstract: BPMN choreography is a modeling language capable to describe scenarios where several independent participants have to collaborate in a climate of opposing interests and therefore are forced to trust each other. For this reason, in many contexts, a strong need for transparency, responsibility, and choreography compliance arise by the various participants. Blockchains and smart contracts, thanks to their characteristic of providing a decentralized and consensus-based validation mechanism, seem to be able to meet these needs in an untrusted scenario. Nevertheless, most of the related work focused either on transparency, accountability, or compliance, but none on all three of them. Furthermore, such works do not take into account the nondeterministc nature of choreographies. This work aims at using blockchains and smart contracts in this scenario providing a formally well-defined set of tools to match all three the aforementioned requirements. This work applies the proposed techniques to a case study from the construction industry, an economical relevant application domain where the demand for transparency, accountability, and compliance with procurement contracts (that can be modeled as choreographies) is very strong.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/299829

Automatic Repair of Timestamp Comparisons
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING
Autore/i: Liva, Giovanni; Khan, Muhammad Taimoor; Pinzger, Martin; Spegni, Francesco; Spalazzi, Luca
Classificazione: 1 Contributo su Rivista
Abstract: Automated program repair has the potential to reduce the developers' effort to fix errors in their code. In particular, modern programming languages, such as Java, C, and C#, represent time as integer variables that suffer from integer overflow, introducing subtle errors that are hard to discover and repair. Recent researches on automated program repair rely on test cases to discover failures to correct, making them suitable only for regression errors. We propose a new strategy to automatically repair programs that suffer from timestamp overflows that are manifested in comparison expressions. It unifies the benefits of static analysis and automatic program repair avoiding dependency on testing to identify and correct defected code. Our approach performs an abstract analysis over the time domain of a program using a Time Type System to identify the problematic comparison expressions. The repairing strategy rewrites the timestamp comparisons exploiting the binary representation of machine numbers to correct the code. We have validated the applicability of our approach with 20 open source Java projects. The results show that it is able to correctly repair all 246 identified errors. To further validate the reliability of our approach, we have proved the soundness of both, type system and repairing strategy. Furthermore, several patches for three open source projects have been acknowledged and accepted by their developers.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/275521

Parameterized model checking of networks of timed automata with Boolean guards
THEORETICAL COMPUTER SCIENCE
Autore/i: Spalazzi, L.; Spegni, F.
Classificazione: 1 Contributo su Rivista
Abstract: Parameterized model checking is a formal verification technique for verifying that some specifications hold in systems consisting of many similar cooperating but indistinguishable processes. The problem is known to be undecidable in general, even when restricted to reachability properties. To overcome this limitation, several techniques have been explored to address specific system families, logical formulas or topologies of process networks. Some use the notion of cutoff, i.e. if a certain property is verified for systems up to a certain size (the cutoff) then it is verified for systems of any size. Here we analyze the case of networks consisting of an arbitrary number of timed automata that can synchronize by looking at which state the neighbors are currently. We show that cutoffs exist independently from the checked formula, with or without a distinguished process acting as controller. We show how, exploiting the cutoffs, we can obtain upper bounds on complexity of the parameterized model-checking problem. Finally, we show how to use the theoretical results in order to model and verify a distributed algorithm for clock synchronization based on gossip techniques.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/275520

Verifying temporal specifications of Java programs
SOFTWARE QUALITY JOURNAL
Autore/i: Spegni, F.; Spalazzi, L.; Liva, G.; Pinzger, M.; Bollin, A.
Classificazione: 1 Contributo su Rivista
Abstract: Many Java programs encode temporal behaviors in their source code, typically mixing three features provided by the Java language: (1) pausing the execution for a limited amount of time, (2) waiting for an event that has to occur before a deadline expires, and (3) comparing timestamps. In this work, we show how to exploit modern SMT solvers together with static analysis in order to produce a network of timed automata approximating the temporal behavior of a set of Java threads. We also prove that the presented abstraction preserves the truth of MTL and ATCTL formulae, two well-known logics for expressing timed specifications. As far as we know, this is the first feasible approach enabling the user to automatically model check timed specifications of Java software directly from the source code.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/282888

Verification-as-a-Service for Parameter Assessment
2019 International Conference on High Performance Computing and Simulation, HPCS 2019
Autore/i: Spalazzi, L.; Spegni, F.
Editore: Institute of Electrical and Electronics Engineers Inc.
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Abstract: When a professional or researcher faces the task of analyzing some real-world IT system, being it a security protocol, a piece of software, or something else, it comes the moment when the system parameters are enumerated and for each of them he/she has to define its possible values.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/290378

High-Performance Computing for Formal Security Assessment
2019 International Conference on High Performance Computing and Simulation, HPCS 2019
Autore/i: Spalazzi, L.; Spegni, F.
Editore: Institute of Electrical and Electronics Engineers Inc.
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Abstract: Assessing the degree of security of a given system w.r.t. some attacker model and security policy can be done by means of formal methods. For instance, the system can be described as a Markov Decision Process, the security policy by means of a modal logic formula, PCTL∗, and then a probabilistic model checker can return the probability with which the policy holds in the system. This methodology suffices when all the system parameters and their values are known a priori. On the other side, in case the degree of security of the system depends on the values of the system parameters, the formally security assessment task must output a probability function which takes the system parameters and returns the probability of a successful attack to the security of the system. One simple way to describe such function involves solving many instances of the probabilistic model checking problem, one for each combination of the parameter values. In this scenario, probabilistic model checking, which suffers from the state explosion problem, may become an unfeasible task for traditional workstations or even servers.In this work we introduce the tool SecMC which drives the user in the task of modeling the system under analysis and the required security policies, together with the parameters that affect them. Next, the user can specify the range of values assumed by the parameters, and the tool can take care of iterating the probabilistic model checking task, distributing the computations among different local or remote nodes of a cluster, and collect the results to produce a combined picture of how the level of security varies w.r.t. the parameter values.In this paper we show how the tool can be used in order to formally assess security of probabilistic systems known from the literature, viz. a probabilistic cryptographic protocol, a synchronization algorithm for wireless devices inspired by fireflies in nature, and the privacy of dispersed cloud storages.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/290379

Modeling Time in Java Programs for Automatic Error Detection
Proceedings - 2018 ACM/IEEE Conference on Formal Methods in Software Engineering, FormaliSE 2018
Autore/i: Liva, Giovanni; Khan, Muhammad Taimoor; Spalazzi, Luca; Spegni, Francesco; Bollin, Andreas; Pinzger, Martin
Editore: Institute of Electrical and Electronics Engineers Inc.
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Abstract: Modern programming languages, such as Java, represent time as integer variables, called timestamps. Timestamps allow developers to tacitly model incorrect time values resulting in a program failure because any negative value or every positive value is not necessarily a valid time representation. Current approaches to automatically detect errors in programs, such as Randoop and FindBugs, cannot detect such errors because they treat timestamps as normal integer variables and test them with random values verifying if the program throws an exception. In this paper, we present an approach that considers the time semantics of the Java language to systematically detect time related errors in Java programs. With the formal time semantics, our approach determines which integer variables handle time and which statements use or alter their values. Based on this information, it translates these statements into an SMT model that is passed to an SMT solver. The solver formally verifies the correctness of the model and reports the violations of time properties in that program. For the evaluation, we have implemented our approach in a prototype tool and applied it to the source code of 20 Java open source projects. The results show that our approach is scalable and it is capable of detecting time errors precisely enough allowing its usability in real-world applications.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/265851

Towards model checking security of real time Java software
Proceedings - 2018 International Conference on High Performance Computing and Simulation, HPCS 2018
Autore/i: Spalazzi, Luca; Spegni, Francesco; Liva, Giovanni; Pinzger, Martin
Editore: Institute of Electrical and Electronics Engineers Inc.
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Abstract: More and more software libraries and applications in high-performance computing and distributed systems are coded using the Java programming language. The correctness of such pieces of code w.r.t. a given set of security policies often depends on the correct handling of timing between concurrent or recurrent events. Model-checking has proven to be an effective tool for verifying the correctness of software. In spite of the growing importance of this application area of formal methods, though, no approach exists that targets the problem of verifying the correctness of real-Time software w.r.t.Timed specifications. The few existing works focus on very different problems, such as schedulability analysis of Java tasks. In this paper we present an approach combining rule-based static analysis together with symbolic execution of Java code to extract networks of timed automata from existing software and then use Uppaal to model-check them against timed specifications. We show through a real-world case study that this approach can be helpful in model-checking security policies of real-Time Java software.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/265853

Security in heterogeneous distributed storage systems: a practically achievable information-theoretic approach
Proc. ISCC 2017
Autore/i: Baldi, Marco; Chiaraluce, Franco; Senigagliesi, Linda; Spalazzi, Luca; Spegni, Francesco
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Abstract: Distributed storage systems and caching systems are becoming widespread, and this motivates the increasing interest on assessing their achievable performance in terms of reliability for legitimate users and security against malicious users. While the assessment of reliability takes benefit of the availability of well established metrics and tools, assessing security is more challenging. The classical cryptographic approach aims at estimating the computational effort for an attacker to break the system, and ensuring that it is far above any feasible amount. This has the limitation of depending on attack algorithms and advances in computing power. The information-theoretic approach instead exploits capacity measures to achieve unconditional security against attackers, but often does not provide practical recipes to reach such a condition. We propose a mixed cryptographic/information theoretic approach with a twofold goal: estimating the levels of information-theoretic security and defining a practical scheme able to achieve them. In order to find optimal choices of the parameters of the proposed scheme, we exploit an effective probabilistic model checker, which allows us to overcome several limitations of more conventional methods.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/250053

A probabilistic small model theorem to assess confidentiality of dispersed cloud storage (extended abstract)
Proc. ICTCS 2017 and CILC 2017
Autore/i: Baldi, Marco; Bartocci, Ezio; Chiaraluce, Franco; Cucchiarelli, Alessandro; Senigagliesi, Linda; Spalazzi, Luca; Spegni, Francesco
Editore: CEUR-WS
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Abstract: Recent developments in cloud architectures and security concerns have originated new models of online storage clouds based on data dispersal algorithms. According to these lgorithms the data is divided into several slices that are distributed among remote and independent storage nodes. Ensuring confidentiality in this context is crucial: only legitimate users should access any part of information they distribute among storage nodes. We use parameterized Markov Decision Processes to model such a class of systems and Probabilistic Model Checking to assess the likelihood of breaking the confidentiality.We showed that a Small Model Theorem can be proven for a specific types of models, preserving PCTL formulae. Finally, we report the result of applying our methodology to feasibly assess the security of existing dispersed cloud storage solutions.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/252391

Accuracy of message counting abstraction in fault-tolerant distributed algorithms
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Autore/i: Konnov, Igor; Widder, Josef; Spegni, Francesco; Spalazzi, Luca
Editore: Springer Verlag
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/247855

Disjunctive timed networks
CEUR Workshop Proceedings
Autore/i: Spalazzi, Luca; Spegni, Francesco
Editore: CEUR-WS
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/255501

A probabilistic small model theorem to assess confidentiality of dispersed cloud storage
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) - 14th International Conference on Quantitative Evaluation of Systems, QEST 2017
Autore/i: Baldi, Marco; Bartocci, Ezio; Chiaraluce, Franco; Cucchiarelli, Alessandro; Senigagliesi, Linda; Spalazzi, Luca; Spegni, Francesco
Editore: Springer Verlag
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Abstract: Recent developments in cloud architectures have originated new models of online storage clouds based on data dispersal algorithms. According to these algorithms the data is divided into several slices that are distributed among remote and independent storage nodes. Ensuring confidentiality in this context is crucial: only legitimate users should access any part of information they distribute among storage nodes. To the best of our knowledge, the security analysis and assessment of existing solutions always assumes of homogeneous networks and honestbut-curious nodes as attacker model.We analyze more complex scenarios with heterogeneous network topologies and a passive attacker eavesdropping the channel between user and storage nodes. We use parameterized Markov Decision Processes to model such a class of systems and Probabilistic Model Checking to assess the likelihood of breaking the confidentiality. Even if, generally speaking, the parameterized model checking is undecidable, in this paper, however, we proved a Small Model Theorem that makes such a problem decidable for the class of models adopted in this work. We discovered that confidentiality is highly affected by parameters such as the number of slices and the number of write and read requests. At design-time, the presented methodology helps to determine the optimal values of parameters affecting the likelihood of a successful attack to confidentiality.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/250578

Parametric and probabilistic model checking of confidentiality in data dispersal algorithms
2016 International Conference on High Performance Computing and Simulation, HPCS 2016
Autore/i: Baldi, Marco; Cucchiarelli, Alessandro; Senigagliesi, Linda; Spalazzi, Luca; Spegni, Francesco
Editore: Institute of Electrical and Electronics Engineers Inc.
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Abstract: Recent developments in cloud storage architectures have originated new models of online storage as cooperative storage systems and interconnected clouds. Such distributed environments involve many organizations, thus ensuring confidentiality becomes crucial: only legitimate clients should recover the information they distribute among storage nodes. In this work we present a unified framework for verifying confidentiality of dispersal algorithms against probabilistic models of intruders. Two models of intruders are given, corresponding to different types of attackers: one aiming at intercepting as many slices of information as possible, and the other aiming at attacking the storage providers in the network. Both try to recover the original information, given the intercepted slices. By using probabilistic model checking, we can measure the degree of confidentiality of the system exploring exhaustively all possible behaviors. Our experiments suggest that dispersal algorithms ensure a high degree of confidentiality against the slice intruder, no matter the number of storage providers in the system. On the contrary, they show a low level of confidentiality against the provider intruder in networks with few storage providers (e.g. interconnected cloud storage solutions).
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/239606

Parameterized model-checking of timed systems with conjunctive guards
Verified Software: Theories, Tools and Experiments
Autore/i: Spalazzi, Luca; Spegni, Francesco
Editore: Springer Verlag
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/225667

Model Checking Grid Security
FUTURE GENERATION COMPUTER SYSTEMS
Autore/i: Pagliarecci, Francesco; Spegni, Francesco; Spalazzi, Luca
Classificazione: 1 Contributo su Rivista
Abstract: Grid computing is one of the leading forms of high performance computing. Security in the grid environment is a challenging issue that can be characterized as a complex system involving many subtleties that may lead designers into error. This is similar to what happens with security protocols where automatic verification techniques (specially model checking) have been proved to be very useful at design time. This paper proposes a formal verification methodology based on model checking that can be applied to host security verification for grid systems. The proposed methodology must take into account that a grid system can be described as a parameterized model, and security requirements can be described as hyperproperties. Unfortunately, both parameterized model checking and hyperproperty verification are, in general, undecidable. However, it has been proved that this problem becomes decidable when jobs have some regularities in their organization. Therefore, this paper presents a verification methodology that reduces a given grid system model to a model to which it is possible to apply a ‘‘cutoff’’ theorem (i.e., a requirement is satisfied by a system with an arbitrary number of jobs if and only if it is satisfied by a system with a finite number of jobs up to a cutoff size). This methodology is supported by a set of theorems, whose proofs are presented in this paper. The methodology is explained by means of a case study: the Condor system.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/87601

Formal methods for practical reverse engineering and software verification
Autore/i: Spegni, Francesco
Editore: Università Politecnica delle Marche
Classificazione: 8 Tesi di dottorato
Abstract: Software development processes are committed at producing high quality software system. Traditionally, this goal is reached through systematic testing. This thesis project analyzes the possibility of applying mathematical logic and so-called formal methods into the software development process. In fact software testing has two major limitations with respect to verification by means of software testing: every test can show correctness for one possible behavior, while formal methods verification shows that correctness, if proved, holds for all the executions of the system. Furthermore, testing can be used to stress the system implementation, while formal verification can be done also during earlier stages of software development, when abstract models of the system are first sketched. In this work we present an integrated working environment that aims at guiding the software engineer along some of the most relevant moments of a software system lifetime: its development, its verification, its maintenance up to a complete re-structuring. The core of the proposed environment is the language XAL , a parametric extension of the theory of networks of timed automata. After defining its syntax and semantics, we show a novel cutoff theorem for it, proving that systems that are both parametric and timed can be model checked. We then describe two methodologies: the former helps in restructuring existing applications using XAL , extracting parameterized finite-state models from legacy code. The latter is about conducting a formal verification using XAL and its cutoff theorem, if needed. A few case-studies are described that uses the proposed language and methodologies. These case-studies are real-world software systems analyzed in a joint effort with Computer VAR ITT and BINT, two Italian ITC companies.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/242049

A modular environment for software development and re-engineering
2012 Second International Workshop on Developing Tools as Plug-Ins (TOPI)
Autore/i: Salvatore, Campana; Andrea, Poli; Spalazzi, Luca; Spegni, Francesco
Editore: IEEE COMPUTER SOCIETY
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Abstract: Traditional software development processes are designed to deal with the construction of new software systems. We believe the software development methodologies should include from the beginning the possibility of a re-engineering phase. With our work we identify the main characteristics that make software (re)engineering tools useful and usable Developing them in a modular architecture allows for a better integration with the developer’s working habits.
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/87612

Dynamic Networks of Timed Automata for Collaborative Systems: a Network Monitoring Case Study
Proc. of the 2010 International Symposium on Collaborative Technologies and Systems (CTS 2010)
Autore/i: S., Campana; Spalazzi, Luca; Spegni, F.
Editore: IEEE Computer Society Press
Luogo di pubblicazione: LOS ALAMITOS CA
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/48774

XAL: A Web Oriented Programming Language Based On Timed-Automata
Proc. of the 2008 IEEE/WIC/ACM International Conference on Web Intelligence (WI’08)
Autore/i: S., Campana; Spalazzi, Luca; F., Spegni
Editore: IEEE Computer Society Press
Luogo di pubblicazione: LOS ALAMITOS, CA
Classificazione: 4 Contributo in Atti di Convegno (Proceeding)
Scheda della pubblicazione: https://iris.univpm.it/handle/11566/48521