|
|
|
|
|
|
by jonjacky
196 days ago
|
|
|
A surprise, from the README: "HiRTOS is formally specified using the Z notation. The Z specification can be found here [link]." I used Z years ago. I haven't seen any new work in Z for many years -- but the linked specification is dated in 2024. Also, "The HiRTOS thread scheduler is formally specified in TLA+/Pluscal. The TLA+/Pluscal specification can be found here [link] It was model-checked using the TLC model checker. The sucessful TLC run [link] took more than 7 hours" |
|
|