Skip to main content

Student Projects

Student Projects General Information

The Group and its Working Environment

Operating Systems and Formal Methods

The projects advertised on these pages are set within the Trustworthy Systems research group at Data61, the largest and most active Operating Systems research group in the southern hemisphere and the Asia-Pacific region and one of the foremost in the world.

Our research activities extend from embedded systems via microkernels through virtualization to general issues of system architecture and system security. The group is also interested in the investigation of architectural support for operating systems and languages. The group is well networked internationally and has collaborations and exchanges of visits with many leading private- and public-sector systems research groups.

One key feature of our group is that formal methods and operating systems practitioners work closely together.

In 2016 we have six full time research staff, all conjoint Data61 and UNSW appointments, thirteen full or part-time engineering/support staff (research assistants and engineers, some PhD qualified), twelve PhD students, and a varying number of undergraduates and Masters of Engineering students.

We are well-equipped with state-of-the-art computing equipment, and have experience with a large range of computer architectures, from ARM to Itanium. The group is is home of the PLEB computer and other designs derived from it. Furthermore, we have modern testing and other lab equipment.

Trustworthy Systems research outcomes are being deployed in commercial products, and the group has a track record of getting Linux kernel patches accepted.

Systems

The project pages here refer to a number of systems we are working on. This is a short overview of them, with links to more information.

L4

... is an extremely small and high-performance operating system microkernel, under active development at Karlsruhe, Dresden and Data61. The TS group has in the past implemented the first 64-bit version (on MIPS, still holds the performance record for single-issue CPUs) and the first multiprocessor version (on Alpha) of this kernel. It is used as the basis of most of our embedded-systems work, and the Iguana and Mungi operating systems are based on it. A number of student projects use it, including Sunswift, the UNSW solar car, and BLUEsat, the UNSW student satellite project.

seL4

Most of our work now uses seL4, the local research kernel, or OKL4, the commercial (but open-source) L4 version marketed by spin-out Open Kernel Labs and based on TS research.

Linux

... needs no introduction. It is a second focus point of the group's research. Some successes include the design and implementation of fast context switching on the StrongARM processor (50 times faster than in standard Linux), and removal of the 2TB Filesystem limit.

 

Served by Apache on Linux on seL4.
Served by Apache on Linux on seL4.