2016
Doctoral thesis
Unknown
Agile processes and formal methods in railway systems
Spagnolo G. O.
A business subject who decides to enter an established technological market is required to accurately analyse the products of the different competitors. In the case of cheap mass products (e.g., mobiles, laptops), the new company can actually purchase the products and evaluate their features in order to compare them. In the case of expensive, large-scale, and often customized, products (e.g., security systems, intelligent transport systems), the company has to rely on the existing public documentation about the products, since the cost required to purchase the actual products would be prohibitive. In this work, we consider the case of Communications-Based Train Control (CBTC) systems. In this context this dissertation present the development a safety critical system, with limited knowledge of the domain, in a context with multiple competitors. The safety critical system shall be developed according to standards (process and product standards). At the same time, there is a limited know- ledge of the domain. Hence, agile methods fit the need of having an in-depth view of the problem, in limited time, and with limited knowledge.
Spagnolo G. O.
A business subject who decides to enter an established technological market is required to accurately analyse the products of the different competitors. In the case of cheap mass products (e.g., mobiles, laptops), the new company can actually purchase the products and evaluate their features in order to compare them. In the case of expensive, large-scale, and often customized, products (e.g., security systems, intelligent transport systems), the company has to rely on the existing public documentation about the products, since the cost required to purchase the actual products would be prohibitive. In this work, we consider the case of Communications-Based Train Control (CBTC) systems. In this context this dissertation present the development a safety critical system, with limited knowledge of the domain, in a context with multiple competitors. The safety critical system shall be developed according to standards (process and product standards). At the same time, there is a limited know- ledge of the domain. Hence, agile methods fit the need of having an in-depth view of the problem, in limited time, and with limited knowledge.
See at: CNR ExploRA
2021
Report
Open Access
Esportazione memoria permanente di riepilogo registratore telematico
Spagnolo G. O., Surano D.
Esportazione Memoria di riepilogo RT: codifiche ed uso proposta di nuovo tracciato che estende il precedente per estrarre tutte le informazioni immagazzinate nella memoria di riepilogo del registratore telematico.Source: ISTI Technical Report, ISTI-2021-TR/014, pp.1–23, 2021
DOI: 10.32079/isti-tr-2021/014
Metrics:
Spagnolo G. O., Surano D.
Esportazione Memoria di riepilogo RT: codifiche ed uso proposta di nuovo tracciato che estende il precedente per estrarre tutte le informazioni immagazzinate nella memoria di riepilogo del registratore telematico.Source: ISTI Technical Report, ISTI-2021-TR/014, pp.1–23, 2021
DOI: 10.32079/isti-tr-2021/014
Metrics:
See at:
ISTI Repository 
| CNR ExploRA
2021
Report
Open Access
Esportazione memoria permanente di dettaglio registratore telematico
Spagnolo G. O., Surano D.
Esportazione Memoria Permanente di Dettaglio Registratore Telematico, codifiche ed uso proposta estensione tracciato esportazione memoria di dettaglio per consentire la esportazione di tutte le informazioni salvate nella memoria di dettaglio del RT.Source: ISTI Technical Report, ISTI-2021-TR/013, pp.1–29, 2021
DOI: 10.32079/isti-tr-2021/013
Metrics:
Spagnolo G. O., Surano D.
Esportazione Memoria Permanente di Dettaglio Registratore Telematico, codifiche ed uso proposta estensione tracciato esportazione memoria di dettaglio per consentire la esportazione di tutte le informazioni salvate nella memoria di dettaglio del RT.Source: ISTI Technical Report, ISTI-2021-TR/013, pp.1–29, 2021
DOI: 10.32079/isti-tr-2021/013
Metrics:
See at:
ISTI Repository | CNR ExploRA
2013
Report
Unknown
CBTC.AGEN.0023_00_06 Protocollo ATS-ATC
Spagnolo G. O., Mazzanti F.
Tecnical report of Protocol ATS-ATC.Source: ISTI Technical reports, 2013
Spagnolo G. O., Mazzanti F.
Tecnical report of Protocol ATS-ATC.Source: ISTI Technical reports, 2013
See at: CNR ExploRA
2014
Journal article
Restricted
From commercial documents to system requirements: an approach for the engineering of novel CBTC solutions
Ferrari A., Spagnolo G. O., Menabeni S., Martelli G.
Communications-based train control (CBTC) systems are the new frontier of automated train control and operation. Currently developed CBTC platforms are actually very complex systems including several functionalities, and every installed system, developed by a different company, varies in extent, scope, number, and even names of the implemented functionalities. International standards have emerged, but they remain at a quite abstract level, mostly setting terminology. This paper presents the results of an experience in defining a global model of CBTC, by mixing semi-formal modelling and product line engineering. The effort has been based on an in-depth market analysis, not limiting to particular aspects but considering as far as possible the whole picture. The paper also describes a methodology to derive novel CBTC products from the global model, and to define system requirements for the individual CBTC components. To this end, the proposed methodology employs scenario-based requirements elicitation aided with rapid prototyping. To enhance the quality of the requirements, these are written in a constrained natural language (CNL), and evaluated with natural language processing (NLP) techniques. The final goal is to go toward a formal representation of the requirements for CBTC systems. The overall approach is discussed, and the current experience with the implementation of the method is presented. In particular, we show how the presented methodology has been used in practice to derive a novel CBTC architecture.Source: International journal on software tools for technology transfer (Print) (2014): 1–21. doi:10.1007/s10009-013-0298-6
DOI: 10.1007/s10009-013-0298-6
Metrics:
Ferrari A., Spagnolo G. O., Menabeni S., Martelli G.
Communications-based train control (CBTC) systems are the new frontier of automated train control and operation. Currently developed CBTC platforms are actually very complex systems including several functionalities, and every installed system, developed by a different company, varies in extent, scope, number, and even names of the implemented functionalities. International standards have emerged, but they remain at a quite abstract level, mostly setting terminology. This paper presents the results of an experience in defining a global model of CBTC, by mixing semi-formal modelling and product line engineering. The effort has been based on an in-depth market analysis, not limiting to particular aspects but considering as far as possible the whole picture. The paper also describes a methodology to derive novel CBTC products from the global model, and to define system requirements for the individual CBTC components. To this end, the proposed methodology employs scenario-based requirements elicitation aided with rapid prototyping. To enhance the quality of the requirements, these are written in a constrained natural language (CNL), and evaluated with natural language processing (NLP) techniques. The final goal is to go toward a formal representation of the requirements for CBTC systems. The overall approach is discussed, and the current experience with the implementation of the method is presented. In particular, we show how the presented methodology has been used in practice to derive a novel CBTC architecture.Source: International journal on software tools for technology transfer (Print) (2014): 1–21. doi:10.1007/s10009-013-0298-6
DOI: 10.1007/s10009-013-0298-6
Metrics:
See at:
International Journal on Software Tools for Technology Transfer 
| link.springer.com | CNR ExploRA
2014
Software
Unknown
Completeness assistant for requirements
Ferrari A., Spagnolo G. O.
Completeness Assistant for Requirements (CAR) is a natural language processing tool, to improve the completeness of the requirements, which supports the definition of the requirements: the tool helps the requirements engineer in discovering relevant concepts and interactions.
Ferrari A., Spagnolo G. O.
Completeness Assistant for Requirements (CAR) is a natural language processing tool, to improve the completeness of the requirements, which supports the definition of the requirements: the tool helps the requirements engineer in discovering relevant concepts and interactions.
See at: github.com | CNR ExploRA
2016
Software
Unknown
Verification component understandability BPMN
Spagnolo G. O., Ferrari A.
In Learn PAd, we developed a quality assessment strategy that allows to guarantee that the used BP models result being understandable by the civil servants. The quality assessment strategy includes modeling understandability guidelines which are supported by a Java tool called verification component understandability BPMN.Project(s): LEARN PAD
Spagnolo G. O., Ferrari A.
In Learn PAd, we developed a quality assessment strategy that allows to guarantee that the used BP models result being understandable by the civil servants. The quality assessment strategy includes modeling understandability guidelines which are supported by a Java tool called verification component understandability BPMN.Project(s): LEARN PAD
See at: github.com | CNR ExploRA
2016
Software
Unknown
User interface for content analysis component
Spagnolo G. O., Ferrari A.
This is the Content Analysis component of the LearnPAd platform. It implements automated procedures to verify that the textual content that describes the tasks of a Business Process (e.g., documents created in the Collaborative Workspace) provides information that is consistent with respect to the Business Process model itself, and to automatically identify ambiguous sentences and vague terms in natural language requirements, and estimates quantitative indexes concerning the linguistic quality of the contents.Project(s): LEARN PAD
Spagnolo G. O., Ferrari A.
This is the Content Analysis component of the LearnPAd platform. It implements automated procedures to verify that the textual content that describes the tasks of a Business Process (e.g., documents created in the Collaborative Workspace) provides information that is consistent with respect to the Business Process model itself, and to automatically identify ambiguous sentences and vague terms in natural language requirements, and estimates quantitative indexes concerning the linguistic quality of the contents.Project(s): LEARN PAD
See at: github.com | CNR ExploRA
2016
Software
Unknown
User Interface for guidelines verification component
Spagnolo G. O., Ferrari A.
User Interface for guidelines verification component.Project(s): LEARN PAD
Spagnolo G. O., Ferrari A.
User Interface for guidelines verification component.Project(s): LEARN PAD
See at: github.com | CNR ExploRA
2016
Software
Unknown
Content analysis component
Spagnolo G. O., Ferrari A.
The Content Analysis Component includes all the functionalities for analysing NL content of procedure descriptions coming from the LearnPAd platform. It implements automated procedures to verify that the textual content that describes the tasks of a Business Process (e.g., documents created in the Collaborative Workspace) provides information that is consistent with respect to the Business Process model itself, and to automatically identify ambiguous sentences and vague terms in natural language requirements, and estimates quantitative indexes concerning the linguistic quality of the contents.Project(s): LEARN PAD
Spagnolo G. O., Ferrari A.
The Content Analysis Component includes all the functionalities for analysing NL content of procedure descriptions coming from the LearnPAd platform. It implements automated procedures to verify that the textual content that describes the tasks of a Business Process (e.g., documents created in the Collaborative Workspace) provides information that is consistent with respect to the Business Process model itself, and to automatically identify ambiguous sentences and vague terms in natural language requirements, and estimates quantitative indexes concerning the linguistic quality of the contents.Project(s): LEARN PAD
See at: github.com | CNR ExploRA
2019
Contribution to book
Open Access
QuOD: An NLP Tool to Improve the Quality of Business Process Descriptions
Ferrari A., Spagnolo G. O., Fiscella A., Parente G.
In real-world organisations, business processes (BPs) are often described by means of natural language (NL) documents. Indeed, although semi-formal graphical notations exist to model BPs, most of the legacy process knowledge--when not tacit--is still conveyed through textual procedures or operational manuals, in which the BPs are specified. This is particularly true for public administrations (PAs), in which a large variety of BPs exist (e.g., definition of tenders, front-desk support) that have to be understood and put into practice by civil servants. [Question/problem] Incorrect understanding of the BP descriptions in PAs may cause delays in the delivery of services to citizens, or, in some cases, incorrect execution of the BPs. [Principal idea/results] In this paper, we present the development of an NLP-based tool named QuOD (Quality Analyser for Official Documents), oriented to detect linguistic defects in BP descriptions and to provide recommendations for improvements. [Contribution] QuOD is the first tool that addresses the problem of identifying NL defects in BP descriptions of PAs. The tool is available online at http://narwhal.it/quod/index.html.Source: From Software Engineering to Formal Methods and Tools, and Back Essays Dedicated to Stefania Gnesi on the Occasion of Her 65th Birthday, edited by ter Beek M.H.; Fantechi A.; Semini L., pp. 267–281, 2019
DOI: 10.1007/978-3-030-30985-5_17
Metrics:
Ferrari A., Spagnolo G. O., Fiscella A., Parente G.
In real-world organisations, business processes (BPs) are often described by means of natural language (NL) documents. Indeed, although semi-formal graphical notations exist to model BPs, most of the legacy process knowledge--when not tacit--is still conveyed through textual procedures or operational manuals, in which the BPs are specified. This is particularly true for public administrations (PAs), in which a large variety of BPs exist (e.g., definition of tenders, front-desk support) that have to be understood and put into practice by civil servants. [Question/problem] Incorrect understanding of the BP descriptions in PAs may cause delays in the delivery of services to citizens, or, in some cases, incorrect execution of the BPs. [Principal idea/results] In this paper, we present the development of an NLP-based tool named QuOD (Quality Analyser for Official Documents), oriented to detect linguistic defects in BP descriptions and to provide recommendations for improvements. [Contribution] QuOD is the first tool that addresses the problem of identifying NL defects in BP descriptions of PAs. The tool is available online at http://narwhal.it/quod/index.html.Source: From Software Engineering to Formal Methods and Tools, and Back Essays Dedicated to Stefania Gnesi on the Occasion of Her 65th Birthday, edited by ter Beek M.H.; Fantechi A.; Semini L., pp. 267–281, 2019
DOI: 10.1007/978-3-030-30985-5_17
Metrics:
See at:
ISTI Repository | doi.org | link.springer.com | CNR ExploRA
2022
Conference article
Restricted
Technical debt management in automotive software industry
Lami G., Spagnolo G. O.
The suppliers of software-intensive electronic automotive components are facing technical challenges due to the innovation rush and the growing time pressure from customers. As the quality of on-board automotive electronic systems is strongly dependent on the quality of their development practices, car manufacturers and suppliers proactively focus on improving technical and organizational processes. Automotive SPICE (ASPICE) is today the reference standard for assessing and improving automotive electronics processes and projects in this setting. As car manufacturers use ASPICE to qualify their suppliers of software-intensive systems, such a standard becomes a market demand. This paper identifies and discusses the benefits and impact of the integration and harmonization of Technical Debt Management (TDM) in an ASPICE- compliant software development project. Besides this paper provides a conceptual framework and a reference process description for the integration of ASPICE and TDM practices in a sample Software Engineering process.Source: SEAA 2022 - 48th EUROMICRO Conference on Software Engineering and Advanced Applications, pp. 294–297, Maspalomas, Gran Canaria, Spain, 31/08 - 02/09/2022
DOI: 10.1109/seaa56994.2022.00053
Metrics:
Lami G., Spagnolo G. O.
The suppliers of software-intensive electronic automotive components are facing technical challenges due to the innovation rush and the growing time pressure from customers. As the quality of on-board automotive electronic systems is strongly dependent on the quality of their development practices, car manufacturers and suppliers proactively focus on improving technical and organizational processes. Automotive SPICE (ASPICE) is today the reference standard for assessing and improving automotive electronics processes and projects in this setting. As car manufacturers use ASPICE to qualify their suppliers of software-intensive systems, such a standard becomes a market demand. This paper identifies and discusses the benefits and impact of the integration and harmonization of Technical Debt Management (TDM) in an ASPICE- compliant software development project. Besides this paper provides a conceptual framework and a reference process description for the integration of ASPICE and TDM practices in a sample Software Engineering process.Source: SEAA 2022 - 48th EUROMICRO Conference on Software Engineering and Advanced Applications, pp. 294–297, Maspalomas, Gran Canaria, Spain, 31/08 - 02/09/2022
DOI: 10.1109/seaa56994.2022.00053
Metrics:
See at:
ieeexplore.ieee.org | CNR ExploRA
2023
Contribution to book
Open Access
REFSQ 2023: joint proceedings of workshops, doctoral symposium, posters & tools track, and journal early feedback track - Preface
Spagnolo G. O., Ferrari A., Penzenstadler B.
This document is the preface of the Joint Proceedings of Workshops, Doctoral Symposium, Posters & Tools Track, and Journal Early Feedback Track of the 29th International Working Conference on Requirement Engineering: Foundation for Software Quality (REFSQ 2023), 17th--20th April 2023, held in Barcelona, Catalunya, Spain.Source: Joint Proceedings of REFSQ-2023 Workshops, Doctoral Symposium, Posters & Tools Track and Journal Early Feedback co-located with the 28th International Conference on Requirements Engineering: Foundation for Software Quality (REFSQ 2023), edited by Ferrari A. et al., 2023
Spagnolo G. O., Ferrari A., Penzenstadler B.
This document is the preface of the Joint Proceedings of Workshops, Doctoral Symposium, Posters & Tools Track, and Journal Early Feedback Track of the 29th International Working Conference on Requirement Engineering: Foundation for Software Quality (REFSQ 2023), 17th--20th April 2023, held in Barcelona, Catalunya, Spain.Source: Joint Proceedings of REFSQ-2023 Workshops, Doctoral Symposium, Posters & Tools Track and Journal Early Feedback co-located with the 28th International Conference on Requirements Engineering: Foundation for Software Quality (REFSQ 2023), edited by Ferrari A. et al., 2023
See at:
ceur-ws.org | ISTI Repository | CNR ExploRA
2012
Conference article
Restricted
Product Line Engineering Applied to CBTC Systems Development
Ferrari A., Spagnolo G. O., Martelli G., Menabeni S.
Communications-based Train Control (CBTC) systems are the new frontier of automated train control and operation. Currently developed CBTC platforms are actually very complex systems including several functionalities, and every installed system, developed by a different company, varies in extent, scope, number, and even names of the implemented functionalities. International standards have emerged, but they remain at a quite abstract level, mostly setting terminology. This paper reports intermediate results in an effort aimed at defining a global model of CBTC, by mixing semi-formal modelling and product line engineering. The effort has been based on an in-depth market analysis, not limiting to particular aspects but considering as far as possible the whole picture. The adopted methodology is discussed and a preliminary model is presented.Source: ISoLA 2012 - 5th International Symposium on Leveraging Applications of Formal Methods, pp. 216–230, Heraklion, Greece, 15-18/10/2012
DOI: 10.1007/978-3-642-34032-1_22
Metrics:
Ferrari A., Spagnolo G. O., Martelli G., Menabeni S.
Communications-based Train Control (CBTC) systems are the new frontier of automated train control and operation. Currently developed CBTC platforms are actually very complex systems including several functionalities, and every installed system, developed by a different company, varies in extent, scope, number, and even names of the implemented functionalities. International standards have emerged, but they remain at a quite abstract level, mostly setting terminology. This paper reports intermediate results in an effort aimed at defining a global model of CBTC, by mixing semi-formal modelling and product line engineering. The effort has been based on an in-depth market analysis, not limiting to particular aspects but considering as far as possible the whole picture. The adopted methodology is discussed and a preliminary model is presented.Source: ISoLA 2012 - 5th International Symposium on Leveraging Applications of Formal Methods, pp. 216–230, Heraklion, Greece, 15-18/10/2012
DOI: 10.1007/978-3-642-34032-1_22
Metrics:
See at:
doi.org | link.springer.com | CNR ExploRA
2012
Conference article
Restricted
Model-based evaluation of the availability of a CBTC system.
Ferrari A., Itria M. L., Chiaradonna S., Spagnolo G. O.
A metro control system is a software/hardware platform that provides automated mechanisms to enforce the safety of a metropolitan transportation system. In this field, the current technical trend is the Communications-based Train Control (CBTC) solution. CBTC platforms are characterized by a continuous wireless interaction between trains and ground controls. Several degrees of automation are provided, from basic traffic monitoring to unattended train operation. Besides safety issues, a CBTC system is also required to guarantee a high level of availability. These platforms are normally composed of several subsystems and devices, and estimating the overall availability of the system is not a trivial task. Stochastic Activity Networks (SAN) are a powerful formalism that allows modelling and evaluating complex distributed systems. In this paper, a study is presented that shows how SAN models can be employed to evaluate the availability attributes of a CBTC system. The current results show that the SAN technology and the analysis tool adopted, named Möbius, are mature for a profitable employment in industrial practice.Source: Software Engineering for Resilient Systems. 4th International Workshop, pp. 165–179, Pisa, Italy, 27-28 September 2012
DOI: 10.1007/978-3-642-33176-3_12
Metrics:
Ferrari A., Itria M. L., Chiaradonna S., Spagnolo G. O.
A metro control system is a software/hardware platform that provides automated mechanisms to enforce the safety of a metropolitan transportation system. In this field, the current technical trend is the Communications-based Train Control (CBTC) solution. CBTC platforms are characterized by a continuous wireless interaction between trains and ground controls. Several degrees of automation are provided, from basic traffic monitoring to unattended train operation. Besides safety issues, a CBTC system is also required to guarantee a high level of availability. These platforms are normally composed of several subsystems and devices, and estimating the overall availability of the system is not a trivial task. Stochastic Activity Networks (SAN) are a powerful formalism that allows modelling and evaluating complex distributed systems. In this paper, a study is presented that shows how SAN models can be employed to evaluate the availability attributes of a CBTC system. The current results show that the SAN technology and the analysis tool adopted, named Möbius, are mature for a profitable employment in industrial practice.Source: Software Engineering for Resilient Systems. 4th International Workshop, pp. 165–179, Pisa, Italy, 27-28 September 2012
DOI: 10.1007/978-3-642-33176-3_12
Metrics:
See at:
doi.org | link.springer.com | CNR ExploRA
2013
Report
Unknown
CBTC.ATS.0001_00_05 Specifica preliminare di sistema
Spagnolo G. O, Ferrari A., Mazzanti F.
Preliminary Requirements and Specification System for ATS (Automatic Train Supervision) within the CBTC according to the reference standardSource: ISTI Technical reports, 2013
Spagnolo G. O, Ferrari A., Mazzanti F.
Preliminary Requirements and Specification System for ATS (Automatic Train Supervision) within the CBTC according to the reference standardSource: ISTI Technical reports, 2013
See at: CNR ExploRA
2013
Conference article
Restricted
Mining commonalities and variabilities from natural language documents
Ferrari A., Spagnolo G. O., Dell'Orletta F.
A company who wishes to enter an established marked with a new, competitive product is required to analyse the product solutions of the competitors. Identifying and comparing the features provided by the other vendors might greatly help during the market analysis. However, mining common and variant features of from the publicly available documents of the competitors is a time consuming and error-prone task. In this paper, we suggest to employ a natural language processing approach based on textit{contrastive analysis} to identify commonalities and variabilities from the brochures of a group of vendors. We present a first step towards a practical application of the approach, in the the context of the market of Communications-Based Train Control (CBTC) systems.Source: SPLC 2013 - 17th International Software Product Line Conference, pp. 116–120, Tokyo, Japan, 26-30 August 2013
Ferrari A., Spagnolo G. O., Dell'Orletta F.
A company who wishes to enter an established marked with a new, competitive product is required to analyse the product solutions of the competitors. Identifying and comparing the features provided by the other vendors might greatly help during the market analysis. However, mining common and variant features of from the publicly available documents of the competitors is a time consuming and error-prone task. In this paper, we suggest to employ a natural language processing approach based on textit{contrastive analysis} to identify commonalities and variabilities from the brochures of a group of vendors. We present a first step towards a practical application of the approach, in the the context of the market of Communications-Based Train Control (CBTC) systems.Source: SPLC 2013 - 17th International Software Product Line Conference, pp. 116–120, Tokyo, Japan, 26-30 August 2013
See at:
dl.acm.org | CNR ExploRA
2014
Report
Unknown
TCPS specifica business process e log.
Spagnolo G. O., Coco A., Marchetti E.
Present the business process model of the TPCS system. Modelling the export and import processes of the Port of Livorno. Describe the structure of the logs that the system must have in order to apply the techniques of processes mining.Source: ISTI Technical reports, 2014
Spagnolo G. O., Coco A., Marchetti E.
Present the business process model of the TPCS system. Modelling the export and import processes of the Port of Livorno. Describe the structure of the logs that the system must have in order to apply the techniques of processes mining.Source: ISTI Technical reports, 2014
See at: CNR ExploRA
2014
Conference article
Restricted
Deadlock avoidance in train scheduling: A model checking approach
Mazzanti F., Spagnolo G. O., Della Longa S., Ferrari A.
In this paper we present the deadlock avoidance approach used in the design of the scheduling kernel of an Automatic Train Supervision (ATS) system. The ATS that we have designed prevents the occurrence of deadlocks by performing a set of runtime checks just before allowing a train to move further. For each train, the set of checks to be performed at each step of progress is retrieved from statically generated ATS configuration data. For the verification of the correctness of the logic used by the ATS and the validation of the constraints verified by the runtime checks, we define a formal model that represents the ATS behavior, the railway layout, and the planned service structure. We use this formal model to verify both the absence of deadlocks and absence of false positives (i.e., cases in which a train is unnecessarily disallowed to proceed). The verification is carried out by exploiting the UMC model checking verification framework locally developed at ISTI-CNR. © 2014 Springer International Publishing.Source: FMICS 2014 - Formal Methods for Industrial Critical Systems. 19th International Conference, pp. 109–123, Florence, Italy, 11-12 September 2014
DOI: 10.1007/978-3-319-10702-8_8
Metrics:
Mazzanti F., Spagnolo G. O., Della Longa S., Ferrari A.
In this paper we present the deadlock avoidance approach used in the design of the scheduling kernel of an Automatic Train Supervision (ATS) system. The ATS that we have designed prevents the occurrence of deadlocks by performing a set of runtime checks just before allowing a train to move further. For each train, the set of checks to be performed at each step of progress is retrieved from statically generated ATS configuration data. For the verification of the correctness of the logic used by the ATS and the validation of the constraints verified by the runtime checks, we define a formal model that represents the ATS behavior, the railway layout, and the planned service structure. We use this formal model to verify both the absence of deadlocks and absence of false positives (i.e., cases in which a train is unnecessarily disallowed to proceed). The verification is carried out by exploiting the UMC model checking verification framework locally developed at ISTI-CNR. © 2014 Springer International Publishing.Source: FMICS 2014 - Formal Methods for Industrial Critical Systems. 19th International Conference, pp. 109–123, Florence, Italy, 11-12 September 2014
DOI: 10.1007/978-3-319-10702-8_8
Metrics:
See at:
doi.org | www.scopus.com | CNR ExploRA
2014
Conference article
Restricted
Designing a deadlock-free train scheduler: A model checking approach
Mazzanti F., Spagnolo G. O., Ferrari A.
In this paper we present the approach used in the design of the scheduling kernel of an Automatic Train Supervision (ATS) system. A formal model of the railway layout and of the expected service has been used to identify all the possible critical sections of the railway layout in which a deadlock might occur. For each critical section, the prevention of the occurrence of deadlocks is achieved by constraining the set of trains allowed to occupy these sections at the same time. The identification of the critical sections and the verification of the correctness of the logic used by the ATS is carried out by exploiting a model checking verification framework locally developed at ISTI-CNR and based on the tool UMC.Source: NASA Formal Methods. 6th International Symposium, pp. 264–269, Houston, TX, USA, 29 April - 1 May 2014
DOI: 10.1007/978-3-319-06200-6_22
Metrics:
Mazzanti F., Spagnolo G. O., Ferrari A.
In this paper we present the approach used in the design of the scheduling kernel of an Automatic Train Supervision (ATS) system. A formal model of the railway layout and of the expected service has been used to identify all the possible critical sections of the railway layout in which a deadlock might occur. For each critical section, the prevention of the occurrence of deadlocks is achieved by constraining the set of trains allowed to occupy these sections at the same time. The identification of the critical sections and the verification of the correctness of the logic used by the ATS is carried out by exploiting a model checking verification framework locally developed at ISTI-CNR and based on the tool UMC.Source: NASA Formal Methods. 6th International Symposium, pp. 264–269, Houston, TX, USA, 29 April - 1 May 2014
DOI: 10.1007/978-3-319-06200-6_22
Metrics:
See at:
doi.org | www.scopus.com | CNR ExploRA