CAmkES: Component Architecture for microkernel-based Embedded Systems

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

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

The CAmkES platform for seL4 has been released as open source (under a BSD license). It is available as part of the seL4 open source release and is hosted on GitHub.

Current areas of active CAmkES research include:

Development of trustworthy component-based systems
Generation of verified CAmkES glue code
Architectural-level system design

Further Documentation

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

CAmkES design
CAmkES Tutorial
CAmkES manual (including information about modifying CAmkES itself and some information about its internals)

People

Past

Adrian Danis
Alyssa Besseling
Andrew Baumann
Andri Toggenburger
Gernot Heiser
Ihor Kuz
Justin King Lacroix
Leonid Ryzhyk
Matthew Fernandez
Nicholas Fitzroy-Dale
Sarika Gupta
Sergio Ruocco
Siwei Zhuang
Steve Xie
Ted Wong
Yan Liu

Publications

		Gernot Heiser, Gerwin Klein and June Andronick seL4 in Australia: From research to real-world trustworthy systems Communications of the ACM, Volume 63, Issue 4, pp. 72-75, April, 2020
		Gerwin Klein, June Andronick, Ihor Kuz, Toby Murray, Gernot Heiser and Matthew Fernandez Formally verified software in the real world Communications of the ACM, Volume 61, Issue 10, pp. 68-77, October, 2018
		Matthew Fernandez Formal verification of a component platform PhD Thesis, School of Computer Science and Engineering, UNSW, Sydney, Australia, Sydney, Australia, July, 2016
		Matthew Fernandez, Peter Gammie, June Andronick, Gerwin Klein and Ihor Kuz CAmkES glue code semantics Technical Report, NICTA and UNSW, November, 2013
		Matthew Fernandez, Ihor Kuz, Gerwin Klein and June Andronick Towards a verified component platform Workshop on Programming Languages and Operating Systems (PLOS), pp. 1–7, Farmington, PA, USA, November, 2013
		Matthew Fernandez, Gerwin Klein, Ihor Kuz and Toby Murray CAmkES formalisation of a component platform Technical Report, NICTA and UNSW, November, 2013
		Matthew Fernandez, Ihor Kuz and Gerwin Klein Formalisation of a component platform Poster presented at Operating Systems Design and Implementation 2012, October, 2012
		Nicholas FitzRoy-Dale Architecture optimisation PhD Thesis, UNSW, Sydney, Australia, March, 2011
		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, December, 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, Volume 80, Number 5, pp. 687–699, May, 2007 Preprint
		Nicholas FitzRoy-Dale A declarative approach to extensible interface compilation International Workshop on Microkernels for Embedded Systems, Sydney, Australia, January, 2007

Trustworthy Systems