Terms¶
TERM |
DESCRIPTION |
FURTHER |
|---|---|---|
badge |
An seL4/CamkES concept to assign IDs to communication endpoints, which can’t be manipulated and thus are sufficient to identify a caller. |
|
CMake |
Open-source, cross-platform family of tools designed to build, test and package software |
|
component |
A type of functional entity. It is important to stress this distinction. ‘Component’ is used colloquially to refer to both types and instances, but in a formal sense ‘component’ refers only to the type. To make this more concrete, the statement component foo f describes a component instance f, whose type is foo. |
|
connector |
A type of link between instances. The distinction between ‘connector’ and ‘connection’ is the same as that between ‘component’ and ‘instance,’ i.e. a connection is an instantiation of a particular connector. |
|
dataport |
Port interfaces that are used by a component. A component’s dataports are expected to be available to it at runtime as shared memory regions. |
|
ninja |
Small build system with a focus on speed. It differs from other build systems in two major respects: it is designed to have its input files generated by a higher-level build system, and it is designed to run builds as fast as possible. |
|
QEMU |
Hosted virtual machine monitor: it emulates the machine’s processor through dynamic binary translation and provides a set of different hardware and device models for the machine, enabling it to run a variety of guest operating systems. |
|
seL4 |
High-assurance, high-performance operating system microkernel. It is unique because of its comprehensive formal verification, without compromising performance. |