Show simple item record

dc.contributor.authorButterfield, Andrew
dc.contributor.editorJonathan P. Bowen, Qin Li, Qiwen Xu.en
dc.coverage.temporal978-3-031-40436-8en
dc.date.accessioned2023-10-10T11:19:12Z
dc.date.available2023-10-10T11:19:12Z
dc.date.created15/09/2023en
dc.date.issued2023
dc.date.submitted2023en
dc.identifier.citationAndrew Butterfield and Frédéric Tuong, Applying Formal Verification to an Open-Source Real-Time Operating System. In Jonathan P. Bowen, Qin Li, Qiwen Xu. (Eds.) Theories of Programming and Formal Methods, LNCS 14080, Shanghai, China, Springer Nature Switzerland, 2023, 348 - 366en
dc.identifier.otherY
dc.identifier.urihttp://hdl.handle.net/2262/104012
dc.description.abstractThis paper describes work done using formal methods to verify parts of the RTEMS real-time operating system, as part of an activity sponsored by the European Space Agency to qualify multi-core processors for spaceflight. A variety of formalisms were investigated, keeping in mind the need to be a good fit with the RTEMS community in general. The technique that was deployed used Promela to model aspects of the operating system behavior, and the SPIN model-checker to do test generation. This involved developing Promela models, which are formal artifacts, and then developing a simple machine-readable observation language that made it easy to connect model behavior to the generation of C test code. The observation language was then refined to code using a dictionary mapping observable elements to test code snippets. Neither the observable language of the dictionary mapping are formal, so this paper also explores how these might be given UTP semantics, and linked together, in which the research of He Jifeng plays a key role. It finishes defining a future research agenda that uses this work with a real-world application to drive the research.en
dc.format.extent348en
dc.format.extent366en
dc.language.isoenen
dc.publisherSpringer Nature Switzerlanden
dc.relation.ispartofseriesLNCS 14080;
dc.rightsYen
dc.subjectRTEMSen
dc.subjectReal-Time Operating Systemsen
dc.subjectTest Generationen
dc.subjectUnifying theories of programmingen
dc.subjectPromela/SPINen
dc.subjectModel checkingen
dc.titleApplying Formal Verification to an Open-Source Real-Time Operating Systemen
dc.title.alternativeTheories of Programming and Formal Methodsen
dc.typeConference Paperen
dc.type.supercollectionscholarly_publicationsen
dc.type.supercollectionrefereed_publicationsen
dc.identifier.peoplefinderurlhttp://people.tcd.ie/butrfeld
dc.identifier.rssinternalid259292
dc.identifier.doihttp://dx.doi.org/10.1007/978-3-031-40436-8_13
dc.rights.ecaccessrightsopenAccess
dc.description.technical978-3-031-40435-1en
dc.identifier.orcid_id0000-0002-2337-2101


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record