University of Cambridge > Talks.cam > Microsoft Research Cambridge, public talks > Michael Weber, University of Twente; Microsoft Research Lectures

Michael Weber, University of Twente; Microsoft Research Lectures

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

Abstract: Embedded systems are ubiquitous in everyday appliances, ranging from washing machines to cars. We present a verification approach for the (often safety-critical) software used in such systems. Embedded systems software is commonly written for specific micro- controller hardware, in a mixture of C with non-standard compiler extensions and assembler. A model checking tool for such software must support features like direct memory accesses, interrupt handling, inline assembler instructions, usage of timers, communication interfaces, etc. In our approach, we first compile a C program to its binary representation with an unmodified standard compiler, disassemble the resulting binary and feed it into our model checking framework. This has the additional benefit of the model checker verifying what is actually executed on the micro-controller and thus may even catch errors introduced during compilation, e.g. in one of the compiler`s optimization passes. We show examples of non- trivial errors that can be found with this approach, and also reflect on its scalability.

This talk is part of the Microsoft Research Cambridge, public talks series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2019 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity