CAmkES: Component Architecture for microkernel-based Embedded Systems

An example CAmkES system

Composing Embedded Systems Software

The CAmkES project provides a solution for quickly and reliably building complex microkernel-based embedded systems software.

  • Latest news:

  • Motivation: CAmkES is a platform that abstracts the low-level mechanisms of a microkernel, providing communication primitives and support for decomposition of a system into functional units. With this platform as a base, embedded systems software is designed as a set of protected and separated services that communicate with each other through highly efficient and secure interprocess communication mechanisms. Given that services are protected from each other by a combination of a proven kernel and hardware protection, resulting systems have the potential to be highly reliable and secure.

    The design of such a modular system becomes increasingly complicated as the number of services and degrees of interconnection grow. In addition to the platform itself, CAmkES provides a model and tools that reduce this complexity and make the design and implementation of large microkernel-based systems feasible.

  • Approach: Using a component-based software development approach to building microkernel-based embedded systems software, the system is modelled as a set of interacting software components. These software components have explicit interaction interfaces, and a system design details the connections between components. Furthermore, the components are designed in such a way as to be reusable in different systems and not to rely on the implementation specifics of the connection mechanisms. This enables more rapid development, portability and more manageable systems.

  • Challenges: Component-based development shifts the development emphasis from programming software to composing software systems. It brings with it obvious benefits for embedded systems such as reusability, maintainability, and a reduction of software complexity which leads to improved productivity. However, applying component-based development in the embedded domain also introduces several new concepts and challenges.

    • Resource-constrained environments;
    • Desirable flexibility for component design and implementation, through parameterisation and configuration;
    • Component reusability, exemplified by independence from their environment; and
    • Support for a variety of computational models (or architectural styles), including event-based models, dataflow models, etc.

Status

Current areas of active CAmkES research are the correctness of component systems and architectural-level system design.

We have an internal implementation of the CAmkES platform for seL4. This is our current research platform, supporting the above research.

The CAmkES technology has been licensed to Open Kernel Labs (Now General Dynamics Broadband) for integration into their products. The CAmkES framework for OKL4 has been released as open source. Please see our CAmkES software pages for more information and to download it.

Archived information about prior CAmkES research can be found here.

Further Documentation

Further information about the design and implementation of CAmkES can be found on the following pages:

Contact

Ihor Kuz, ihor.kuz<at>nicta.com.au

People

Current

Past

Publications

Abstract PDF Matthew Fernandez, Peter Gammie, June Andronick, Gerwin Klein and Ihor Kuz
CAmkES glue code semantics
Technical Report, NICTA and UNSW, November, 2013
Abstract
Slides
PDF Matthew Fernandez, Ihor Kuz, Gerwin Klein and June Andronick
Towards a verified component platform
Workshop on Programming Languages and Operating Systems (PLOS), pp. 6, Farmington, PA, USA, November, 2013
Abstract PDF Matthew Fernandez, Gerwin Klein, Ihor Kuz and Toby Murray
CAmkES formalisation of a component platform
Technical Report, NICTA and UNSW, November, 2013
Abstract PDF Matthew Fernandez, Ihor Kuz and Gerwin Klein
Formalisation of a component platform
Poster Presentation, Operating Systems Design and Implementation 2012, Hollywood, CA, USA, October, 2012.
Abstract PDF Nicholas FitzRoy-Dale
Architecture optimisation
PhD Thesis, UNSW, Sydney, Australia, March, 2011
Abstract PDF Nicholas FitzRoy-Dale and Ihor Kuz
Towards automatic performance optimisation of componentised systems
2nd Workshop on Isolation and Integration in Embedded Systems, Nuremberg, Germany, April, 2009
Abstract PDF 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, Volume 41, Number 4, pp. 3–11, July, 2007
Abstract PDF Ihor Kuz and Yan Liu
Extending the capabilities of component models for embedded systems
International Conference on the Quality of Software-Architectures (QoSA), Boston, MA, USA, July, 2007
Abstract link 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, Volume 80, Number 5, pp. 687–699, May, 2007
Preprint
Abstract PDF Nicholas FitzRoy-Dale
A declarative approach to extensible interface compilation
Proceedings of the 1st International Workshop on Microkernels for Embedded Systems (MIKES), Sydney, Australia, January, 2007

Served by Apache on Linux on seL4