2017
Software
Open Access
AMPL model for the dependable dynamic vehicle routing problem
Basile D
AMPL integer linear programming program for the dependable dynamic vehicle routing problem, referred in the paper published at RSSRail 2017
Basile D
AMPL integer linear programming program for the dependable dynamic vehicle routing problem, referred in the paper published at RSSRail 2017
See at:
github.com 
| CNR IRIS | CNR IRIS 
2017
Other
Open Access
ISTI Young Research Award 2017
Barsocchi P., Basile D., Candela L., Ciancia V., Delle Piane M., Esuli A., Ferrari A., Girardi M., Guidotti R., Lonetti F., Moroni D., Nardini F. M., Rinzivillo S., Vadicamo L.
The ISTI Young Researcher Award is an award for young people of Institute of Information Science and Technologies (ISTI) with high scientific production. In particular, the award is granted to young staff members (less than 35 years old) by assessing the yearly scientific production of the year preceding the award. This report documents procedure and results of the 2017 edition of the award.Source: ISTI Technical reports, 2017
Barsocchi P., Basile D., Candela L., Ciancia V., Delle Piane M., Esuli A., Ferrari A., Girardi M., Guidotti R., Lonetti F., Moroni D., Nardini F. M., Rinzivillo S., Vadicamo L.
The ISTI Young Researcher Award is an award for young people of Institute of Information Science and Technologies (ISTI) with high scientific production. In particular, the award is granted to young staff members (less than 35 years old) by assessing the yearly scientific production of the year preceding the award. This report documents procedure and results of the 2017 edition of the award.Source: ISTI Technical reports, 2017
See at:
ISTI Repository | CNR ExploRA
2017
Conference article
Open Access
Specifying variability in service contracts
Basile D, Di Giandomenico F, Gnesi S, Degano P, Ferrari Gl
In Service Oriented Computing (SOC) contracts characterise the behavioural conformance of a composition of services and guarantee that the composition does not lead to spurious results. Variability features can enable services to adapt to customer requirements and to changes in the context in which they execute. We extend a recently introduced formal model of service contracts to specify variability mechanisms in a composition of services. Necessary and permitted service requests can be defined and triggered to increase adaptability. The compositional rules of the original formalism are enriched to fulfil all necessary requirements and the maximal number of permitted ones.DOI: 10.1145/3023956.3023965
Metrics:
Basile D, Di Giandomenico F, Gnesi S, Degano P, Ferrari Gl
In Service Oriented Computing (SOC) contracts characterise the behavioural conformance of a composition of services and guarantee that the composition does not lead to spurious results. Variability features can enable services to adapt to customer requirements and to changes in the context in which they execute. We extend a recently introduced formal model of service contracts to specify variability mechanisms in a composition of services. Necessary and permitted service requests can be defined and triggered to increase adaptability. The compositional rules of the original formalism are enriched to fulfil all necessary requirements and the maximal number of permitted ones.DOI: 10.1145/3023956.3023965
Metrics:
See at:
dl.acm.org | CNR IRIS | ISTI Repository | doi.org | CNR IRIS | CNR IRIS
2017
Contribution to book
Open Access
Model-based evaluation of energy saving systems
Basile D, Di Giandomenico F, Gnesi S
Nowadays, there is a great attention towards cautious usage of energy sources to be employed in disparate application domains, including critical infrastructures, to save both in financial terms and in environmental impact. This chapter focuses on stochastic model-based as a support to the analysis of energy saving systems, in combination with other non functional properties, such as reliability, safety and availability. We discuss general guidelines to build a model-based framework to analyse critical cyber-physical systems, where effective energy consumption is required, while assuring imposed levels of resilience. Also, an overview of the most commonly employed methodologies and tools for model-based analysis is provided, and extensive literature is indicated as pointers to relevant research activities performed on this attractive topic over the last decades. Finally, in order to corroborate the proposed framework, a case study in the railway domain is proposed. By adopting the Stochastic Activity Networks formalism, the framework is instantiated to analyse effective trade-offs between energy consumption and satisfaction of other dependability related requirements.DOI: 10.1007/978-3-319-44162-7_10
Metrics:
Basile D, Di Giandomenico F, Gnesi S
Nowadays, there is a great attention towards cautious usage of energy sources to be employed in disparate application domains, including critical infrastructures, to save both in financial terms and in environmental impact. This chapter focuses on stochastic model-based as a support to the analysis of energy saving systems, in combination with other non functional properties, such as reliability, safety and availability. We discuss general guidelines to build a model-based framework to analyse critical cyber-physical systems, where effective energy consumption is required, while assuring imposed levels of resilience. Also, an overview of the most commonly employed methodologies and tools for model-based analysis is provided, and extensive literature is indicated as pointers to relevant research activities performed on this attractive topic over the last decades. Finally, in order to corroborate the proposed framework, a case study in the railway domain is proposed. By adopting the Stochastic Activity Networks formalism, the framework is instantiated to analyse effective trade-offs between energy consumption and satisfaction of other dependability related requirements.DOI: 10.1007/978-3-319-44162-7_10
Metrics:
See at:
CNR IRIS | link.springer.com | doi.org | CNR IRIS | CNR IRIS
2017
Other
Open Access
Controller synthesis of contract-based service product lines: extended version
Basile D, Ter Beek Mh, Di Giandomenico F, Gnesi S, Degano P, Ferrari Gl, Legay A
In Service-Oriented Computing, contracts offer a way to characterise the behavioural conformance of a composition of services, and guarantee that the results do not lead to spurious compositions. Through variability modelling, a product line of services is enabled to adapt to customer requirements and to changes in the context where they operate. We extend a previously introduced formal model of service contracts towards variability and product line modelling, in particular we include: (i) feature-based constraints and (ii) four classes of service requests to characterise different types of service agreement. We then exploit Supervisory Control Theory to synthesise the most permissive controller of a composition 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, the controller 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.
Basile D, Ter Beek Mh, Di Giandomenico F, Gnesi S, Degano P, Ferrari Gl, Legay A
In Service-Oriented Computing, contracts offer a way to characterise the behavioural conformance of a composition of services, and guarantee that the results do not lead to spurious compositions. Through variability modelling, a product line of services is enabled to adapt to customer requirements and to changes in the context where they operate. We extend a previously introduced formal model of service contracts towards variability and product line modelling, in particular we include: (i) feature-based constraints and (ii) four classes of service requests to characterise different types of service agreement. We then exploit Supervisory Control Theory to synthesise the most permissive controller of a composition 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, the controller 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.
See at:
CNR IRIS | ISTI Repository | CNR IRIS
2017
Other
Open Access
A refinement approach to analyse critical cyber-physical systems. Extended Version
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.
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.
See at:
CNR IRIS | ISTI Repository | CNR IRIS
2017
Conference article
Open Access
Statistical model checking of an energy-saving cyber-physical system in the railway domain
Basile D, Di Giandomenico F, Gnesi S
Studies devoted to reduce the energy consumption while guaranteeing acceptable reliability levels are nowadays gaining importance in a variety of application sectors. Analyses through formal models and tools help developers of energy supply strategies in properly trading between energy consumption and reliability. Generally, probabilistic phenomena are involved in those systems, and they can be modelled through stochastic formalisms. Validating these models is paramount, so to guarantee reliance on the analysis results they provide. In this paper, we uniformly address both evaluation and validation of energy consumption policies on a case study from the railway domain using formal techniques. In particular, we analyse a system of rail road switch heaters, which are used to keep the temperature of rail road switches above certain levels to assure their correct functioning. Strategies based on thresholds to control the energy supply are modelled through hybrid automata, a formalism which allows to analyse both the discrete and the continuous nature of cyber-physical systems. We verify the correctness of the proposed model, and we evaluate energy consumption and reliability indicators through Statistical Model Checking using the Uppaal SMC toolbox.DOI: 10.1145/3019612.3019824
Metrics:
Basile D, Di Giandomenico F, Gnesi S
Studies devoted to reduce the energy consumption while guaranteeing acceptable reliability levels are nowadays gaining importance in a variety of application sectors. Analyses through formal models and tools help developers of energy supply strategies in properly trading between energy consumption and reliability. Generally, probabilistic phenomena are involved in those systems, and they can be modelled through stochastic formalisms. Validating these models is paramount, so to guarantee reliance on the analysis results they provide. In this paper, we uniformly address both evaluation and validation of energy consumption policies on a case study from the railway domain using formal techniques. In particular, we analyse a system of rail road switch heaters, which are used to keep the temperature of rail road switches above certain levels to assure their correct functioning. Strategies based on thresholds to control the energy supply are modelled through hybrid automata, a formalism which allows to analyse both the discrete and the continuous nature of cyber-physical systems. We verify the correctness of the proposed model, and we evaluate energy consumption and reliability indicators through Statistical Model Checking using the Uppaal SMC toolbox.DOI: 10.1145/3019612.3019824
Metrics:
See at:
dl.acm.org | CNR IRIS | ISTI Repository | doi.org | CNR IRIS | CNR IRIS
2017
Conference article
Open Access
Orchestration of dynamic service product lines with featured modal contract automata
Basile D., Ter Beek M. H., Di Giandomenico F., Gnesi S.
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.Source: SPLC'17 21st International Systems & Software Product Line Conference, pp. 117–122, Sevilla, Spain, 25-29 September 2017
DOI: 10.1145/3109729.3109741
Metrics:
Basile D., Ter Beek M. H., Di Giandomenico F., Gnesi S.
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.Source: SPLC'17 21st International Systems & Software Product Line Conference, pp. 117–122, Sevilla, Spain, 25-29 September 2017
DOI: 10.1145/3109729.3109741
Metrics:
See at:
ISTI Repository | dl.acm.org | doi.org | CNR ExploRA
2017
Conference article
Open Access
Dependable dynamic routing for urban transport systems through integer linear programming
Basile D, Di Giandomenico F, Gnesi S
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.DOI: 10.1007/978-3-319-68499-4
Project(s): ASTRail
Metrics:
Basile D, Di Giandomenico F, Gnesi S
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.DOI: 10.1007/978-3-319-68499-4
Project(s): ASTRail
Metrics:
See at:
CNR IRIS | ISTI Repository | CNR IRIS | CNR IRIS | link.springer.com | link.springer.com
2017
Conference article
Open Access
FMCAT: Supporting dynamic service-based product lines
Basile D, Di Giandomenico F, Gnesi S
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.DOI: 10.1145/3109729.3109760
Metrics:
Basile D, Di Giandomenico F, Gnesi S
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.DOI: 10.1145/3109729.3109760
Metrics:
See at:
dl.acm.org | CNR IRIS | ISTI Repository | doi.org | CNR IRIS | CNR IRIS
2017
Conference article
Open Access
Enhancing models correctness through formal verification: a case study from the railway domain
Basile D, Di Giandomenico F, Gnesi S
Model-based approaches are widely used for analysing systems belonging to a variety of domains, including the transportation sector. A critical issue with models is their validation, in order to justifiably put reliance on the analysis results they provide (including non functional indicators such as reliability, performance and energy consumption). Typically, cross-validation is performed, e.g. through exercising modelling by different formalisms/tools or through forms of experimental analysis. In this paper, we address validation of a case study from the railway domain via formal techniques, specifically with automata-based models. Validation of interaction aspects of Stochastic Activity Networks models of rail road switch heaters, developed for the purpose of evaluating energy consumption and reliability indicators, is performed through a tool based on contract automata, a recently introduced formalism for verifying properties of communication-based applications.DOI: 10.5220/0006291106790686
Metrics:
Basile D, Di Giandomenico F, Gnesi S
Model-based approaches are widely used for analysing systems belonging to a variety of domains, including the transportation sector. A critical issue with models is their validation, in order to justifiably put reliance on the analysis results they provide (including non functional indicators such as reliability, performance and energy consumption). Typically, cross-validation is performed, e.g. through exercising modelling by different formalisms/tools or through forms of experimental analysis. In this paper, we address validation of a case study from the railway domain via formal techniques, specifically with automata-based models. Validation of interaction aspects of Stochastic Activity Networks models of rail road switch heaters, developed for the purpose of evaluating energy consumption and reliability indicators, is performed through a tool based on contract automata, a recently introduced formalism for verifying properties of communication-based applications.DOI: 10.5220/0006291106790686
Metrics:
See at:
CNR IRIS | ISTI Repository | ISTI Repository | www.scitepress.org | doi.org | CNR IRIS | CNR IRIS