215 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 Journal article Open Access OPEN

Enhancing sustainability of the railway infrastructure: Trading energy saving and unavailability through efficient switch heating policies
Chiaradonna S., Masetti G., Di Giandomenico F., Righetti F., Vallati C.
Railway is currently envisioned as the most promising transportation system for both people and freight to reduce atmospheric emission and combat climate change. In this context, ensuring the energy efficiency of the railway systems is paramount in order to sustain their future expandability with minimum carbon footprint. Recent advancements in computing and communication technologies are expected to play a significant role to enable novel integrated control and management strategies in which heterogeneous data is exploited to noticeably increase energy efficiency. In this paper we focus on exploiting the convergence of heterogeneous information to improve energy efficiency of railway systems, in particular on the heating system for the railroad switches, one of the major energy intensive components. To this aim, we define new policies to efficiently manage the heating of these switches exploiting also external information such as weather and forecast data. In order to assess the performance of each strategy, a stochastic model representing the structure and operation of the railroad switch heating system and environmental conditions (both weather profiles and specific failure events) has been developed and exercised in a variety of representative scenarios. The obtained results allow to understand both strengths and limitations of each energy management policy, and serves as a useful support to make the choice of the best technique to employ to save on energy consumption, given the system conditions at hand.Source: Sustainable computing: informatics and systems (Print) 30 (2021). doi:10.1016/j.suscom.2021.100519
DOI: 10.1016/j.suscom.2021.100519

See at: ISTI Repository Open Access | Sustainable Computing Informatics and Systems Restricted | Sustainable Computing Informatics and Systems Restricted | Sustainable Computing Informatics and Systems Restricted | CNR ExploRA Restricted | Sustainable Computing Informatics and Systems Restricted | www.sciencedirect.com Restricted


2021 Journal article Open Access OPEN

On identity-aware replication in stochastic modeling for simulation-based dependability analysis of large interconnected systems
Chiaradonna S., Di Giandomenico F., Masetti G.
This paper focuses on the generation of stochastic models for dependability and performability analysis, through mechanisms for the automatic replication of template models when identity of replicas cannot be anonymous. The major objective of this work is to support the modeler in selecting the most appropriate replication mechanism, given the characteristics of the system under analysis. To this purpose, three most used solutions to identity-aware replication are considered and a formal framework to allow representing them in a consistent way is first defined. Then, a comparison of their behavior is extensively carried out, with focus on efficiency, both from a theoretical perspective and from a quantitative viewpoint. For the latter, a specific implementation of the considered replication mechanisms in the Möbius modeling environment and a case study representative of realistic interconnected infrastructures are developed.Source: Performance evaluation 147 (2021). doi:10.1016/j.peva.2021.102192
DOI: 10.1016/j.peva.2021.102192

See at: ISTI Repository Open Access | Performance Evaluation Restricted | Performance Evaluation Restricted | Performance Evaluation Restricted | CNR ExploRA Restricted | Performance Evaluation Restricted | www.sciencedirect.com Restricted


2021 Conference article Open Access OPEN

Supervisory synthesis of configurable behavioural contracts with modalities
Basile D., Ter Beek M. H., Degano P., Legay A., Ferrari G. L., Gnesi S., Di Giandomenico F.
Service contracts characterise the desired behavioural compliance of a composition of services, typically defined by the fulfilment of all service requests through service offers. Contract automata are a formalism for specifying behavioural service contracts. Based on the notion of synthesis of the most permissive controller from Supervisory Control Theory, a safe orchestration of contract automata can be computed that refines a composition into a compliant one. This short paper summarises the contributions published in [8], where we endow contract automata with two orthogonal layers of variability: (i) at the structural level, constraints over service requests and offers define different configurations of a contract automaton, depending on which requests and offers are selected or discarded; and (ii) at the behavioural level, service requests of different levels of criticality can be declared, which induces the novel notion of semi-controllability. The synthesis of orchestrations is thus extended to respect both the structural and the behavioural variability constraints. Finally, we show how to efficiently compute the orchestration of all configurations from only a subset of these configurations. A recently redesigned and refactored tool supports the developed theory.Source: FORTE 2021 - 41st IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, pp. 177–181, Online conference, 14-18/06/2021
DOI: 10.1007/978-3-030-78089-0_10

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


2020 Conference article Open Access OPEN

30 years of simulation-based quantitative analysis tools: a comparison experiment between Möbius and Uppaal SMC
Basile D., Ter Beek M. H., Di Giandomenico F., Fantechi A., Gnesi S., Spagnolo G. O.
We provide a brief comparison of the modelling and analysis capabilities of two different formalisms and their associated simulation-based tools, acquired from experimenting with these methods and tools on one specific case study. The case study is a cyber-physical system from an industrial railway project, namely a railroad switch heater, and the quantitative properties concern energy consumption and reliability. We modelled and analysed the case study with stochastic activity networks and Möbius on the one hand and with stochastic hybrid automata and Uppaal SMC on the other hand. We give an overview of the performed experiments and highlight specific features of the two methodologies. This yields some pointers for future research and improvements.Source: ISoLA 2020 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, pp. 368–384, Rhodes, Greece, 20-30/10/2020
DOI: 10.1007/978-3-030-61362-4_21

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


2020 Conference article Open Access OPEN

Analyzing Forward Robustness of Feedforward Deep Neural Networks with LeakyReLU Activation Function Through Symbolic Propagation
Masetti G., Di Giandomenico F.
FeedForward Deep Neural Networks (DNNs) robustness is a relevant property to study, since it allows to establish whether the classification performed by DNNs is vulnerable to small perturbations in the provided input, and several verification approaches have been developed to assess such robustness degree. Recently, an approach has been introduced to evaluate forward robustness, based on symbolic computations and designed for the ReLU activation function. In this paper, a generalization of such a symbolic approach for the widely adopted LeakyReLU activation function is developed. A preliminary numerical campaign, briefly discussed in the paper, shows interesting results.Source: Joint European Conference on Machine Learning and Knowledge Discovery in Databases, pp. 460–474, 14/09/2020
DOI: 10.1007/978-3-030-65965-3_31

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


2020 Conference article Open Access OPEN

Trading dependability and energy consumption in critical infrastructures: Focus on the rail switch heating system
Chiaradonna S., Di Giandomenico F., Masetti G.
Traditionally, critical infrastructures demand for high dependability, being the services they provide essential to human beings and the society at large. However, more recent attention to cautious usage of energy resources is changing this vision and calls for solutions accounting for appropriate multi-requirements combinations when developing a critical infrastructure. In such a context, analysis supports able to assist the designer in envisioning a satisfactory trade-off among the multi-requirements for the system at hand are highly helpful. In this paper, the focus is on the railway sector and the contribution is a stochastic model-based analysis framework to quantitatively assess trade-offs between dependability indicators and electrical energy consumption incurred by the rail switch heating system.Moving from a preliminary study that concentrated on energy consumption only, the analysis framework has been extended to become a solid support to devise appropriate tuning of the heating policy that guarantees satisfactory trade-offs between dependability and energy consumption. An evaluation campaign in a variety of climate scenarios demonstrates the feasibility and utility of the developed framework.Source: 25th IEEE Pacific Rim International Symposium on Dependable Computing, pp. 150–159, Perth, Australia, 01/12/2021
DOI: 10.1109/prdc50213.2020.00026

See at: ISTI Repository Open Access | academic.microsoft.com Restricted | dblp.uni-trier.de Restricted | doi.org Restricted | ieeexplore.ieee.org Restricted | ieeexplore.ieee.org Restricted | CNR ExploRA Restricted | xplorestaging.ieee.org Restricted


2020 Contribution to conference Open Access OPEN

Enhancing sustainability of the railway infrastructure through efficient energy management policies
Chiaradonna S., Masetti G., Di Giandomenico F., Righetti F., Vallati C.
Railway is currently envisioned as the most promising transportation system for both people and freight to reduce atmospheric emission and combat climate change. In this context, ensuring the energy efficiency of the railway systems is paramount in order to sustain their future expandability with minimum carbon footprint. Recent advancements in computing and communication technologies are expected to play a significant role to enable novel integrated control and management strategies in which heterogeneous data is exploited to noticeably increase energy efficiency. In this paper we focus on exploiting the convergence of heterogeneous information to improve energy efficiency of railway systems, in particular on the heating system for the railroad switches, one of the major energy intensive components. To this aim, we define new policies to efficiently manage the heating of these switches exploiting also external information such as weather and forecast data. In order to assess the performance of each strategy, a stochastic model representing the structure and operation of the railroad switch heating system and environmental conditions (both weather profiles and specific failure events) has been developed and exercised in a variety of representative scenarios. The obtained results allow to understand both strengths and limitations of each energy management policy, and serves as a useful support to make the choice of the best technique to employ to save on energy consumption, given the system conditions at hand.Source: 11th International Green and Sustainable Computing Conference, Virtual Conference, 19/10/2020, 22/10/2020

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


2020 Conference article Open Access OPEN

Failure management strategies for IoT-based railways systems
Righetti F., Vallati C., Anastasi G., Masetti G., Di Giandomenico F.
Railways monitoring and control are currently performed by different heterogeneous vertical systems working in isolation without or with limited cooperation among them. Such configuration, widely adopted in practical deployments today, is in contrast with the integrated vision of systems that are at the foundation of the smart-city concept. In order to overcome the current fractured ecosystem that monitors and controls railways functionalities, the adoption of a novel integrated approach is mandatory to create an all-in-one railway system. To this aim, new IoT-based communication technologies, like wireless or Power Line Communication technologies, are considered the main enablers to integrate in a very rapid and easy manner existing vertical systems. In this work, we analyse the architecture of future railways systems based on a mix of wireless and Power Line Communication technologies. In our analysis, we aim at studying possible failure management strategies on rail-road switches to improve the level of reliability, crucial requirement for systems that demand maximum resiliency as they manage a critical function of the infrastructure. In particular, we propose a set of solutions aimed at detecting and handling network and sensor failures to ensure continuity in the execution of the basic control functions. The proposed approach is evaluated by means of simulations and demonstrated to be effective in ensuring a good level of performance even when failures occur.Source: 2020 IEEE International Conference on Smart Computing, pp. 386–391, Bologna, 14-17/09/2020
DOI: 10.1109/smartcomp50058.2020.00082

See at: ISTI Repository Open Access | academic.microsoft.com Restricted | dblp.uni-trier.de Restricted | ieeexplore.ieee.org Restricted | CNR ExploRA Restricted | xplorestaging.ieee.org Restricted


2019 Report Restricted

Progetto SIGS - Architettura del Sistema (D3.1)
Baronti P., Barsocchi P., Ferro E., Furfari F., Di Giandomenico F., La Rosa D., Mavilia F., Miori V., Potortì F., Ancillotti E., Bolettieri S., Borgia E., Bruno R., Piscione P., Valerio L.
In questo documento presentiamo i risultati dell'Attività 3.1: "Definizione dell'architettura del sistema ICT per la gestione del sistema edificio". In particolare, viene definita l'architettura generale della piattaforma ICT per la raccolta e gestione dei dati da dispositivi IoT. Inoltre, sono presentate le tecnologie principali che costituiscono la piattaforma ICT, sia in termini di protocolli di comunicazione che di piattaforma software per la gestione ed erogazione di servizi ad applicazioni distribuite. Infine, vengono presentati i modelli di interazione fra le varie componenti che costituiscono la piattaforma ICT e gli attori del sistema.Source: Project report, SIGS, Deliverable D3.1, 2019

See at: CNR ExploRA Restricted


2019 Report Restricted

Progetto SIGS - Sistema di raccolta ed elaborazioni dati (D3.2)
Baronti P., Barsocchi P., Ferro E., Furfari F., Di Giandomenico F., La Rosa D., Mavilia F., Miori V., Potortì F., Ancillotti E., Bolettieri S., Borgia E., Bruno R., Piscione P., Valerio L.
In questo documento presentiamo i risultati dell'Attività 3.2: "Sviluppo della sensoristica per il monitoraggio dei consumi energetici" e dell'Attività 3.3: "Sviluppo del middleware di comunicazione e di gestione di grossi volumi da sensori eterogenei ". In particolare, vengono presentati i vari standard di comunicazione radio per dispositivi IoT che sono stati integrati nella nostra piattaforma, e per ogni tecnologia vengono descritti i sensori ed attuatori che sono integrati nella piattaforma. Inoltre, viene descritta l'architettura software dei componenti che permettono di integrare le diverse tecnologie di comunicazione IoT (ZigBee, ZWave e 6LoWPAN) con il Middleware di comunicazione e gestione dei dati di tipo publish/subscribe che è stato adottato come riferimento per la piattaforma ICT di raccolta e gestione dei dati. Infine, viene descritta l'architettura software della dashboard, cioè una applicazione web il cui scopo principale è la visualizzazione e manipolazione, attraverso un'interfaccia web, delle serie temporali e dei metadati dei dispositivi (sensori e attuatori) di una rete di sensori.Source: Project report, SIGS, Deliverable D3.2, 2019

See at: CNR ExploRA Restricted


2019 Journal article Open Access OPEN

Controller synthesis of service contracts with variability
Basile D., Ter Beek M. H., Degano P., Legay A., Ferrari G. L., Gnesi S., Di Giandomenico F.
Service contracts characterise the desired behavioural compliance of a composition of services. Compliance is typically defined by the fulfilment of all service requests through service offers, as dictated by a given Service-Level Agreement (SLA). Contract automata are a recently introduced formalism for specifying and composing service contracts. Based on the notion of synthesis of the most permissive controller from Supervisory Control Theory, a safe orchestration of contract automata can be computed that refines a composition into a compliant one. To model more fine-grained SLA and more adaptive service orchestrations, in this paper we endow contract automata with two orthogonal layers of variability: (i) at the structural level, constraints over service requests and offers define different configurations of a contract automaton, depending on which requests and offers are selected or discarded, and (ii) at the behavioural level, service requests of different levels of criticality can be declared, which induces the novel notion of semi-controllability. The synthesis of orchestrations is thus extended to respect both the structural and the behavioural variability constraints. Finally, we show how to efficiently compute the orchestration of all configurations from only a subset of these configurations. A prototypical tool supports the developed theory.Source: Science of computer programming (Print) 187 (2019). doi:10.1016/j.scico.2019.102344
DOI: 10.1016/j.scico.2019.102344

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


2019 Journal article Open Access OPEN

On Extending and Comparing Newton-Raphson Variants for Solving Power-Flow Equations
Dutto S., Masetti G., Chiaradonna S., Di Giandomenico F.
This paper focuses on power-flow equations solutions, based on the Newton-Raphson method. Two major contributions are offered. First, the definition of novel solution variants, resorting to Wirtinger calculus, is attempted. The obtained developments, although original in their formulation, led to already known variants. Despite the impaired originality of the obtained solution, there are significant lessons learned from such an effort. The second major contribution consists of a deep comparison analysis of existing solution strategies, based on complex and real variables, and the Wirtinger based ones, all properly reformulated to allow direct comparison with each other. The goal is to investigate strengths and weaknesses of the addressed techniques in terms of computational effort and convergence rate, which are the most relevant aspects to consider while choosing the approach to employ to solve power-flow equations for a specific power system under study.Source: IEEE transactions on power systems 34 (2019): 2577–2587. doi:10.1109/TPWRS.2019.2897640
DOI: 10.1109/tpwrs.2019.2897640

See at: ISTI Repository Open Access | IEEE Transactions on Power Systems Restricted | ieeexplore.ieee.org Restricted | IEEE Transactions on Power Systems Restricted | IEEE Transactions on Power Systems Restricted | IEEE Transactions on Power Systems Restricted | CNR ExploRA Restricted | IEEE Transactions on Power Systems Restricted


2019 Conference article Open Access OPEN

Stochastic modeling and evaluation of large interdependent composed models through Kronecker algebra and exponential sums
Masetti G., Robol L., Chiaradonna S., Di Giandomenico F.
The KAES methodology for efficient evaluation of dependability-related properties is proposed. KAES targets systems representable by Stochastic Petri Nets-based models, composed by a large number of submodels where interconnections are managed through synchronization at action level. The core of KAES is a new numerical solution of the underlying CTMC process, based on powerful mathematical techniques, including Kronecker algebra, Tensor Trains and Exponential Sums. Specifically, advancing on existing literature, KAES addresses efficient evaluation of the Mean-Time-To-Absorption in CTMC with absorbing states, exploiting the basic idea to further pursue the symbolic representation of the elements involved in the evaluation process, so to better cope with the problem of state explosion. As a result, computation efficiency is improved, especially when the submodels are loosely interconnected and have small number of states. An instrumental case study is adopted, to show the feasibility of KAES, in particular from memory consumption point of view.Source: The 40th International Conference on Application and Theory of Petri Nets and Concurrency, pp. 47–66, Berlin, 23-28/06/2019
DOI: 10.1007/978-3-030-21571-2_3

See at: arpi.unipi.it Open Access | Archivio della Ricerca - Università di Pisa 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 Journal article Open Access OPEN

Smart Services for Railways
Di Giandomenico F., Gnesi S, Spagnolo G. O., Fantechi A.
The project STINGRAY (SmarT station INtelliGent RAilwaY) addresses the role of the railway station, traditionally seen as a meeting point for a city, in order to enhance its importance and integration into the smart city of the future.Source: ERCIM news (2019): 34–35.

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


2019 Contribution to conference Open Access OPEN

Software Engineering for Resilient Systems - 11th International Workshop, SERENE 2019
Calinescu R., Di Giandomenico F.
This volume contains the proceedings of the 11th International Workshop on Software Engineering for Resilient Systems (SERENE 2019). SERENE 2019 took place in Naples, Italy, on September 17, 2019. The SERENE workshop is an annual event that brings together leading researchers and practitioners from academia and industry, to advance the state of the art and to identify open challenges in the software engineering of resilient systems.DOI: 10.1007/978-3-030-30856-8

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


2019 Contribution to book Restricted

On quantitative assessment of reliability and energy consumption indicators in railway systems
Basile D., Di Giandomenico F., Gnesi S.
Stochastic model-based approaches are widely used for obtaining quantitative non-functional indicators of the analysed systems, as for example reliability, performance and energy consumption. However, a critical issue with models is their validation, in order to justifiably put reliance on the analysis results they provide. In this paper, we address cross-validation on a case study from the railway domain, by modelling and evaluating it with different formalisms and tools.Stochastic Activity Networks models and Stochastic Hybrid Automata models of rail road switch heaters, developed for the purpose of evaluating energy consumption and reliability indicators, will be evaluated with Mobius and Uppaal SMC. We will compare the obtained results, to improve their trustworthiness and to provide insights on the design and analysis of energy-saving cyber-physical systems.Source: Green IT Engineering: Social, Business and Industrial Applications, edited by Vyacheslav Kharchenko, Yuriy Kondratenko, Janusz Kacprzyk, pp. 423–447, 2019
DOI: 10.1007/978-3-030-00253-4_18

See at: academic.microsoft.com Restricted | link.springer.com Restricted | link.springer.com Restricted | CNR ExploRA Restricted | rd.springer.com Restricted


2019 Contribution to book Open Access OPEN

A Refined Framework for Model-Based Assessment of Energy Consumption in the Railway Sector
Chiaradonna S., Di Giandomenico F., Masetti G., Basile D.
Awareness and efforts to moderate energy consumption, desirable from both economical and environmental perspectives, are nowadays increasingly pursued. However, when critical sectors are addressed, energy saving should be cautiously tackled, so to not impair stringent dependability properties such contexts typically require. This is the case of the railway transportation system, which is the critical infrastructure this paper focuses on. For this system category, the attitude has been typically to neglect efficient usage of energy sources, motivated by avoiding to put dependability in danger. The new directives, both at national and international level, are going to change this way of thinking. Our study intends to be a useful support to careful energy consumption. In particular, a refined stochastic modeling framework is offered, tailored to the railroad switch heating system, through which analyses can be performed to understand the sophisticated dynamics between the system (both the cyber and physical components) and the surrounding weather conditions.Source: From Software Engineering to Formal Methods and Tools, and Back. Essays Dedicated to Stefania Gnesi on the Occasion of Her 65th Birthday, edited by Maurice H. ter Beek, Alessandro Fantechi, Laura Semini, pp. 481–501, 2019
DOI: 10.1007/978-3-030-30985-5_28

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 Conference article Open Access OPEN

Towards Runtime Monitoring for malicious behaviors detection in Smart Ecosystems
Cioroaica E., Di Giandomenico F., Kuhn T., Lonetti F., Marchetti E., Jahic J., Schnicke F.
A Smart Ecosystem reflects in the control decisions of entities of different nature, especially of its software components. Particularly, the malicious behavior requires a more accurate attention. This paper discusses the challenges related to the evaluation of software smart agents and proposes a first solution leveraging the monitoring facilities for a) assuring conformity between the software agent and its digital twin in a real-time evaluation and b) validating decisions of the digital twins during runtime in a predictive simulation.Source: ISSREW 2019 - IEEE International Symposium on Software Reliability Engineering Workshops, pp. 200–203, Berlin, Germany, 27-30 October, 2019
DOI: 10.1109/issrew.2019.00072
Project(s): SECREDAS via OpenAIRE

See at: ISTI Repository Open Access | Fraunhofer-ePrints Open Access | academic.microsoft.com Restricted | dblp.uni-trier.de Restricted | ieeexplore.ieee.org Restricted | CNR ExploRA Restricted | xplorestaging.ieee.org Restricted


2018 Journal article Open Access OPEN

A tour of secure software engineering solutions for connected vehicles
Bertolino A., Calabrò A., Di Giandomenico F., Lami G., Lonetti F., Marchetti E., Martinelli F., Matteucci I., Mori P.
The growing number of vehicles daily moving on roads increases the need of protecting the safety and security of passengers, pedestrians, and vehicles themselves. This need is intensified when considering the pervasive introduction of Information and Communication Technologies (ICT) systems into modern vehicles, because this makes such vehicles potentially vulnerable from the point of view of security. The convergence of safety and security requirements is one of the main outstanding research challenges in software-intensive systems. This work reviews existing methodologies and solutions addressing security issues in the automotive domain with a focus on the integration between safety and security aspects. In particular, we identify the main security issues with vehicular communication technologies and existing gaps between state-of-the-art methodologies and their implementation in the real world. Starting from a literature survey and referring to widely accepted standards of the domain, such as AUTOSAR and ISO 26262, we discuss research challenges and set baselines for a holistic secure-by-design approach targeting safety and security aspects all along the different phases of the development process of automotive software.Source: Software quality journal 26 (2018): 1223–1256. doi:10.1007/s11219-017-9393-3
DOI: 10.1007/s11219-017-9393-3

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


2018 Contribution to book Open Access OPEN

A refinement approach to analyse critical cyber-physical systems
Basile D., Di Giandomenico F., Gnesi S.
Cyber-Physical Systems (CPS) are characterised by digital components controlling physical equipment, and CPS are typically influenced by the surrounding environment conditions. Due to the stochastic continuous nature of the involved physical phenomena, for quantitative evaluation of non-functional properties (e.g. dependability, performance) stochastic hybrid model-based approaches are mainly used. In case of critical applications, it is also important to verify specific qualitative aspects (e.g. safety). Generally, stochastic hybrid approaches are not suitable to account for the co-existence of both qualitative and quantitative aspects. In this paper we address this issue by proposing a refinement approach for analysing stochastic hybrid systems starting from a verified discrete representation of their logic. Different formalisms are used and formally related. It is then possible to combine the quantitative assessment of stochastic continuous properties with the qualitative verification of logic soundness, thus improving the trustworthiness of the analysis results.Source: Software Engineering and Formal Methods, edited by Antonio Cerone, Marco Roveri, pp. 267–283, 2018
DOI: 10.1007/978-3-319-74781-1_19
Project(s): ASTRail via OpenAIRE

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