Docker Public Model-2-Text Tools for Executable and Verifiable LLFSMs: The Microwave Example

This video shows how the model of the timer-driven microwave (as an arrangement of logic-labelled finite-state machines [LLFSMs]) is translated to executable code for LISP, for C and assembler (MIPS 32 bits). It also shows how it is translated for two model checkers (NuSMV and tlc), and properties are verified with LTL and CTL. Even real-time properties are checked, showing that opening the door causes the motor to stop within a time-bound.

Видео Docker Public Model-2-Text Tools for Executable and Verifiable LLFSMs: The Microwave Example автора Python практика