source: rtems-central/formal/promela/models/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: 1.6 KB
Line 
1# RTEMS Promela Models
2
3`formal/promela/models/'
4
5This directory contains formal models written in Promela to support test generation.
6
7## Contributors
8
9* Andrew Butterfield
10* Frédéric Tuong
11* Robert Jennings
12* Jerzy Jaśkuć
13* Eoin Lynch
14
15## License
16
17This project is licensed under the
18[BSD-2-Clause](https://spdx.org/licenses/BSD-2-Clause.html) or
19[CC-BY-SA-4.0](https://spdx.org/licenses/CC-BY-SA-4.0.html).
20
21## Models Overview
22
23There are currently five models present. Four are test-generation ready, whilst the fifth is still work in progress.
24
25We identify the usual RTEMS name for the component,
26the Promela "model-name", and the path to the model directory.
27
28* Barrier Manager: "barrier-mgr-model" `formal/promela/models/barriers`
29* Chains API:  "chains-api-model" `formal/promela/models/chains`
30* Event Manager "event-mgr-model" `formal/promela/models/events`
31* Message Manager "msg-mgr-model" `formal/promela/models/messages`
32* MrsP Thread Queues "mrsp-threadq-model" `formal/promela/models/threadq`
33
34## Doing Test Generation
35
36Ensure that the virtual environment defined in `formal/promela/src/env` is active.
37
38We shall assume that the alias `tb` has been defined as suggested in  `formal/promela/src/README.md`.
39
40Simply enter the relevant model sub-directory and invoke `tb` from the command line with desired command line arguments.
41
42A simple sequence that clears out all previously generated tests (from all models), clears all generated artifacts from this model,
43and then does the whole test generation process is:
44
45```
46tb zero
47tb clean
48tb all <model-name>
49```
50
51This will produce a test report in `<testsuite>-test.log`.
52
53
Note: See TracBrowser for help on using the repository browser.