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.

Enhancing Models Correctness through Formal Verification: A Case Study from the Railway Domain / Gnesi, Stefania; Di Giandomenico, Felicita; Basile, Davide. - ELETTRONICO. - (2017), pp. 679-686. (Intervento presentato al convegno 5th International Conference on Model-Driven Engineering and Software Development, MODELSWARD 2017) [10.5220/0006291106790686].

Enhancing Models Correctness through Formal Verification: A Case Study from the Railway Domain

Di Giandomenico, Felicita;Basile, Davide
2017

Abstract

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.
2017
Proceedings of the 5th International Conference on Model-Driven Engineering and Software Development, MODELSWARD 2017,
5th International Conference on Model-Driven Engineering and Software Development, MODELSWARD 2017
Gnesi, Stefania; Di Giandomenico, Felicita; Basile, Davide
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificatore per citare o creare un link a questa risorsa: https://hdl.handle.net/2158/1142446
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 2
social impact