Repository logo
 
Publication

Verification of multiple models of a safetycritical motor controller in railway systems

dc.contributor.authorProenca, José
dc.contributor.authorBorrami, Sina
dc.contributor.authorNova, Jorge Sanchez de
dc.contributor.authorPereira, David
dc.contributor.authorSpilere Nandi, Giann
dc.date.accessioned2022-06-22T15:13:46Z
dc.date.available2022-06-22T15:13:46Z
dc.date.issued2022-06-02
dc.description.abstractMotor 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.sponsorshipThis 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.versionN/Apt_PT
dc.identifier.urihttp://hdl.handle.net/10400.22/20635
dc.language.isoengpt_PT
dc.relationUIDP/UIDB/04234/2020pt_PT
dc.relationNORTE-01-0145-FEDER-028550pt_PT
dc.relationVerification and Validation of Automated Systems' Safety and Security
dc.rights.urihttp://creativecommons.org/licenses/by-nc/4.0/pt_PT
dc.subjectVerificationpt_PT
dc.subjectVariabilitypt_PT
dc.subjectRailwaypt_PT
dc.subjectReal time Automatapt_PT
dc.titleVerification of multiple models of a safetycritical motor controller in railway systemspt_PT
dc.title.alternative220504pt_PT
dc.typejournal article
dspace.entity.typePublication
oaire.awardTitleVerification and Validation of Automated Systems' Safety and Security
oaire.awardURIinfo:eu-repo/grantAgreement/FCT/3599-PPCDT/ECSEL%2F0016%2F2019/PT
oaire.awardURIinfo:eu-repo/grantAgreement/EC/H2020/876852/EU
oaire.fundingStream3599-PPCDT
oaire.fundingStreamH2020
person.familyNameProenca
person.familyNamePereira
person.familyNameNANDI
person.givenNameJose
person.givenNameDavid
person.givenNameGIANN CARLOS
person.identifier.ciencia-id2412-FE81-2767
person.identifier.ciencia-id0F12-0F3E-06E1
person.identifier.orcid0000-0003-0971-8919
person.identifier.orcid0000-0002-9851-0679
person.identifier.orcid0000-0002-3206-0599
person.identifier.ridK-4256-2016
person.identifier.scopus-author-id24067286500
project.funder.identifierhttp://doi.org/10.13039/501100001871
project.funder.identifierhttp://doi.org/10.13039/501100008530
project.funder.nameFundação para a Ciência e a Tecnologia
project.funder.nameEuropean Commission
rcaap.rightsopenAccesspt_PT
rcaap.typearticlept_PT
relation.isAuthorOfPublicationa9b67049-85ec-485a-a937-334ba113f087
relation.isAuthorOfPublicationf58e1e61-3caa-4e5a-ab19-31121d881779
relation.isAuthorOfPublicationaa673f73-38c8-4db5-8e80-f96582f1e18c
relation.isAuthorOfPublication.latestForDiscoveryaa673f73-38c8-4db5-8e80-f96582f1e18c
relation.isProjectOfPublication43bf0ece-7313-48dc-bc45-10ce83b59819
relation.isProjectOfPublication1b3082bd-64c8-41d8-9f32-bb7f4b0d7bde
relation.isProjectOfPublication.latestForDiscovery43bf0ece-7313-48dc-bc45-10ce83b59819

Files

Original bundle
Now showing 1 - 2 of 2
Loading...
Thumbnail Image
Name:
ART_CISTER_TR220504_2022.pdf
Size:
824.88 KB
Format:
Adobe Portable Document Format
No Thumbnail Available
Name:
license.txt
Size:
1.74 KB
Format:
Item-specific license agreed upon to submission