Overview

VAMOS is a microkernel developed and verified in the context of the German research projects Verisoft and VerisoftXT. The same context also developed and verified the Verified Architecture Microprocessor (VAMP). The Verisoft project aimed at pervasive formal verification of computer systems from application software down to silicon-level hardware design. [VAMOS development context]

Role in the Verisoft architecture

Within the Verisoft architecture, VAMOS is part of the System Software Layer. The architecture described in the evidence includes application software, system software, tools, and hardware layers, with VAMOS positioned as the microkernel in the system-software stack. [VAMOS in Verisoft architecture]

The application-software layer includes foundational proofs for a verification approach to system-level concurrent programs that run as user processes on VAMOS. [User processes on VAMOS]

Services

The evidence identifies VAMOS as providing infrastructure for several system-software functions that require verification:

• memory virtualization;
• communication with hardware devices;
• processes, represented as sequences of assembly instructions;
• inter-process communication (IPC) via synchronous message passing. [VAMOS services]

Verification context

VAMOS appears in a broader verified-system setting that also includes the VAMP processor and its assembly-level instruction-set model, VAMPasm. The cited case study focuses on test generation for VAMP, but it describes VAMOS as part of the same formally verified Verisoft system stack. [VAMOS and VAMP context]