source: rtems-central/formal/README.md @ 3f4d9a4

Last change on this file since 3f4d9a4 was 3f4d9a4, checked in by Andrew Butterfield <Andrew.Butterfield@…>, on 01/10/23 at 19:44:42

top level FV hierarchy

  • Property mode set to 100644
File size: 801 bytes
Line 
1# Formal Verification
2
3`formal`
4
5This directory contains the models and tooling developed as part of the ESA-sponsored activity ***Qualification of RTEMS Symmetric Multiprocessing (SMP)***, that has been added into RTEMS in the `rtems-central` repository.
6
7## Contributors
8
9* Andrew Butterfield
10* Frédéric Tuong
11* Robert Jennings
12* Jerzy Jaśkuć
13* Eoin Lynch
14* James Gooding Hunt
15
16## License
17
18This project is licensed under the
19[BSD-2-Clause](https://spdx.org/licenses/BSD-2-Clause.html) or
20[CC-BY-SA-4.0](https://spdx.org/licenses/CC-BY-SA-4.0.html).
21
22## Overview
23
24At present, the only formal verification in play here is the use of Promela to build formal models of key RTEMS components, and the SPIN model-checker to perform C test generation.
25
26This can be found in the `promela` sub-directory
27
Note: See TracBrowser for help on using the repository browser.