Subscribe: Contact: Sitemap: Printer Friendly
Subscribe to our RSS feed
Home >  Research >  Software Systems  > About Us  > Vision

About the Software Systems Research Group SSRG@NICTA

Vision

We will change the practice of design and implementation of software systems, by enabling affordable, routine design and implementation of large and complex software, with strong whole-of-system guarantees for safety- or security-critical systems and integrated, adaptive architectures that directly address business needs for enterprise ecosystems.

The strong trend towards more complexity and at the same time more reliance on software systems is unbroken and accelerating. In the embedded space, this leads to immediate safety and security concerns. In the enterprise space, the need for integration, adaptability, and business platforms is already a major factor for business impact. Mobile devices with security requirements and enterprise applications with evolving adaptation needs are connecting both problem spaces and further compound the problem. Over the whole spectrum there is a strong need to develop and deploy trustworthy software quickly and cost effectively.

NICTA's Software Systems Research Group (SSRG) aims to achieve fundamental, game-changing improvements in the design, implementation, and verification of software systems scaling from the embedded to the enterprise space. We will apply rigorous techniques at various abstraction levels of software systems, to achieve solid and practically meaningful guarantees, ranging from provable security, safety, and reliability properties of critical systems, to integrated and adaptive architectures that predictably meet performance and business objectives in real-word enterprise environments.

In the safety- and security-critical area, we build on our widely deployed kernel technology and systems research, and proven world-class expertise in applied formal methods, illustrated by the seL4 microkernel and its formal proof of correctness (see ERTOS and L4.verified). In the enterprise space, we build on our successful enterprise architecture services engagements, and on our expertise in software process engineering, business-rule modelling and software architectures to help developers build systems that address the right business needs and have real-world impact (see Business Adaptation and Interoperation).

Research Training

The SSRG team strongly believes in a tight integration of research and education, and consequently has a strategic education agenda, aimed at producing graduates with world-class knowledge and skills in our research areas. These graduates power our own research, spread skills to Australian industry, and enhance NICTA's and UNSW's reputation when taking jobs overseas.

Achievements

Past achievements of the SSRG team include:

  • World's first formal proof of functional correctness of a complete, general-purpose operating-system kernel;
  • First-ever sound and complete timing analysis of a protected multi-tasking operating system kernel
  • Two papers accepted to SOSP'09 (including a best-paper award). These are the first papers from Australia in the 42-year history of the top OS conference;
  • Machine-checked proof of security and isolation properties of the access control model of the capability-based operating system seL4;
  • Design and implementation of a high-performance capability-based secure microkernel (seL4) that integrates kernel and user resources in the same protection and management framework;
  • The automatic generation of well-performing device drivers from formal specifications (Termite);
  • A new approach to the design of device drivers which eliminates the majority of typical driver bugs by construction (Dingo);
  • A comprehensive approach to accurate energy management via dynamic voltage and frequency scaling that does not rely on pre-characterisation or inaccurate models of the hardware (Koala);
  • Highest message-passing performance ever reported on a number of architectures.
  • A review of the impact of process simulation research upon software systems published at ACM Impact Project workshop.
  • The Lending Industry XML Initiative (LIXI) developed and released industry-wide reference business processes, architectures and implementations for lending transactions to more than 100 Australian financial firms.
  • Contributed to ISO/IEC/IEEE 42010 Systems and software engineering Architecture description standard.
  • Our Empirical Software Engineering team named one of the three top research groups in the field in Communications of the ACM
  • Our spinout company Open Kernel Labs has deployed OKL4, its descendant of our L4-embedded microkernel, in more than a billion mobile phones.

Formal awards:

  • October 2011: Goanna was evaluated as the leading static analysis tools detecting more than twice as many serious bugs as the next best published competitor. Report on the Third Static Analysis Tool Exposition (SATE 2010), NIST Special Publication 500-283, Oct 2011
  • September 2011: Best Paper Award at ESEM'11 for An Empirical Investigation of Systematic Reviews in Software Engineering.
  • August 2011: June Andronick wins the MIT TR-35 for the 35 young innovators under 35 who are tackling important problems in transformative ways.
  • April 2011: The verified seL4 kernel makes the MIT TR-10, the world's top ten emerging technologies in 2011.
  • Aug 2010: Innovation Hero Award by Sydney University's Warren Centre for Advanced Engineering for Gernot Heiser
  • Feb 2010: NICTA's Richard A Newton Impact Award for Research Excellence to the seL4 and L4.verified team for the formal verification of the seL4 microkernel.
  • April 2010: Best Paper Award at ASWEC'10 for A Statistical Method for Middleware System Architecture Evaluation
  • October 2009: Best-Paper Award at SOSP'09 for seL4: Formal verification of an OS kernel
  • September 2009: Gernot Heiser wins the Engineering, Mathematics and Computer Sciences Category of the NSW Scientist of the Year 2009 Award
  • August 2008: ACSAC'08 Best Paper Award for Pre-virtualization: Soft layering for virtual machines
  • May 2008: NICTA's Richard A Newton Impact Award for Research Excellence to Gernot Heiser for research leading to the creation of Open Kernel Labs
  • December 2007: Best Paper Award at APSEC'07 for Optimising Project Feature Weights for Analogy-based Software Cost Estimation using the Mantel Correlation
  • November 2007: CISRA Award for best research paper to ERTOS PhD student Harvey Tuch
  • May 2007: iAward, Category Applications and Infrastructure Tools to Gernot Heiser by the Australian Information Industry Association (AIIA)
  • April 2007: Most Influential Paper Award at ASWEC 2007 for the ASWEC 1997 paper Validating the defect detection performance advantage of group designs for software reviews: report of a replicated experiment
  • September 2006: Best Paper Award at ISESE'06 for An Evaluation of Proposed Guidelines for Reporting Software Engineering Experiments
  • November 2005: Best Paper Award at WICSA'05 for Customized Benchmark Generation Using MDA
  • April 2005: USENIX'05 Best Student-Paper Award for Itanium—a system implementor's tale

Contacts

On the SSRG contacts page.

Served by Apache on Linux on seL4