Pubblicazioni con acknowledgment al progetto SISTER
- M. Gharib, P. Lollini, A. Bondavalli
"A conceptual model for analyzing information quality in System-of-Systems"
12th System of Systems Engineering Conference (SoSE), Waikoloa, HI, 2017, pp. 1-6.
A System-of-Systems (SoS) is an integration of a finite number of Constituent Systems (CSs), which are networked together for achieving a certain higher goal. Therefore, integration is the key viability of any SoS. Although the integration of CSs can be achieved by the exchange of information, no existing work has considered the quality of such information. Without considering Information Quality (IQ), a CS may depend on inaccurate, incomplete, inconsistent, invalid, and/or untrustworthy information, which might lead to its failure, and in turn to catastrophic incidents in the case of critical SoS. The main objective of the paper is proposing a novel conceptual model that provides the required concepts for analyzing for SoS. We illustrate the utility of the model with an example concerning the Intelligent Transportation System (ITS) domain.
- Basile, D., Di Giandomenico, F., Gnesi, S.,
"A Refinement Approach to Analyse Critical Cyber-Physical Systems"
In Software Engineering and Formal Methods – (SEFM) 2017 Collocated Workshops: DataMod, FAACS, MSE, CoSim-CPS, and FOCLASA, (pp. 267-283) Trento, Italy, September 4-5, 2017, Revised Selected Papers
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.
- Basile D., Di Giandomenico F., Gnesi S.
"Dependable Dynamic Routing for Urban Transport Systems Through Integer Linear Programming"
In: Fantechi A., Lecomte T., Romanovsky A. (eds) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. RSSRail 2017. Lecture Notes in Computer Science, vol 10598. Springer, Cham
Highly automated transport systems play an important role in the transformation towards a digital society, and planning the optimal routes for a set of fleet vehicles has been proved useful for improving the delivered services. Traditionally, routes are planned beforehand. However, with the advent of autonomous urban transport systems (e.g. autonomous cars), possible obstructions of tracks due to traffic congestion or bad weather conditions need to be handled on the fly. In this paper we tackle the problem of dynamically computing routes of vehicles in urban lines in the presence of potential obstructions. The problem is formulated as an integer linear optimization problem. The proposed algorithm will assign routes to vehicles dynamically, considering the track segments that are no longer available and the positions of the vehicles in the urban area. The recomputed routes guarantee the minimal waiting time for passengers. Safety of the computed routes is also guaranteed.
- Davide Basile, Maurice H. ter Beek, Felicita Di Giandomenico, and Stefania Gnesi
"Orchestration of Dynamic Service Product Lines with Featured Modal Contract Automata"
In Proceedings of the 21st International Systems and Software Product Line Conference - Volume B (SPLC '17), Maurice ter Beek, Walter Cazzola, Oscar Diaz, Marcello La Rosa, Roberto López-Herrejón, Thomas Thüm, Javier Troya, Antonio Ruiz-Cortés, and David Benavides (Eds.). ACM, New York, NY, USA, 117-122.
In Service-Oriented Computing, contracts provide a way to characterise the behavioural conformance of a composition of services, and to guarantee that the results do not lead to spurious compositions. Adding variability leads to a product line of services capable of adapting to customer requirements and to changes in the context in which they operate. To this aim, we extended a previously introduced formal model of service contracts. In particular, we included: (i) feature-based constraints and (ii) four classes of service requests to characterise different variants of service agreement. We then exploited Supervisory Control Theory to define an algorithm to synthesise an orchestration of services that satisfies: (i) all feature constraints of the service product line, and (ii) the maximal number of service requests for which an agreement can be reached. Moreover, such an orchestration of a service product line, whose number of products is potentially exponential in the number of features, can be synthesised from only a subset of its products. A prototypical tool supports the developed theory. In this short paper, we provide the intuition for our approach and illustrate it by means of a Hotel reservation service product line.
- Davide Basile, Felicita Di Giandomenico, and Stefania Gnesi
"FMCAT: Supporting Dynamic Service-based Product Lines"
In Proceedings of the 21st International Systems and Software Product Line Conference - Volume B (SPLC '17), Maurice ter Beek, Walter Cazzola, Oscar Diaz, Marcello La Rosa, Roberto López-Herrejón, Thomas Thüm, Javier Troya, Antonio Ruiz-Cortés, and David Benavides (Eds.). ACM, New York, NY, USA, 3-8.
We describe FMCAT, a toolkit for Featured Modal Contract Automata (FMCA). FMCAT supports the analysis of dynamic service product lines, i.e., applications consisting of ensembles of interacting services organized as product lines. Services are modelled as FMCA, with features identifying obligations and requirements of services. Service requirements can be either permitted or necessary, whereas the latter are further partitioned according to their criticality. A notion of agreement among service contracts is used to characterise safety.
We show how FMCAT can be used to (i) specify dynamic service product line, (ii) efficiently identify all valid products, and to synthesise a safe orchestration of services for either (iii) a single product, or (iv) the whole service product line. FMCAT exploits the theory of FMCA to efficiently perform the above tasks by only visiting a subset of valid products, and it is equipped with a GUI.
Pubblicazioni dei partner sulle tematiche del progetto SISTER
- A. Bondavalli, A. Ceccarelli, P. Lollini, L. Montecchi and M. Mori
"System-of-Systems to Support Mobile Safety Critical Applications: Open Challenges and Viable Solutions"
in IEEE Systems Journal, vol. 12, no. 1, pp. 250-261, March 2018
A dramatic shift in system complexity is occurring, bringing monolithic system designs to be progressively replaced by modular approaches. In the latest years, this trend has been emphasized by the system of systems (SoS) concept, in which a complex system or application is the result of the integration of many independent, autonomous constituent systems (CS), brought together in order to satisfy a global goal under certain rules of engagement. The overall behavior of the SoS, emerging from such complex interactions and dependencies, poses several threats in terms of dependability, timeliness, and security, due to the challenging operating and environmental conditions caused by mobility, wireless connectivity, and the use of off-the-shelf components. Referring to our experience in mobile safety-critical applications gained from three different research projects, in this paper, we illustrate the challenges and benefits posed by the adoption of an SoS approach in designing, developing, and maintaining mobile safety-critical applications, and we report on some possible solutions.
- D'Arco, M., Renga, A., Ceccarelli, A., Brancati, F., & Bondavalli, A.
"Enhancing workers safety in worksites through augmented GNSS sensors"
Measurement, 117, 144-152, 2018.
Human-assistive wearable technologies can monitor the position of a worker in a critical worksite and improve his safety by raising warnings when he is in a dangerous zone. In railway worksites, it is observed that GNSS localization is not applicable due to the relevant localization errors, which are only partially attributable to the specific characteristics of the worksite. Besides, alternative solutions that rely on the support of anchors have the drawback of lengthening the set-up and dismantle time of the worksite. To provide safe localization of railway trackside workers, a system that exploits augmented-GNSS wearable sensors is proposed. Each sensor includes a GPS receiver capable of sharing its coordinates with the other sensors, and is further complemented with a low-cost multi-way distance meter to measure its distance from the other sensors. The main attention is paid to the data fusion approach adopted to improve the accuracy of the position estimate by combining the relative distance measurements to the GPS coordinates.
- Bondavalli Andrea, Francesco Brancati
"Certifications of Critical Systems -The CECRIS Experience"
River Publishers, 2017
In recent years, a considerable amount of effort has been devoted, both in industry and academia, to the development, validation and verification of critical systems, i.e. those systems whose malfunctions or failures reach a critical level both in terms of risks to human life as well as having a large economic impact. Certifications of Critical Systems - The CECRIS Experience documents the main insights on Cost Effective Verification and Validation processes that were gained during work in the European Research Project CECRIS (Certification of Critical Systems). The objective of the research was to tackle the challenges of certification by focusing on those aspects that turn out to be more difficult/important for current and future critical systems industry: the effective use of methodologies, processes and tools. Starting from both the scientific and industrial state of the art methodologies for system development and the impact of their usage on the verification and validation and certification of critical systems, the project aimed at developing strategies and techniques supported by automatic or semi-automatic tools and methods for these activities, setting guidelines to support engineers during the planning of the verification and validation phases. Topics covered include: Safety Assessment, Reliability Analysis, Critical Systems and Applications, Functional Safety, Dependability Validation, Dependable Software Systems, Embedded Systems, System Certification.
- Vincenzo Di Massa, Mirko Damiani, Maurizio Papini, Gianluca Mandò
"Redundant and Reliable Architecture Based on Open Source Tools for Light-Rail-Transit On-Board-Systems"
In: Fantechi A., Lecomte T., Romanovsky A. (eds) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. RSSRail 2017. Lecture Notes in Computer Science, vol 10598, pp.212-220. Springer, Cham
The LRT (Light Rail Transit) systems are a kind of urban transport that has aspects in common to both tramways and metros. This paper analyses the Thales LRT On-Board-Systems (OBS) architecture, which is designed to achieve a high level of availability. Such architecture is built on top of open source technologies and consolidated telecommunication standards. Architectural requirements are met also thanks to the used Open-Source foundations. In particular the Qt framework, the 0MQ and the ASN.1 to C compiler have been used to develop a micro-service oriented fault resistant system. Redundant services are spawned on replicated identical hardware units, one of which is the master, and are seamlessly and automatically kept in sync by the algorithms described in this paper. In case of a service failure on one of the replicated hardware boxes, a choice is made between two alternatives: (1) a full mastership changeover is performed and another redundant box becomes the new master (2) a micro-service is migrated to another redundant box in order to take control of the same non-faulty device. The described architecture is being actively used in both LRT and metro solutions, thus this work will describe the benefits on the field and the effectiveness of the architecture in terms of code quality and maintainability. Since the development of the mentioned projects has been carried on inside an Agile team, some considerations will be made about benefits, constraints and pitfalls of such kind of methodologies, on strictly regulated and safety related projects.
- Mandò Gianluca, Giambene Giovanni
"LTE System Design for Urban Light Rail Transport"
In: Fantechi A., Lecomte T., Romanovsky A. (eds) Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. RSSRail 2017. Lecture Notes in Computer Science, vol 10598, pp.17-33. Springer, Cham
This paper deals with the performance of LTE-A (Long Term Evolution-Advanced) cellular networks for supporting operational, safety-critical signaling, and standard IT services for urban transportation. Our interests have been focused on Light Rail Transit (LRT) signaling performance for the Songjiang (China) tramway project. Several stationary and mobility use cases have been considered and mean end-to-end delay and Packet Loss Rate (PLR) key performance indicators have been evaluated. Simulation results highlight that, in stationary conditions, LRT signaling performance requirements are fulfilled, while PLR performance degrades when mobility is introduced. Furthermore, we have evaluated the impact of non-critical IT traffic (e.g., UDP-based video) on TCP-based signaling by demonstrating that signaling throughput is not affected by video in stationary scenarios, whereas, in the presence of mobility, handovers degrade signaling performance, which can be guaranteed only if a QoS-aware scheduler is adopted. In conclusions, our results demonstrate that LTE-A can safely support operative and non-critical applications in urban transportation scenarios, where strong connectivity requirements are crucial.
- Marco Mori, Andrea Ceccarelli, Paolo Lollini, Bernhard Frömel, Francesco Brancati, Andrea Bondavalli
"Systems‐of‐systems modeling using a comprehensive viewpoint‐based SysML profile"
Journal of Software: Evolution and Process (2017)
In recent years, more and more efforts have been devoted in supporting the design of systems‐of‐systems (SoS). Designing such systems is a multidisciplinary problem which involves considering emergent phenomena, assuring the achievement of dependability/security requirements, guaranteeing system responsiveness, and supporting dynamicity/evolution and multicriticality of provided services. A first step towards a viable design approach is to provide a conceptual model of SoS which captures SoS concepts, and their interrelationships aiming at enhancing the understandability of SoS to stakeholders and providing the basis for further automated analysis. In this context, the AMADEOS European project is bringing together researchers and practitioners to provide the support to design SoS starting from the definition of a domain specific ontology serving as a vocabulary for SoS. Our contribution consists in the modeling of the key SoS concepts and relationships defined in AMADEOS adopting a systems modeling language visual modeling language. We propose a systems modeling language profile for SoS, and we show its applicability in a Smart Grid scenario. We show how to use the profile in a model‐driven engineering process to support different types of analyses, and we discuss how to integrate the profile in a user‐friendly model‐driven engineering tool for SoS rapid modeling, validation, code‐generation, and simulation.
- A. Vasenev, L. Montoya, A. Ceccarelli
"A Hazus-Based Method for Assessing Robustness of Electricity Supply to Critical Smart Grid Consumers during Flood Events"
2016 11th International Conference on Availability, Reliability and Security (ARES), Salzburg, 2016, pp. 223-228.
Ensuring an external electricity supply to critical city components during flood events requires adequate urban grid planning. The proliferation of smart grid technologies means that such planning needs to assess how smart grids might function during floods. This paper proposes a method to qualitatively investigate robustness of electricity supply to smart grid consumers during flood events. This method builds on the Hazus methodology and aims to provide inputs for the risk analysis of urban grids.