• ERTOS Home
•  
• News
• Events
  • 2008-12-01 WOSSA 2008
• Jobs
• Research
• People
• Publications
• Software
• Hardware
• Education
• Collaboration and Commercialisation
• Contact
• Search

Seminar day: The Future of Embedded Software

NICTA is organising a day full of exciting seminars to present the future of embedded software. The seminars cover major embedded software research projects and consist of presentations, discussions and partially demos.

You are cordially invited to attend the whole day or individual seminars. The seminars are open to the public.

Please RSVP for catering purposes with subject "RSVP seminar day" to Emilia.Sotirova [at] nicta.com.au

• Program
• Venue
• Abstracts and biographies

Program

Monday, April 16, 2007

Venue

Abstracts and Biographies

The Design and Implementation of a Formally Verifiable Microkernel

The secure embedded L4 project (seL4) aims to produce a precisely specified kernel programming interface and reference implementation of a secure embedded microkernel. Both the model of the kernel API and kernel reference implementation itself must be amenable to formal verification to reach the end goal of a fully formally verified microkernel.

This talk will examine some of the issues we encountered on the ongoing path to a formally verified microkernel, and our approaches to solving those issues. Some specific examples that will be discussed include our novel approach to providing an iterative development environment readily use-able to both kernel programmers and formal practitioners, and the kernel design decisions that ease the formal verification.

Bio:
Dr Kevin Elphinstone is a senior lecturer at the University of New South Wales, and a senior researcher with the NICTA Embedded, Real-Time, and Operating Systems program, where he leads the seL4 project. Past work includes time as a Research Associate at Karlsruhe University, Germany, and a Visiting Scientist at the IBM TJ Watson Research Center, NY. He holds a PhD in Computer Science from UNSW.

Verifying a High-Performance Micro-Kernel

This presentation will give an overview of the L4.verified project at NICTA. The aim of the project is to formally verify, in the theorem prover Isabelle/HOL, the functional correctness of the next L4 microkernel. The talk will give a high-level introduction to the abstract L4 specification, to a framework for formal refinement and invariant proofs on monadic functional programs, and to a framework for verifying low-level C programs with pointers in Hoare-Logic.

Bio:
Dr Gerwin Klein is a senior researcher with the NICTA Formal Methods program. He holds a PhD from Technische Universität München where he formally verified the the Java Bytecode Verifier. He is currently leading the L4.verified project at NICTA.

Real-Time Guarantees from the Ground Up

Along with the wave of embedded systems being swept into everyday life, ranging from mobile phone to cars, real-time systems become also more ubiquitous. An embedded system is labelled to be also a real-time system, when correctness of operation is not just defined by performing a given function, but also keeping the time needed to perform this function within specified limits.

In order to provide such guarantees the worst-case execution time of all parts of the system need to be known. Within the Potoroo project we aim to analyse the L4 microkernel with a measurement based approach. The approach is supported by static analysis and can be used beyond the real-time domain to provide directing input into optimisation of the code.

Bio:
In 1995 Stefan M. Petters received a Diplomingenieur degree (Master in Engineering equivalent) in Electrical Engineering and Information Technology from the corresponding faculty (EI) at the Technical University Munich (TUM), Germany. After this degree Stefan worked as a Research Assistant till early 1999 at the Institute for Real-Time Computer Systems at the TUM before moving up to a Lecturer equivalent position in the same institute. In 2002 Stefan was awarded a Dr.-Ing. degree from the Faculty of EI at TUM. Stefan had moved on earlier that year to work as Research Associate and Teaching Fellow within the Real-Time Group at the University of York, England. After almost 2.5 years, Stefan moved to work at NICTA within the ERTOS program in mid 2004. Stefan's main research interests are in real-time, with focus on temporal system analysis.

Component architecture for microkenrnel-based embedded systems

Component-based software engineering is well suited as a means of decreasing the complexity of developing microkernel-based embedded systems such as those currently being built on the L4 platform. This presentation will give an overview of the NICTA CAmkES (component architecture for microkernel-based embedded systems) project. The aim of the project is to investigate component-based development of embedded systems and to provide a flexible and lightweight component architecture for microkernel-based embedded systems. The talk will give an overview of the core CAmkES architecture, the principles underlying the architecture design, show how systems can be developed using this architecture, and provide a glimpse of the future directions that research in this project will take.

Bio:
Dr. Ihor Kuz is a researcher in NICTAs Embedded, Real-Time, and Operating Systems (ERTOS) program. He obtained his PhD from the Delft University of Technology in the Netherlands. His interests include operating systems for embedded systems, distributed systems, and component-based software engineering. He is currently leading the CAmkES project at NICTA.

Bug Busting: Let Goanna Get Rid of Your Software Bugs

Goanna is an automatic software code analysis tool that tackles the problems of software defect detection and security vulnerability prevention. Goanna is particularly suited for embedded system software development, helping to reduce testing costs, risks of product recalls, and to minimizing the time to market. In this talk we will present some of the automated technology that allows a fast and precise analysis and we will demonstrate some of its capabilities on real C/C++ code.

Bio:
Dr Ralf Huuck is a researcher within NICTA's Formal Method program and the leader of the Goanna project. He champions the idea of automated software verification technology, leading to higher software quality without putting additional burden on the software developer. Ralf obtained his PhD in the area of software verification for embedded systems at the University of Kiel, Germany, in 2003.