Viðburðir eftir árum

ICE-TCS seminar: Formal Methods for Modelling and Analysis of Single-Event Upsets

  • 11.9.2015, 14:00 - 15:00


Date/Time: Friday, 11 September 2015 at 2pm
Place: Room M.102
Speaker: Mads Chr. Olesen (Aalborg University, Denmark)
Title: Formal Methods for Modelling and Analysis of Single-Event Upsets

Abstract: When a high-energy particle such as a proton strikes a CPU, the impact may result in the corruption of a data register on the CPU.

Such a single-event upset (SEU), in which a random bit is flipped in the content of a data register, can lead to critical errors in the execution of a program. This is particularly problematic for security- or safety-critical systems where such errors may have grave consequences.

In this paper we develop a formal semantic framework for easy formal modelling of a large variety of SEUs in a core assembly language capturing the essential features of the ARM assembly language.

We use this framework to formally prove the soundness of a static analysis enforcing so-called blue/green separation in a given program.

Blue/green separation is a replication based technique for making a program fault-tolerant with respect to data-flow SEUs; however, full coverage requires special hardware support. We further use our semantic framework for deriving program fragments, so-called gadgets, for partial blue/green separation without special hardware. Finally, we illustrate how to apply statistical model checking in our framework to model and quantify faults that go well beyond data-flow SEUs and can provide statistics on the level of fault-tolerance of a program. We use this to provide evidence that our suggested program modifications significantly decrease the probability of such errors going undetected.

(Joint work with: René Rydhof Hansen, Kim Guldstrand Larsen and Erik Ramsgaard Wognsen)

Vinsamlegast athugið að á viðburðum Háskólans í Reykjavík (HR) eru teknar ljósmyndir og myndbönd sem notuð eru í markaðsstarfi HR. Hægt er að nálgast frekari upplýsingar á eða með því að senda tölvupóst á netfangið:
Please note that at events hosted at Reykjavik University (RU), photographs and videos are taken which might be used for RU marketing purposes. Read more about this on our or send an e-mail: