SEWORLD Archives

SEWORLD

SEWORLD@LISTSERV.ACM.ORG

Options: Use Forum View

Use Monospaced Font
Show Text Part by Default
Show All Mail Headers

Message: [<< First] [< Prev] [Next >] [Last >>]
Topic: [<< First] [< Prev] [Next >] [Last >>]
Author: [<< First] [< Prev] [Next >] [Last >>]

Print Reply
Subject: FormalRTEMS - Postdoc in formal verification of real-time OS
From: SEWORLD Moderator <[log in to unmask]>
Reply-To:SEWORLD Moderator <[log in to unmask]>
Date:Wed, 4 Sep 2019 17:14:27 -0000
Content-Type:text/plain

The School of Computer Science and Statistics in Trinity College Dublin is
seeking a post-doctoral Research Fellow in the field of formal software
verification, for a duration of 15-18 months, to start as soon as possible.
Salary range €40k-€51.5k p.a., depending on experience and precise duration.

RTEMS-SMP Qualification is an activity funded by the European Space Agency 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.

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 model-checking and
possibly 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 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.

The position is based at Trinity College Dublin, Ireland (http://www.tcd.ie) and
the research fellow will become of a member of Lero - the Irish Software
Research Centre (http://lero.ie). It will also involve travel to some of the
partners, as well as the the European Space Research and Technology Centre
(ESTEC). 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.

Further details, including how to apply, can be obtained from
https://www.scss.tcd.ie/Andrew.Butterfield/recruitment/ESA-RTEMS-SMP-Task-3.html
which will be regularly updated, or via twitter hashtag #FormalRTEMS.

Application deadline, 12noon, Irish Standard Time, Wednesday, 18th September.

--------------------------------------------------------------------
Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
Lero@TCD, Head of Foundations & Methods Research Group
School of Computer Science and Statistics,
Room G.39, O'Reilly Institute, Trinity College, University of Dublin
                        http://www.scss.tcd.ie/Andrew.Butterfield/
--------------------------------------------------------------------
--------------------------------------------------------------------
Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
Lero@TCD, Head of Foundations & Methods Research Group
School of Computer Science and Statistics,
Room G.39, O'Reilly Institute, Trinity College, University of Dublin
                         http://www.scss.tcd.ie/Andrew.Butterfield/
--------------------------------------------------------------------

============================================================
To contribute to SEWORLD, send your submission to
mailto:[log in to unmask]

http://sigsoft.org/resources/seworld.html provides more
information on SEWORLD as well as links to a complete
archive of messages posted to the list.
============================================================

ATOM RSS1 RSS2