Да, SPIN - очень хорошая модель для проверки, но мне интересно, что вы хотите?Вы просто хотите услышать, что да, я слышал и играл с SPIN, или вы хотите узнать, как смоделировать проверку исходного кода?
Например, если вы программист на C, возьмите в свои руки ESBMC , напишите небольшую программу и запустите на ней ESBMC.
Это должно помочь вам понять, что можно сделать и как это сделать.Кстати, для начала Model Checking - это не статический анализ.Это на самом деле гораздо мощнее.Это антистатический анализ.Проверка модели на самом деле «в (очень узком) смысле» имитирует вашу программу и находит ситуации (комбинации аргументов, исключительные ситуации, пограничные случаи), в которых она действительно потерпит неудачу.