проект SLAM

Проект SLAM , начатый в 1999 году Томасом Боллом и Шрирамом Раджамани из Microsoft Research , был направлен на проверку свойств безопасности программного обеспечения с использованием методов проверки моделей . Он был реализован в OCaml и использовался для поиска множества ошибок в драйверах устройств Windows. Он распространяется как часть пакета разработки Microsoft Windows Driver Foundation под названием Static Driver Verifier (SDV). «Изначально SLAM был аббревиатурой, но мы сочли его слишком громоздким для объяснения. Теперь мы предпочитаем думать об «устранении» ошибок в программе». ^[1] Первоначально оно означало «программное обеспечение (спецификации), языки программирования, абстракцию и проверку моделей». ^[2] Обратите внимание, что с тех пор Microsoft повторно использовала SLAM для обозначения «мобильных аннотаций социального местоположения». ^[3]

См. также

Проверка модели абстракции
средство проверки модели BLAST , средство проверки модели, похожее на SLAM, которое использует «ленивую абстракцию».

Ссылки

^ Болл, Томас; Кук, Байрон; Левин, Владимир; и Раджамани, Шрирам К.; SLAM и средство проверки статических драйверов: передача технологий формальных методов внутри Microsoft ; Конспекты лекций по информатике (LNCS), Vol. 2999: Бойтен, Эрке А.; Деррик, Джон; и Смит, Грэм; ред.; Четвертая Международная конференция по интегрированным формальным методам (IFM 2004), 4–7 апреля 2004 г., Кентербери, Великобритания , Спрингер, Берлин/Гейдельберг, стр. 1–20.
^ Болл, Томас; Левин, Владимир; и Раджамани, Шрирам К.; Десятилетие проверки моделей программного обеспечения с помощью SLAM ; Сообщения ACM, Vol. 54(7), стр. 68–76 (июль 2011 г.)
^ Мондок, Мэтт; Microsoft Slam: оставайтесь на связи и преследуйте своих друзей ; Ars Technica, 10 октября 2006 г.