9 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
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

See at: github.com | CNR ExploRA


2016 Conference article Open Access OPEN

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

See at: hal.inria.fr Open Access | ISTI Repository Open Access | academic.microsoft.com Restricted | arpi.unipi.it Restricted | core.ac.uk Restricted | dblp.uni-trier.de Restricted | doi.org Restricted | flore.unifi.it Restricted | hal.inria.fr Restricted | hal.inria.fr Restricted | Hyper Article en Ligne Restricted | link.springer.com Restricted | link.springer.com Restricted | CNR ExploRA Restricted | rd.springer.com Restricted


2016 Contribution to conference Open Access OPEN

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

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


2016 Journal article Open Access OPEN

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
DOI: 10.1007/978-3-662-45917-1_3

See at: Logical Methods in Computer Science Open Access | Logical Methods in Computer Science Open Access | Logical Methods in Computer Science Open Access | Logical Methods in Computer Science Open Access | Logical Methods in Computer Science Open Access | Logical Methods in Computer Science Open Access | www.cs.le.ac.uk Open Access | academic.microsoft.com Restricted | arpi.unipi.it Restricted | core.ac.uk Restricted | dblp.uni-trier.de Restricted | flore.unifi.it Restricted | link.springer.com Restricted | link.springer.com Restricted | lmcs.episciences.org Restricted | CNR ExploRA Restricted | rd.springer.com Restricted


2016 Report Open Access OPEN

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

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


2016 Journal article Open Access OPEN

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

See at: ISTI Repository Open Access | Journal of Rail Transport Planning & Management Restricted | Journal of Rail Transport Planning & Management Restricted | Journal of Rail Transport Planning & Management Restricted | Journal of Rail Transport Planning & Management Restricted | CNR ExploRA Restricted | Journal of Rail Transport Planning & Management Restricted | Journal of Rail Transport Planning & Management Restricted | www.sciencedirect.com Restricted


2016 Conference article Open Access OPEN

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

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 | link.springer.com Restricted | link.springer.com Restricted | CNR ExploRA Restricted | rd.springer.com Restricted


2016 Journal article Open Access OPEN

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 via OpenAIRE

See at: Journal of Logical and Algebraic Methods in Programming Open Access | Journal of Logical and Algebraic Methods in Programming Restricted | Journal of Logical and Algebraic Methods in Programming Restricted | Journal of Logical and Algebraic Methods in Programming Restricted | Journal of Logical and Algebraic Methods in Programming Restricted | Journal of Logical and Algebraic Methods in Programming Restricted | Journal of Logical and Algebraic Methods in Programming Restricted | Journal of Logical and Algebraic Methods in Programming Restricted | Journal of Logical and Algebraic Methods in Programming Restricted | CNR ExploRA Restricted | Journal of Logical and Algebraic Methods in Programming Restricted


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 )

See at: github.com | CNR ExploRA