Spin - формальная проверка

Question

Spin - формальная проверка

Имеет ли кто-нибудь контакт с проверкой модели с помощью этого инструмента SPIN, даже больше любой информации о проверке модели (параллельные программы)

4

model-checking spin

Источник

user265519 17 май '11 в 23:34

1 ответ

Решение

Другие вопросы по тегам model-checking spin

user290516 20 июл '11 в 16:10 2011-07-20 16:10 · Accepted Answer · 2011-07-20 16:10

Да, SPIN - очень хорошая модель проверки, но мне интересно, что вы хотите? Вы просто хотите услышать, что да, я слышал и играл с SPIN, или вам нужны предложения, как смоделировать проверку исходного кода?

Например, если вы программист на C, попробуйте ESBMC, напишите небольшую программу и запустите на ней ESBMC.

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