dc.contributor.author | Butterfield, Andrew | |
dc.contributor.editor | Jonathan P. Bowen, Qin Li, Qiwen Xu. | en |
dc.coverage.temporal | 978-3-031-40436-8 | en |
dc.date.accessioned | 2023-10-10T11:19:12Z | |
dc.date.available | 2023-10-10T11:19:12Z | |
dc.date.created | 15/09/2023 | en |
dc.date.issued | 2023 | |
dc.date.submitted | 2023 | en |
dc.identifier.citation | Andrew 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 - 366 | en |
dc.identifier.other | Y | |
dc.description.abstract | This 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.extent | 348 | en |
dc.format.extent | 366 | en |
dc.language.iso | en | en |
dc.publisher | Springer Nature Switzerland | en |
dc.relation.ispartofseries | LNCS 14080; | |
dc.rights | Y | en |
dc.subject | RTEMS | en |
dc.subject | Real-Time Operating Systems | en |
dc.subject | Test Generation | en |
dc.subject | Unifying theories of programming | en |
dc.subject | Promela/SPIN | en |
dc.subject | Model checking | en |
dc.title | Applying Formal Verification to an Open-Source Real-Time Operating System | en |
dc.title.alternative | Theories of Programming and Formal Methods | en |
dc.type | Conference Paper | en |
dc.type.supercollection | scholarly_publications | en |
dc.type.supercollection | refereed_publications | en |
dc.identifier.peoplefinderurl | http://people.tcd.ie/butrfeld | |
dc.identifier.rssinternalid | 259292 | |
dc.identifier.doi | http://dx.doi.org/10.1007/978-3-031-40436-8_13 | |
dc.rights.ecaccessrights | openAccess | |
dc.description.technical | 978-3-031-40435-1 | en |
dc.identifier.orcid_id | 0000-0002-2337-2101 | |
dc.identifier.uri | http://hdl.handle.net/2262/104012 | |