Typology
operator:
and / or
Language
operator:
and / or
Date
operator:
and / or
Rights
operator:
and / or
2016
Software
Unknown
The Stochastic Activity Network models of the rail road switch heating system for Moebius tool
Basile D.
The SAN models of the rail road switch heating system This is a SAN model done in Moebius in 2015 and published at JRTPM2016 https://doi.org/10.1016/j.jrtpm.2016.03.003
Basile D.
The SAN models of the rail road switch heating system This is a SAN model done in Moebius in 2015 and published at JRTPM2016 https://doi.org/10.1016/j.jrtpm.2016.03.003
See at: github.com | CNR ExploRA
2016
Conference article
Open Access
Playing with our CAT and communication-centric applications
Basile D., Degano P., Ferrari G. -L., Tuosto E.
We describe CAT, a toolkit supporting the analysis of communication-centric applications, i.e., applications consisting of ensembles of interacting services. Services are modelled in CAT as contract automata and communication safety is defined in terms of agreement properties. With the help of a simple (albeit non trivial) example, we demonstrate how CAT can (i) verify agreement properties, (ii) synthesise an orchestrator enforcing communication safety, (iii) detect misbehaving services, and (iv) check when the services form a choreography. The use of mixed-integer linear programming is a distinguished characteristic of CAT that allows us to verify context-sensitive properties of agreement.Source: Formal Techniques for Distributed Objects, Components, and System. 36th IFIP WG 6.1 International Conference, pp. 62–73, Heraklion, Crete, Greece, 6-9 June 2016
DOI: 10.1007/978-3-319-39570-8_5
Metrics:
Basile D., Degano P., Ferrari G. -L., Tuosto E.
We describe CAT, a toolkit supporting the analysis of communication-centric applications, i.e., applications consisting of ensembles of interacting services. Services are modelled in CAT as contract automata and communication safety is defined in terms of agreement properties. With the help of a simple (albeit non trivial) example, we demonstrate how CAT can (i) verify agreement properties, (ii) synthesise an orchestrator enforcing communication safety, (iii) detect misbehaving services, and (iv) check when the services form a choreography. The use of mixed-integer linear programming is a distinguished characteristic of CAT that allows us to verify context-sensitive properties of agreement.Source: Formal Techniques for Distributed Objects, Components, and System. 36th IFIP WG 6.1 International Conference, pp. 62–73, Heraklion, Crete, Greece, 6-9 June 2016
DOI: 10.1007/978-3-319-39570-8_5
Metrics:
See at:
hal.inria.fr 
| ISTI Repository | doi.org 
| Hyper Article en Ligne | link.springer.com | CNR ExploRA
2016
Contribution to conference
Open Access
Energy-saving buildings assessment through stochastic hybrid model-based evaluation
Basile D., Di Giandomenico F., Gnesi S.
Optimizing the energy consumption of buildings is an increasingly important topic in ICT. Smart Buildings monitor and control their energy consumptions and safety-related aspect through networks of sensors and actuators connected to the Internet. Policies of energy consumption can be adopted to optimize the interactions among the involved nodes, while satisfying required safety and reliability levels. Stochastic hybrid formalisms have been proved a viable solution for evaluating the effectiveness of energy saving solutions for Smart Buildings, to support tuning of the most suitable one.Source: 2th CINI Annual Conference on ICT for Smart Cities & Communities, Benevento, Italy, 29-30 September 2016
Basile D., Di Giandomenico F., Gnesi S.
Optimizing the energy consumption of buildings is an increasingly important topic in ICT. Smart Buildings monitor and control their energy consumptions and safety-related aspect through networks of sensors and actuators connected to the Internet. Policies of energy consumption can be adopted to optimize the interactions among the involved nodes, while satisfying required safety and reliability levels. Stochastic hybrid formalisms have been proved a viable solution for evaluating the effectiveness of energy saving solutions for Smart Buildings, to support tuning of the most suitable one.Source: 2th CINI Annual Conference on ICT for Smart Cities & Communities, Benevento, Italy, 29-30 September 2016
See at:
ISTI Repository | CNR ExploRA
2016
Journal article
Open Access
Automata for specifying and orchestrating service contracts
Basile D., Degano P., Ferrari G.
An approach to the formal description of service contracts is presented in terms of automata. We focus on the basic property of guaranteeing that in the multi-party composition of principals each of them gets his requests satisfied, so that the overall composition reaches its goal. Depending on whether requests are satisfied synchronously or asynchronously, we construct an orchestrator that at static time either yields composed services enjoying the required properties or detects the principals responsible for possible violations. To do that in the asynchronous case we resort to Linear Programming techniques. We also relate our automata with two logically based methods for specifying contracts.Source: Logical Methods in Computer Science 12 (2016). doi:10.2168/LMCS-12(4:6)2016
DOI: 10.2168/lmcs-12(4:6)2016
Metrics:
Basile D., Degano P., Ferrari G.
An approach to the formal description of service contracts is presented in terms of automata. We focus on the basic property of guaranteeing that in the multi-party composition of principals each of them gets his requests satisfied, so that the overall composition reaches its goal. Depending on whether requests are satisfied synchronously or asynchronously, we construct an orchestrator that at static time either yields composed services enjoying the required properties or detects the principals responsible for possible violations. To do that in the asynchronous case we resort to Linear Programming techniques. We also relate our automata with two logically based methods for specifying contracts.Source: Logical Methods in Computer Science 12 (2016). doi:10.2168/LMCS-12(4:6)2016
DOI: 10.2168/lmcs-12(4:6)2016
Metrics:
See at:
Logical Methods in Computer Science | Logical Methods in Computer Science | lmcs.episciences.org | CNR ExploRA
2016
Report
Open Access
Stochastic model-based evaluation of reliable energy-saving rail road switch heating systems
Basile D., Chiaradonna S., Di Giandomenico F., Gnesi S.
Rail road switch heaters are used to avoid the formation of snow and ice on top of rail road switches during the cold season, in order to guarantee their correct functioning. Effective management of the energy consumption of these devices is important to reduce the costs and minimise the environmental impact. While doing so, it is critical to guarantee the reliability of the system. In this work we analyse reliability and energy consumption indicators for a system of (remotely controlled) rail road switch heaters by developing and solving a stochastic model-based approach based on the Stochastic Activity Networks (SAN) formalism. An on-off policy is considered for heating the switches, with parametric thresholds of activation/deactivation of the heaters and considering different classes of priority. A case study has been developed inspired by a real rail road station, to practically demonstrate the application of the proposed approach to understand the impact of different thresholds and priorities on the indicators under analysis (probability of failure and energy consumption).Source: ISTI Technical reports, 2016
Basile D., Chiaradonna S., Di Giandomenico F., Gnesi S.
Rail road switch heaters are used to avoid the formation of snow and ice on top of rail road switches during the cold season, in order to guarantee their correct functioning. Effective management of the energy consumption of these devices is important to reduce the costs and minimise the environmental impact. While doing so, it is critical to guarantee the reliability of the system. In this work we analyse reliability and energy consumption indicators for a system of (remotely controlled) rail road switch heaters by developing and solving a stochastic model-based approach based on the Stochastic Activity Networks (SAN) formalism. An on-off policy is considered for heating the switches, with parametric thresholds of activation/deactivation of the heaters and considering different classes of priority. A case study has been developed inspired by a real rail road station, to practically demonstrate the application of the proposed approach to understand the impact of different thresholds and priorities on the indicators under analysis (probability of failure and energy consumption).Source: ISTI Technical reports, 2016
See at:
ISTI Repository | CNR ExploRA
2016
Journal article
Open Access
A stochastic model-based approach to analyze reliable energy-saving rail road switch heating systems
Basile D., Chiaradonna S., Di Giandomenico F., Gnesi S.
Rail road switch heaters are used to avoid the formation of snow and ice on top of rail road switches during the cold season, in order to guarantee their correct functioning. Effective management of the energy consumption of these devices is important to reduce the costs and minimise the environmental impact. While doing so, it is critical to guarantee the reliability of the system. In this work we analyse reliability and energy consumption indicators for a system of (remotely controlled) rail road switch heaters by developing and solving a stochastic model-based approach based on the Stochastic Activity Networks (SAN) formalism. An on-off policy is considered for heating the switches, with parametric thresholds of activation/deactivation of the heaters and considering different classes of priority. A case study has been developed inspired by a real rail road station, to practically demonstrate the application of the proposed approach to understand the impact of different thresholds and priorities on the indicators under analysis (probability of failure and energy consumption).Source: Journal of rail transport planning & management (Print) 6 (2016): 163–181. doi:10.1016/j.jrtpm.2016.03.003
DOI: 10.1016/j.jrtpm.2016.03.003
Metrics:
Basile D., Chiaradonna S., Di Giandomenico F., Gnesi S.
Rail road switch heaters are used to avoid the formation of snow and ice on top of rail road switches during the cold season, in order to guarantee their correct functioning. Effective management of the energy consumption of these devices is important to reduce the costs and minimise the environmental impact. While doing so, it is critical to guarantee the reliability of the system. In this work we analyse reliability and energy consumption indicators for a system of (remotely controlled) rail road switch heaters by developing and solving a stochastic model-based approach based on the Stochastic Activity Networks (SAN) formalism. An on-off policy is considered for heating the switches, with parametric thresholds of activation/deactivation of the heaters and considering different classes of priority. A case study has been developed inspired by a real rail road station, to practically demonstrate the application of the proposed approach to understand the impact of different thresholds and priorities on the indicators under analysis (probability of failure and energy consumption).Source: Journal of rail transport planning & management (Print) 6 (2016): 163–181. doi:10.1016/j.jrtpm.2016.03.003
DOI: 10.1016/j.jrtpm.2016.03.003
Metrics:
See at:
Flore (Florence Research Repository) | ISTI Repository | Journal of Rail Transport Planning & Management | www.sciencedirect.com | CNR ExploRA
2016
Conference article
Open Access
Tuning energy consumption strategies in the railway domain: A model-based approach
Basile D., Di Giandomenico F., Gnesi S.
Cautious usage of energy resources is gaining great attention nowadays, both from environmental and economical point of view. Therefore, studies devoted to analyze and predict energy consumption in a variety of application sectors are becoming increasingly important, especially in combination with other non-functional properties, such as reliability, safety and availability. This paper focuses on energy consumption strategies in the railway sector, addressing in particular rail road switches through which trains are guided from one track to another. Given the criticality of their task, the temperature of these devices needs to be kept above certain levels to assure their correct functioning. By applying a stochastic model-based approach, we analyse a family of energy consumption strategies based on thresholds to trigger the activation/deactivation of energy supply. The goal is to offer an assessment framework through which appropriate tuning of threshold-based energy supply solutions can be achieved, so to select the most appropriate one, resulting in a good compromise between energy consumption and reliability level.Source: Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications. 7th International Symposium, pp. 315–330, Corfu, Greece, 10-14 October 2016
DOI: 10.1007/978-3-319-47169-3_23
Metrics:
Basile D., Di Giandomenico F., Gnesi S.
Cautious usage of energy resources is gaining great attention nowadays, both from environmental and economical point of view. Therefore, studies devoted to analyze and predict energy consumption in a variety of application sectors are becoming increasingly important, especially in combination with other non-functional properties, such as reliability, safety and availability. This paper focuses on energy consumption strategies in the railway sector, addressing in particular rail road switches through which trains are guided from one track to another. Given the criticality of their task, the temperature of these devices needs to be kept above certain levels to assure their correct functioning. By applying a stochastic model-based approach, we analyse a family of energy consumption strategies based on thresholds to trigger the activation/deactivation of energy supply. The goal is to offer an assessment framework through which appropriate tuning of threshold-based energy supply solutions can be achieved, so to select the most appropriate one, resulting in a good compromise between energy consumption and reliability level.Source: Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications. 7th International Symposium, pp. 315–330, Corfu, Greece, 10-14 October 2016
DOI: 10.1007/978-3-319-47169-3_23
Metrics:
See at:
ISTI Repository | doi.org | link.springer.com | CNR ExploRA
2016
Journal article
Open Access
Relating two automata-based models of orchestration and choreography
Basile D., Degano P., Ferrari G., Tuosto E.
We investigate the relations between two automata-based models for describing and studying distributed services, called contract automata and communicating machines. In the first model, distributed services are abstracted away as automata - oblivious of their partners - that coordinate with each other through an orchestrator. The second one is concerned with the interactions occurring between distributed services, that are represented by channel-based asynchronous communications; then services are coordinated through choreography. We define a notion of strong agreement on contract automata; exhibit a natural mapping from this model to communicating machines with a synchronous semantics; and give conditions to ensure that strong agreement corresponds to well-formed choreography. Then these results are extended to a more liberal notion of agreement and to a fully asynchronous semantics of communicating machines.Source: Journal of Logical and Algebraic Methods in Programming [online] 85 (2016): 425–446. doi:10.1016/j.jlamp.2015.09.011
DOI: 10.1016/j.jlamp.2015.09.011
Project(s): MEALS
Metrics:
Basile D., Degano P., Ferrari G., Tuosto E.
We investigate the relations between two automata-based models for describing and studying distributed services, called contract automata and communicating machines. In the first model, distributed services are abstracted away as automata - oblivious of their partners - that coordinate with each other through an orchestrator. The second one is concerned with the interactions occurring between distributed services, that are represented by channel-based asynchronous communications; then services are coordinated through choreography. We define a notion of strong agreement on contract automata; exhibit a natural mapping from this model to communicating machines with a synchronous semantics; and give conditions to ensure that strong agreement corresponds to well-formed choreography. Then these results are extended to a more liberal notion of agreement and to a fully asynchronous semantics of communicating machines.Source: Journal of Logical and Algebraic Methods in Programming [online] 85 (2016): 425–446. doi:10.1016/j.jlamp.2015.09.011
DOI: 10.1016/j.jlamp.2015.09.011
Project(s): MEALS
Metrics:
See at:
Journal of Logical and Algebraic Methods in Programming | Flore (Florence Research Repository) | CNR ExploRA
2016
Software
Unknown
AMPL model for Weak Agreement in contract automata, implementation of weak liability checking, published at FORTE2016
Basile D.
AMPL model for Weak Agreement in contract automata, implementation of weak liability checking, published at FORTE2016. This is a prototype implementation of the verification techniques for the properties of weak agreement and weak safety of a CA. The linear problems are specified using AMPL. (http://www.ampl.com/DOWNLOADS/) The main files are: weakagreement.mod weaksafety.mod To run an example print from command line "ampl flow.run", the script flow.run will be executed, that will check if the CA described in the file "flow.dat" admits weak agreement. To check weak safety it suffices to change in the file "flow.run" the model to weaksafety.mod. The specification of the CA is given in the file flow.dat. An automa is defined through: the number of nodes (it is assumed that the node 1 is the initial node); the id of the final node (assuming only one final state); the cardinality of the alphabet of actions the matrix of transitions (0 if there is no transition for the arc (n,m) 1 if there is a transition for the arc (n,m) ) for each action a matrix of labels ( 1 if the action is an offer in the transition (n,m) -1 if the action is a request in the transition (n,m) 0 if the action is a match )
Basile D.
AMPL model for Weak Agreement in contract automata, implementation of weak liability checking, published at FORTE2016. This is a prototype implementation of the verification techniques for the properties of weak agreement and weak safety of a CA. The linear problems are specified using AMPL. (http://www.ampl.com/DOWNLOADS/) The main files are: weakagreement.mod weaksafety.mod To run an example print from command line "ampl flow.run", the script flow.run will be executed, that will check if the CA described in the file "flow.dat" admits weak agreement. To check weak safety it suffices to change in the file "flow.run" the model to weaksafety.mod. The specification of the CA is given in the file flow.dat. An automa is defined through: the number of nodes (it is assumed that the node 1 is the initial node); the id of the final node (assuming only one final state); the cardinality of the alphabet of actions the matrix of transitions (0 if there is no transition for the arc (n,m) 1 if there is a transition for the arc (n,m) ) for each action a matrix of labels ( 1 if the action is an offer in the transition (n,m) -1 if the action is a request in the transition (n,m) 0 if the action is a match )
See at: github.com | CNR ExploRA