ERTOS Publications, Theses and Technical Reports
- Publications from NICTA's ERTOS Group ( 2008, 2007, 2006, 2005, 2004, 2003 )
- Non-NICTA publications by the UNSW OS group ( 2008, 2006, 2005, 2004, 2003, 2002 )
- Selected undergraduate student theses
 | is the abstract of the paper |
 | is the paper in compressed PostScript (.ps.gz or .ps.Z) format |
 | is the paper in PDF format |
 | is a reference to locations, where we can not directly refer to the downloadable document. |
 | means that the paper is yet to be published |
ERTOS Publications
2008
2007
|
|
|
Gernot Heiser Your system is secure? Prove it! USENIX ;login:, 32(6), 35–38, (December, 2007) |
|
|
|
Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone Verified protection model of the seL4 microkernel Technical Report , NICTA, October, 2007 |
|
|
|
Leonid Ryzhyk, Ihor Kuz and Gernot Heiser Formalising device driver interfaces Proceedings of the 4th Workshop on Programming Languages and Operating Systems, Stevenson, Washington, USA, October, 2007 |
|
|
|
David C. Snowdon, Stefan M. Petters and Gernot Heiser Accurate On-line Prediction of Processor and Memory Energy Usage Under Voltage Scaling Proceedings of the 7th International Conference on Embedded Software, Salzburg, Austria, October, 2007 |
|
|
|
Luke Macpherson Performing under overload, PhD Thesis, University of NSW, Sydney 2052, Australia, 2007 |
|
|
|
Andrew Baumann Dynamic update for operating systems, PhD Thesis, University of NSW, Sydney 2052, Australia, 2007 |
|
|
|
Proceedings of the 2007 Workshop on Operating System Platforms for Embedded Real-Time Applications Technical Report , NICTA, July, 2007 Proceedings of the 2007 Workshop on Operating System Platforms for Embedded Real-Time Applications |
|
|
|
Kevin Elphinstone, David Greenaway and Sergio Ruocco Lazy scheduling and direct process switch — merit or myths? Proceedings of the 3rd Workshop on Operating System Platforms for Embedded Real-Time Applications, Pisa, Italy, July, 2007 Preliminary version |
|
|
|
Ansgar Fehnker, Ralf Huuck, Felix Rauch and Sean Seefried Analysing Embedded System Software Proceedings of C/C++ Verification Workshop, Oxford, UK, July, 2007 Extended abstract |
|
|
|
Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein and Stefan M. Petters Towards trustworthy computing systems: taking microkernels to the next level ACM Operating Systems Review, 41(4), 3–11, (July, 2007) |
|
|
|
Ihor Kuz and Yan Liu Extending the capabilities of component models for embedded systems Proceedings of the Third International Conference on the Quality of Software-Architectures (QoSA), Boston, MA, USA, July, 2007 |
|
|
|
Jia Meng, Lawrence C. Paulson and Gerwin Klein A termination checker for Isabelle Hoare logic 4th International Verification Workshop - VERIFY'07, Bremen, Germany, July, 2007 |
|
|
|
Stefan M. Petters, Patryk Zadarnowski and Gernot Heiser Measurements or static analysis or both? Proceedings of the 7th Workshop on Worst-Case Execution-Time Analysis, Pisa, Italy, July, 2007 |
|
|
|
David C. Snowdon, Godfrey van der Linden, Stefan M. Petters and Gernot Heiser Accurate run-time prediction of performance degradation under frequency scaling Proceedings of the 3rd Workshop on Operating System Platforms for Embedded Real-Time Applications, Pisa, Italy, July, 2007 |
|
|
|
Andrew Baumann, Jonathan Appavoo, Robert W. Wisniewski, Dilma Da Silva, Orran Krieger and Gernot Heiser Reboots are for hardware: challenges and solutions to updating an operating system on the fly Proceedings of the 2007 Annual USENIX Technical Conference, Santa Clara, CA, USA, June, 2007 |
|
|
|
Ansgar Fehnker, Ralf Huuck, Patrick Jayet, Michel Lussenburg and Felix Rauch Model Checking Software at Compile Time Proceedings of the 1st IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering, Shanghai, China, June, 2007 |
|
|
|
Leonid Ryzhyk, Timothy Bourke and Ihor Kuz Reliable device drivers require well-defined protocols Proceedings of the 3rd Workshop on Hot Topics in System Dependability, Edinburgh, UK, June, 2007 |
|
|
|
Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe and Gernot Heiser Towards a practical, verified kernel Proceedings of the 11th Workshop on Hot Topics in Operating Systems, San Diego, CA, USA, May, 2007 |
|
|
|
Gerwin Klein, Michael Norrish, Kevin Elphinstone and Gernot Heiser Verifying a high-performance micro-kernel 7th Annual High-Confidence Software and Systems Conference, Baltimore, MD, USA, May, 2007 |
|
|
|
Ihor Kuz, Yan Liu, Ian Gorton and Gernot Heiser CAmkES: a component model for secure microkernel-based embedded systems Journal of Systems and Software Special Edition on Component-Based Software Engineering of Trustworthy Embedded Systems, 80(5), 687–699, (May, 2007) Preprint |
|
|
|
Timothy Roscoe, Kevin Elphinstone and Gernot Heiser Hype and virtue Proceedings of the 11th Workshop on Hot Topics in Operating Systems, San Diego, CA, USA, May, 2007 |
|
|
|
Proceedings of the first international workshop on mikrokernels for embedded systems MIKES 2007 Technical Report , NICTA, March, 2007 |
|
|
|
Peter Chubb, Matthew Chapman and Myrto Zehnder [para]virtualisation without pain Proceedings of the 8th Linux.Conf.Au, Sydney, NSW, January, 2007 |
|
|
|
Dhammika Elkaduwe, Philip Derrin and Kevin Elphinstone A memory allocation model for an embedded microkernel Proceedings of the 1st International Workshop on Microkernels for Embedded Systems, Sydney, Australia, January, 2007 |
|
|
|
Nicholas FitzRoy-Dale A declarative approach to extensible interface compilation Proceedings of the 1st International Workshop on Microkernels for Embedded Systems, Sydney, Australia, January, 2007 |
|
|
|
Stefan M. Petters Execution-time profiles Technical Report , NICTA, January, 2007 |
|
|
|
Mohit Singal and Stefan M. Petters Issues in analysing L4 for its WCET Proceedings of the 1st International Workshop on Microkernels for Embedded Systems, Sydney, Australia, January, 2007 |
|
|
|
Harvey Tuch, Gerwin Klein and Michael Norrish Types, bytes, and separation logic Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Nice, France, January, 2007 |
|
|
|
Carl van Schaik and Gernot Heiser High-performance microkernels and virtualisation on ARM and segmented architectures Proceedings of the 1st International Workshop on Microkernels for Embedded Systems, Sydney, Australia, January, 2007 |
2006
|
|
|
Sergio Ruocco User-Level Fine-Grained Adaptive Real-Time Scheduling via Temporal Reflection Proceedings of the 27th IEEE Real-Time Systems Symposium, Rio De Janeiro, Brazil, December, 2006 |
|
|
|
Geoffrey Lee and Charles Gray L4/Darwin: evolving UNIX Conference for Unix, Linux and Open Source Professionals, Melbourne, Vic, Australia, October, 2006 Slides |
|
|
|
RTCSA 2006 WiP Proceedings Technical Report , NICTA, October, 2006 Work in Progress Proceedings of the 13th International Conference on Embedded and Real-Time Computing Systems and Applications RTCSA 2007 |
|
|
|
Philip Derrin, Kevin Elphinstone, Gerwin Klein, David Cock and Manuel M. T. Chakravarty Running the manual: an approach to high-assurance microkernel development Proceedings of the ACM SIGPLAN Haskell Workshop, Portland, OR, USA, September, 2006 |
|
|
|
Kevin Elphinstone, Gerwin Klein and Rafal Kolanski Formalising a high-performance microkernel Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 06), Seattle, USA, August, 2006 |
|
|
|
Ansgar Fehnker, Ralf Huuck, Patrick Jayet, Michel Lussenburg and Felix Rauch Goanna — A Static Model Checker Proceedings of the 11th International Workshop on Formal Methods for Industrial Critical Systems, Bonn, Germany, August, 2006 Published in Lecture Notes in Computer Science, Springer-Verlag (Vol. 4346). |
|
|
|
Stefan Schaefer, Bernhard Scholz, Stefan M. Petters and Gernot Heiser Static analysis support for measurement-based WCET analysis 12th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, Work-in-Progress Session, Sydney, Australia, August, 2006 |
|
|
|
Sergio Ruocco Real-Time Programming and L4 Microkernels Proceedings of the 2nd Workshop on Operating System Platforms for Embedded Real-Time Applications, Dresden, Germany, July, 2006 |
|
|
|
Daniel Potts and Ihor Kuz Adapting distributed shared memory applications in diverse environments Proceedings of the 6th International Symposium on Cluster Computing and the Grid, Singapore, May, 2006 |
|
|
|
Dhammika Elkaduwe, Philip Derrin and Kevin Elphinstone Kernel data – first class citizens of the system Proceedings of the 2nd International Workshop on Object Systems and Software Architectures , Victor Harbor, South Australia, Australia, January, 2006 |
|
|
|
Gernot Heiser, Volkmar Uhlig and Joshua LeVasseur Are virtual-machine monitors microkernels done right? ACM Operating Systems Review, 40(1), 95–99, (January, 2006) |
|
|
|
Rafal Kolanski and Gerwin Klein Formalising the L4 microkernel API Computing: The Australasian Theory Symposium (CATS 06), Hobart, Australia, January, 2006 |
|
|
|
Ben Leslie GrailOS: a micro-kernel based, multi-server, multi-personality operating system Proceedings of the 2nd International Workshop on Object Systems and Software Architectures , Victor Harbor, South Australia, Australia, January, 2006 |
|
|
|
Leonid Ryzhyk and Ihor Kuz Towards operating system support for application-specific fault-tolerance protocols Proceedings of the 2nd International Workshop on Object Systems and Software Architectures , Victor Harbor, South Australia, Australia, January, 2006 |
|
|
|
Simon Winwood, Gerwin Klein and Manuel Chakravarty On the synthesis of proof-carrying temporal reference monitors Proceedings of the 16th International Symposium on Logic-Based Program Synthesis and Transformation, Venice, Italy, 2006 |
2005
|
|
|
Gernot Heiser Secure embedded systems need microkernels USENIX ;login:, 30(6), 9–13, (December, 2005) |
|
|
|
Harvey Tuch and Gerwin Klein A unified memory model for pointers Proceedings of the 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Montego Bay, Jamaica, December, 2005 |
|
|
|
Kevin Elphinstone, Gernot Heiser, Ralf Huuck, Stefan M. Petters and Sergio Ruocco L4cars Embedded Security in Cars (escar 2005) Workshop, Cologne, Germany, November, 2005 |
|
|
|
Andrew Baumann and Jonathan Appavoo Improving dynamic update for operating systems Proceedings of the 20th ACM Symposium on Operating Systems Principles, Work-in-Progress Session, Brighton, UK, October, 2005 |
|
|
|
Joshua LeVasseur, Volkmar Uhlig, Matthew Chapman, Peter Chubb, Ben Leslie and Gernot Heiser Pre-virtualization: slashing the cost of virtualization Technical Report PA005520, NICTA, October, 2005 |
|
|
|
Felix Rauch Comprehensive Throughput Evaluation of LANs in Clusters of PCs with Switchbench — or How to Bring Your Switch to its Knees Proceedings of the IEEE International Symposium on Workload Characterization 2005, Austin, TX, USA, October, 2005 |
|
|
|
Ben Leslie, Peter Chubb, Nicholas Fitzroy-Dale, Stefan Götz, Charles Gray, Luke Macpherson, Daniel Potts, Yueting (Rita) Shen, Kevin Elphinstone and Gernot Heiser User-level device drivers: achieved performance Journal of Computer Science and Technology, 20(5), 654–664, (September, 2005) See TR PA005043 for a preprint |
|
|
|
David C. Snowdon, Sergio Ruocco and Gernot Heiser Power Management and Dynamic Voltage Scaling: Myths and Facts Proceedings of the 2005 Workshop on Power Aware Real-time Computing, New Jersey, USA, September, 2005 Preliminary workshop version |
|
|
|
Stefan M. Petters Deadline spanning: a graph based approach Embedded Real-Time Computing Systems and Applications (RTCSA 2005), Hong Kong, China, August, 2005 |
|
|
|
David Andrews, Iain Bate, Thomas Nolte, Clara Otero-Perez and Stefan M. Petters Impact of embedded systems evolution on RTOS use and design Proceedings of the 1st Workshop on Operating System Platforms for Embedded Real-Time Applications, Palma, Mallorca, Spain, July, 2005 |
|
|
|
Ben Leslie, Peter Chubb, Nicholas Fitzroy-Dale, Stefan Götz, Charles Gray, Luke Macpherson, Daniel Potts, Yueting (Rita) Shen, Kevin Elphinstone and Gernot Heiser User-level device drivers: achieved performance Technical Report PA005043, NICTA, July, 2005 |
|
|
|
David C. Snowdon, Stefan M. Petters and Gernot Heiser Power measurement as the basis for power management Proceedings of the 1st Workshop on Operating System Platforms for Embedded Real-Time Applications, Palma, Mallorca, Spain, July, 2005 |
|
|
|
Simon Winwood and Manuel Chakravarty Secure untrusted binaries — provably! 3rd International Workshop on Formal Aspect of Security and Trust, Newcastle upon Tyne, UK, July, 2005 |
|
|
|
Harvey Tuch, Gerwin Klein and Gernot Heiser OS verification — now! Proceedings of the 10th Workshop on Hot Topics in Operating Systems, Santa Fe, NM, USA, June, 2005 |
|
|
|
Andrew Baumann, Gernot Heiser, Jonathan Appavoo, Dilma Da Silva, Orran Krieger, Robert W. Wisniewski and Jeremy Kerr Providing dynamic update in an operating system Proceedings of the 2005 Annual USENIX Technical Conference, Anaheim, CA, USA, April, 2005 |
|
|
|
Andrew Baumann, Jeremy Kerr, Jonathan Appavoo, Dilma Da Silva, Orran Krieger and Robert W. Wisniewski Module hot-swapping for dynamic update and reconfiguration in K42 Proceedings of the 6th Linux.Conf.Au, Canberra, Australia, April, 2005 |
|
|
|
Matthew Chapman and Gernot Heiser Implementing transparent shared memory on clusters using virtual machines Proceedings of the 2005 Annual USENIX Technical Conference, Anaheim, CA, USA, April, 2005 |
|
|
|
Charles Gray, Matthew Chapman, Peter Chubb, David Mosberger-Tang and Gernot Heiser Itanium — a system implementor's tale Proceedings of the 2005 Annual USENIX Technical Conference, Anaheim, CA, USA, April, 2005 Best Student Paper Award! |
|
|
|
Ben Leslie, Carl van Schaik and Gernot Heiser Wombat: a portable user-mode Linux for embedded systems Proceedings of the 6th Linux.Conf.Au, Canberra, April, 2005 |
|
|
|
Felix Rauch and Thomas M. Stricker OS Support for a Commodity Database on PC Clusters — Distributed Devices vs. Distributed File Systems Proceedings of the 16th Australasian Database Conference, Newcastle, Australia, January, 2005 |
|
|
|
Rafal Kolanski A formal model of the L4 micro-kernel API using the B method Technical Report Technical Report 05-00029-1, National ICT Australia, 2005 |
2004
2003
Other technical reports of the School of Computer Science & Engineering.
Non-NICTA Publications
These publications are from NICTA-independent work of the UNSW OS group (DiSy) which is co-located with ERTOS. They include outcomes of ARC-funded projects and pre-NICTA work of the group.2008
2006
|
|
|
Myrto Zehnder and Peter Chubb Virtualising PCI Gelato ICE, Singapore, October, 2006 |
|
|
|
Shehjar Tikoo and Peter Chubb Improving NFS performance Gelato ICE conference, San Jose, CA, April, 2006 |
2005
|
|
|
Peter Chubb and Darren Williams Linux scalability — from the micro to the HUGE Proceedings of the 6th Linux.Conf.Au, Canberra, ACT, April, 2005 |