Мурφ

Мурφ
Разработчик(и)	Исследовательская группа Дэвида Дилла в Лаборатории компьютерных систем Стэнфордского университета
Стабильная версия	3.1 / ноябрь 1993 г .; 30 лет назад
Репозиторий	github .с / Тайлер-Юта /Мерфи2019
Написано в	ANSI С++
Операционная система	Линукс
Тип	Проверка модели
Лицензия	аналогично лицензии MIT
Веб-сайт	http://verify.stanford.edu/dill/murphi.html (через Wayback Machine)

Murφ (/ˈmɝ.fi/, также пишется Murphi ) — это средство проверки моделей с явным состоянием, разработанное в Стэнфордском университете и широко используемое для формальной проверки протоколов когерентности кэша.

История

Ранняя история Мурфи описана в статье Дэвида Дилла. ^{[ 1 ]} Первая версия Murφ была разработана в Стэнфордском университете в 1990 и 1991 годах профессором Дэвидом Диллом и его аспирантами Андреасом Дрекслером, Аланом Ху и Ханом Янгом и в основном реализована Андреасом Дрекслером. Язык спецификации был значительно изменен и расширен Дэвидом Диллом, Аланом Ху, К. Норрисом Ипом, Ральфом Мелтоном, Сынджуном Паком и Ханом Яном. Ральф Мелтон реализовал новую версию летом и осенью 1992 года. Сынджун Пак добавил проверку жизнеспособности и ограничения справедливости, но поскольку алгоритм проверки жизнеспособности противоречил важным оптимизациям, в частности уменьшению симметрии, проверка жизнеспособности была опущена в последующих выпусках. C. Norris Ip реализовал обратимые правила и конструкторы повторения (которые не включены в версию 3.1), а также добавил симметрию и сокращение мультимножеств (которые есть). Ульрих Штерн реализовал сжатие хеша, ^{[ 2 ]} улучшено использование диска и реализовано Parallel Murφ.

Последним выпуском Стэнфорда был выпуск 3.1 в ноябре 1993 года. множество производных версий Murφ С тех пор другими группами было создано .

Функции

Компилятор Murφ принимает модель, написанную на языке спецификации Murφ, и выводит код C++, который представляет собой верификатор этой модели. (То есть код C++ при выполнении выполняет проверку модели явного состояния для проекта, описанного в спецификации.) Язык спецификации Murφ использует защищенные команды и асинхронную модель чередования параллелизма, при этом вся синхронизация и обмен данными осуществляются через глобальные переменные. Верификатор проверяет свойства безопасности в форме инвариантов и внутренних утверждений, указанных в модели, а также проверяет наличие взаимоблокировок. Не проверяет живость свойств, хотя версия Murφ 2.7L поддерживала проверку набора общих свойств живучести LTL. Язык и верификатор поддерживают некоторые виды снижения симметрии. ^{[ 3 ]}

Первоначально Murφ применялся для проверки протоколов когерентности кэша . ^{[ 4 ]} но применялся и к другим проблемам, включая проверку протоколов безопасности .

Лицензирование

Лицензия Murφ аналогична лицензии MIT. Murφ можно использовать, копировать, изменять, продавать и распространять для любых целей при условии, что включены уведомление об авторских правах и лицензия, название Стэнфордского университета не используется для рекламы или рекламы без разрешения, а модифицированные версии не называются Murphi без разрешения. .

Производные

В Стэнфорде и других местах было создано множество производных версий Murφ, в том числе следующие:

См. также

Ссылки

^ Дилл, Дэвид Л. (2008). Грумберг, Орна; Вейт, Хельмут (ред.). 25 лет проверки моделей: история, достижения, перспективы . стр. 77–88.
^ Стерн, Ульрих; Дилл, Дэвид Л. (1996). Формальное описание методов IX . Бостон, Массачусетс: Спрингер. стр. 333–348.
^ Ип, К. Норрис; Дилл, Дэвид Л. (1993). «Эффективная проверка симметричных параллельных систем». Материалы Международной конференции IEEE по компьютерному дизайну ICCD'93 1993 года . IEEE. стр. 230–234. дои : 10.1109/ICCD.1993.393375 . ISBN 0-8186-4230-0 . S2CID 38444364 .
^ Дилл, Дэвид Л.; Дрекслер, Андреас Дж.; Ху, Алан Дж.; Ян, К. Хан (1992). «Верификация протокола как средство проектирования аппаратного обеспечения». Материалы Международной конференции IEEE 1992 года по компьютерному дизайну: СБИС в компьютерах и процессорах . ИИЭР: 552–525.

Внешние ссылки

[1] Дилл, Дэвид Л. (2008). Грумберг, Орна; Вейт, Хельмут (ред.). 25 лет проверки моделей: история, достижения, перспективы . стр. 77–88.

[2] Стерн, Ульрих; Дилл, Дэвид Л. (1996). Формальное описание методов IX . Бостон, Массачусетс: Спрингер. стр. 333–348.

[3] Ип, К. Норрис; Дилл, Дэвид Л. (1993). «Эффективная проверка симметричных параллельных систем». Материалы Международной конференции IEEE по компьютерному дизайну ICCD'93 1993 года . IEEE. стр. 230–234. дои : 10.1109/ICCD.1993.393375 . ISBN 0-8186-4230-0 . S2CID 38444364 .

[4] Дилл, Дэвид Л.; Дрекслер, Андреас Дж.; Ху, Алан Дж.; Ян, К. Хан (1992). «Верификация протокола как средство проектирования аппаратного обеспечения». Материалы Международной конференции IEEE 1992 года по компьютерному дизайну: СБИС в компьютерах и процессорах . ИИЭР: 552–525.

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]