Publication
Verification of multiple models of a safetycritical motor controller in railway systems
| dc.contributor.author | Proenca, José | |
| dc.contributor.author | Borrami, Sina | |
| dc.contributor.author | Nova, Jorge Sanchez de | |
| dc.contributor.author | Pereira, David | |
| dc.contributor.author | Spilere Nandi, Giann | |
| dc.date.accessioned | 2022-06-22T15:13:46Z | |
| dc.date.available | 2022-06-22T15:13:46Z | |
| dc.date.issued | 2022-06-02 | |
| dc.description.abstract | Motor controllers, such as the ones used in signalling systems, include critical embedded software. Alstom is a company that produces such embedded systems, which must follow complex certification processes that require formal modelling and analysis. The formal analysis of these real-time systems have to balance between including enough details to be useful and abstracting away enough details to be verifiable. This paper describes our work in the context of the European VALU3S project to integrate the analysis of such systems with the Uppaal model checker during the development cycle, involving both developers from Alstom and academic partners. We use special Excel tables to configure the underlying Uppaal models and requirements, bridging these two stakeholders. We follow Software Product Line Engineering principles, e.g., allowing features to be turned on and off and periodicities to be changed, and verify different properties for each of such configuration. We automate the instantiation and verification in Uppaal of a set of selected configurations via an open-source prototype tool named Uppex. | pt_PT |
| dc.description.sponsorship | This work was partially supported by National Funds through FCT/MCTES (Portuguese Foundation for Science and Technology), within the CISTER Research Unit (UIDP/UIDB/04234/2020); also by the Norte Portugal Regional Operational Programme (NORTE 2020) under the Portugal 2020 Partnership Agreement, through the European Regional Development Fund (ERDF) and also by national funds through the FCT, within project NORTE-01-0145-FEDER-028550 (REASSURE); also by COMPETE 2020 under the PT2020 Partnership Agreement, through ERDF, and by national funds through the FCT, within project POCI-01-0145-FEDER- 029946 (DaVinci); also by FCT within project ECSEL/0016/2019 and from the ECSEL Joint Undertaking (JU) under grant agreement No 876852 (VALU3S). The JU receives support from the European Union's Horizon 2020 research and innovation programme and Austria, Czech Republic, Germany, Ireland, Italy, Portugal, Spain, Sweden, Turkey. | pt_PT |
| dc.description.version | N/A | pt_PT |
| dc.identifier.uri | http://hdl.handle.net/10400.22/20635 | |
| dc.language.iso | eng | pt_PT |
| dc.relation | UIDP/UIDB/04234/2020 | pt_PT |
| dc.relation | NORTE-01-0145-FEDER-028550 | pt_PT |
| dc.relation | Verification and Validation of Automated Systems' Safety and Security | |
| dc.rights.uri | http://creativecommons.org/licenses/by-nc/4.0/ | pt_PT |
| dc.subject | Verification | pt_PT |
| dc.subject | Variability | pt_PT |
| dc.subject | Railway | pt_PT |
| dc.subject | Real time Automata | pt_PT |
| dc.title | Verification of multiple models of a safetycritical motor controller in railway systems | pt_PT |
| dc.title.alternative | 220504 | pt_PT |
| dc.type | journal article | |
| dspace.entity.type | Publication | |
| oaire.awardTitle | Verification and Validation of Automated Systems' Safety and Security | |
| oaire.awardURI | info:eu-repo/grantAgreement/FCT/3599-PPCDT/ECSEL%2F0016%2F2019/PT | |
| oaire.awardURI | info:eu-repo/grantAgreement/EC/H2020/876852/EU | |
| oaire.fundingStream | 3599-PPCDT | |
| oaire.fundingStream | H2020 | |
| person.familyName | Proenca | |
| person.familyName | Pereira | |
| person.familyName | NANDI | |
| person.givenName | Jose | |
| person.givenName | David | |
| person.givenName | GIANN CARLOS | |
| person.identifier.ciencia-id | 2412-FE81-2767 | |
| person.identifier.ciencia-id | 0F12-0F3E-06E1 | |
| person.identifier.orcid | 0000-0003-0971-8919 | |
| person.identifier.orcid | 0000-0002-9851-0679 | |
| person.identifier.orcid | 0000-0002-3206-0599 | |
| person.identifier.rid | K-4256-2016 | |
| person.identifier.scopus-author-id | 24067286500 | |
| project.funder.identifier | http://doi.org/10.13039/501100001871 | |
| project.funder.identifier | http://doi.org/10.13039/501100008530 | |
| project.funder.name | Fundação para a Ciência e a Tecnologia | |
| project.funder.name | European Commission | |
| rcaap.rights | openAccess | pt_PT |
| rcaap.type | article | pt_PT |
| relation.isAuthorOfPublication | a9b67049-85ec-485a-a937-334ba113f087 | |
| relation.isAuthorOfPublication | f58e1e61-3caa-4e5a-ab19-31121d881779 | |
| relation.isAuthorOfPublication | aa673f73-38c8-4db5-8e80-f96582f1e18c | |
| relation.isAuthorOfPublication.latestForDiscovery | aa673f73-38c8-4db5-8e80-f96582f1e18c | |
| relation.isProjectOfPublication | 43bf0ece-7313-48dc-bc45-10ce83b59819 | |
| relation.isProjectOfPublication | 1b3082bd-64c8-41d8-9f32-bb7f4b0d7bde | |
| relation.isProjectOfPublication.latestForDiscovery | 43bf0ece-7313-48dc-bc45-10ce83b59819 |