Linux Kernel Verification
Supported by ARO (Army Research Office)
Robert P. Cook, Georgia Southern
 


 

Last updated: Apr 6, 04

The effective development of embedded systems requires a collection of tools to capture requirements, to construct, analyze and simulate specifications, to generate and test implementations, and to monitor and check implementations at run-time. 

The goal of the proposed research is to develop a framework for the integrated use of a suite of methods and tools for the specification, analysis, development, testing, prototyping, simulation and monitoring of embedded software. The framework will be based on systems that the investigators have been studying separately for some time and can also include systems that are developed elsewhere. The primary methods of interest are: formal specifications, test generation from specifications, automated verification, prototyping and simulation, and run-time monitoring and checking.

Examples

kernel/fork.c -- method to allocate unique process ids Click here

Software

Platform-independent POSIX Threads Library

Click here
OpenMP implemented using POSIX Threads Click here

Presentations and Papers

ARO HCES Workshops

Click here

Prototyping Tools

Phoenix experimental Unix, concurrent programming library, discrete-event simulation library Click here

Verification Tools

SPIN/Promela by G.J. Holzmann for formal verification of distributed algorithms Click here
On-line SPIN verifier Click here