|
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 |
|