|
Dr. Andrew BUTTERFIELD
School of Computer Science and Statistics , Trinity College, the University of Dublin , Head of Foundations and Methods Group lero: the Irish Software Research Centre twitter: @AndrewButterfi9 github: andrewbutterfield bitbucket: andrewbutterfield |
|
RTEMS-SMP Qualification is an activity funded by the European Space Agency (ESA) to perform pre-qualification of an upcoming release of the open-source real-time operating system RTEMS (rtems.org). This release provides support for running RTEMS on multi-core systems. It follows on from previous work in this area funded by ESA.
Researchers from Lero, the Irish Software Research Centre are involved in a task that explores the use of formal verification techniques in this qualification process. The task is to deploy formal techniques such as formal modelling, model-checking, and theorem proving, to assist in improving the quality of qualification results in key areas.
Key areas under consideration include: modelling and verifying the multicore scheduling algorithms MrsP and OMIP and key synchronisation primitives; exploring how formal methods can help with test generation, and particularly for assembly code, with coverage analysis; and probabilistic reasoning to work around testing difficulties due to lack of predictability inherent in multi-core systems.
This will require the development and revision of requirements for these algorithms, development of formal models for appropriate formal tools and ways to automate, as far as is practical, the running of those tools.
Two key challenges are: to produce outputs that are suitable for software qualification; while doing this in a way that is acceptable to the open-source community (rtems.org) that maintains the operating system.
The activity is being run by a consortium led by Thales Edisoft (Portugal), with partners Embedded Brains (Germany), Jena Optronik (Germany), CISTER Research Centre, ISEP (Portugal), and Trinity College Dublin (Ireland) as part of Lero, the Irish Software Research Centre.
The ideal candidate will have a PhD in software verification with PhD and postdoctoral experience of a number of the following: formal verification tools used in industry such as Promela/SPIN,TLA+, Frama-C; formal models of concurrency; weak memory models; probabilistic modelling; refactoring code to minimise false positives from static analysis tools; software certification and qualification processes; real-time operating systems; and related topics.
As soon as possible, hoping for October start, 15-18months duration.
The position is based at Trinity College Dublin, Ireland and the research fellow will become of a member of Lero - the Irish Software Research Centre. It will also involve travel to some of the partners, as well as the European Space Research and Technology Centre (ESTEC).