|
|
Главная / Верификация
(версия для печати)
Верификация
Книги Андрея Миронова Миронов А.М. Машинное обучение. Часть 1 (PDF)
 Миронов А.М. Верификация программ методом Model Checking (внешняя ссылка: intsys.msu.ru)
Миронов А.М. Теория процессов (PDF)
Миронов А.М. Теория функциональных программ. Часть 1 (PDF)
Миронов А.М., Френкель С.Л. Метод редукции вероятностных систем переходов (PDF)
Миронов А.М. Верификация программ. Часть 1: нерекурсивные программы. (PDF)
Разное Теория процессов и верификация программ - А.М. Миронов (лекции, осень 2017, мехмат МГУ) (внешняя ссылка: www.youtube.com)
Model checking и верификация программ - А.М. Миронов (лекции, весна 2018, мехмат МГУ) (внешняя ссылка: www.youtube.com)
Курс лекций "Математическая теория программирования", который осенью 2018 года прочел доцент мехмата МГУ Андрей Миронов (внешняя ссылка: www.youtube.com)
Во второй лекции курса он на засечке 13:30 неожиданно хвалит меня, а также высокий уровень энергетики, который почувствовал, побывав у нас. (внешняя ссылка: www.youtube.com)
Спецкурс Математическая теория программирования 7.09.18, часть 2 - А.М. Миронов (внешняя ссылка: www.youtube.com)
Лифшиц Ю. Верификация программ и темпоральные логики. Лекция №3 курса «Современные задачи теоретической информатики» (внешняя ссылка: download.yandex.ru)
Верификация программ и темпоральные логики — конспект лекции (внешняя ссылка: download.yandex.ru)
Лифшиц Ю. Символьная верификация программ. Лекция №4 курса «Современные задачи теоретической информатики» (внешняя ссылка: download.yandex.ru)
Символьная верификация программ — конспект лекции (внешняя ссылка: download.yandex.ru)
Виноградов Р.А., Кузьмин Е.В., Соколов В.А. Верификация автоматных программ средствами CPN/Tools (PDF)
Кузьмин Е.В. Иерархическая модель автоматных программ (PDF)
Васильева К.А., Кузьмин Е.В. Верификация автоматных программ с использованием LTL (PDF)
Кузьмин Е.В., Соколов В.А. О дисциплине специализации «Верификация программ» (PDF)
Кузьмин Е.В., Соколов В.А. О верификации «автоматных» программ (PDF)
Model checking (внешняя ссылка: en.wikipedia.org)
NASA: миссия надежна (внешняя ссылка: www.osp.ru)
Верификация автоматных программ (внешняя ссылка: go4it.unitesk.ru)
Задача валидации и верификации как стандартов IPv6, так и их реализаций, является чрезвычайно актуальной. Международный проект GO4IT. (внешняя ссылка: go4it.unitesk.ru)
Temporal Logic (внешняя ссылка: en.wikipedia.org)
Вельдер С.Э., Шалыто А.А. О верификации простых автоматных программ на основе метода Model Checking (PDF)
The Model Checker Spin (внешняя ссылка: spinroot.com)
Gerard J. Holzmann (внешняя ссылка: www.spinroot.com)
Вудкок Дж. Первые шаги к решению проблемы верификации программ (внешняя ссылка: www.osp.ru)
Джексон Д. Программы проверяют программы (PDF)
Кузьмин Е.В., Соколов В.А. О некоторых подходах к верификации автоматных программ (PDF)
Свидетельство об официальной регистрации программы для ЭВМ "Система моделирования и анализа автоматных программ" (PDF)
 Кларк Э., Грамберг О., Пелед Д. Верификация моделей программ. М.:МЦНМО, 2002. В формате djvu (DjVu — о формате)
Презентации лекций по верификации (внешняя ссылка: logic.pdmi.ras.ru)
Васильева К.А., Кузьмин Е.В., Соколов В.А. Верификация автоматных программ с использованием LTL (PDF)
Baranov S.N., Kotlyarov V.P., Letichevsky A.A., Drobintsev P.D. The technology of automation verification and testing in industrial projects (DjVu — о формате)
Applying Model Checking to Concurrent UML Models (внешняя ссылка: www.jot.fm)
Второй раз присудили премию Тьюринга по верификации. В первый раз в 1996 году - за темпоральную логику, в 2007 году - за model-checking. (внешняя ссылка: ru.wikipedia.org)
Кузьмин Е.В., Соколов В.А. Моделирование, спецификация и верификация "автоматных" программ (PDF)
Верификация моделей как основа новых методологий разработки ПО, способных гарантировать работу программ в точном соответствии с требованиями к ним (внешняя ссылка: www.osp.ru)
Правила Хольцмана для надежного ПО (внешняя ссылка: www.pcweek.ru)
Видеолекции по верификации (внешняя ссылка: logic.pdmi.ras.ru)
Еще одна книга по верификации (внешняя ссылка: fmt.isti.cnr.it)
В поисках надежного кода (PDF)
Разговоры о Model Checking (PDF)
Проектирование в условиях временных ограничений: верификация проектов (DjVu — о формате)
Кулямин В.В. Методы верификации программного обеспечения. 117с. (внешняя ссылка: www.sci-innov.ru)
Кулямин В., Корныхин Е. Формальная верификация: методы и приложения (внешняя ссылка: panda.ispras.ru)
Кубасов С.В., Соколов В.А. Синхронная модель автоматной программы // Моделирование и анализ информационных систем. 2007. № 1, с. 11-18 (внешняя ссылка: mais.uniyar.ac.ru)
Верификация авиационных систем (внешняя ссылка: www.google.ru)
Об инструментальных средствах для критических систем на русском языке (внешняя ссылка: www.avdsys.ru)
Статья о применении формальных методов при создании ответственных систем (внешняя ссылка: www.msse.umn.edu)
Использование формальных методов при создании авиационных систем (2008 г.) - "сумбур вместо музыки" (внешняя ссылка: users.encs.concordia.ca)
Model Checking для критических систем (2010 г.). Stateflow, SAT, конвертор Java-Promela и много чего еще (внешняя ссылка: www.sefm2010.isti.cnr.it)
При верификации в 2008 г. в компании Rockwell Collins используются stateflow (внешняя ссылка: www.csl.sri.com)
Карпов Ю. Новая жизнь верификации (внешняя ссылка: www.osp.ru)
Кузьмин Е.В., Соколов В.А. О верификации LD-программм логических контроллеров // Моделирование и анализ информационных систем. Т. 19, №2 (2012), с. 138-144 (внешняя ссылка: mais.uniyar.ac.ru)
Белоглазов Д.М., Машуков М.Ю., Непомнящий В.А. Верификация телекоммуникационных систем, специфицированных взаимодействующими конечными автоматами, с помощью раскрашенных сетей Петри // Моделирование и анализ информационных систем. Т. 18, №4 (2011), с. 144-156 (внешняя ссылка: mais.uniyar.ac.ru)
Проектирование программных бортовых систем управления с поддержкой верификации. Применение автоматов при спецификации программ критикуется (внешняя ссылка: mais.uniyar.ac.ru)
Презентации на тему "Формальная верификация" (внешняя ссылка: www.myshared.ru)
Приняли доклад на еще одну конференцию по верификации TMPA-2014 (внешняя ссылка: tmpaconf.org)
Статья "Модельно-ориентированное проектирование по стандарту DO-254 с помощью инструментов компаний MathWorks и Mentor Graphics" (внешняя ссылка: matlab.ru)
Применение единых стандартов на бортовое оборудование перспективных изделий авиационной техники (внешняя ссылка: npo-nauka.ru)
Стандарт DO 254 на YouTube (внешняя ссылка: www.youtube.com)
Automated Testing and Validation with Reactis (внешняя ссылка: www.reactive-systems.com)
Наши результаты Корнеев Г.А., Парфенов В.Г., Шалыто А.А. Верификация автоматных программ (PDF)
 Вельдер С.Э., Шалыто А.А. Введение в верификацию автоматных программ
 Вельдер С.Э. Введение в верификацию автоматных программ на основе метода Model checking
Гуров В.С., Шалыто А.А., Яминов Б.Р. Технология верификации автоматных моделей программ без их трансляции во входной язык верификатора (PDF)
Гуров В.С., Яминов Б.Р. Технология верификации автоматных моделей программ без их трансляции во входной язык верификатора (PDF)
Лукин М.А., Шалыто А.А. Автоматизация верификации визуальных автоматных программ (PDF)
Вельдер С.Э., Шалыто А.А. Верификация простых автоматных программ на основе метода Model Checking (PDF)
Курбацкий Е.А., Шалыто А.А. Верификация программ, построенных на основе автоматного подхода (PDF)
Свидетельство о государственной регистрации программы для ЭВМ "Транслятор автоматной Unimod-модели во входной язык верификатора Spin" (PDF)
Свидетельство о государственной регистрации программы для ЭВМ "Расширение верификатора Bagor для верификации автоматных Unimod-моделей" (PDF)
Вельдер С.Э., Шалыто А.А. Введение в верификацию автоматных программ на основе метода Model Checking //Научно-технический вестник. Вып. 42. Фундаментальные и прикладные исследования информационных систем и технологий. СПбГУ ИТМО. 2007, с. 33-48. (внешняя ссылка: ntv.ifmo.ru)
Kurbatsky E. Verification of automata-based programs (PDF)
Егоров К.В. Разработка верификатора автоматных программ
Свидетельство о государственной регистрации программы для ЭВМ "Транслятор автоматной модели во входной язык верификатора SMV"
Свидетельство о государственной регистрации программы для ЭВМ "Система преобразования автоматной модели в модель Крипке и верификация CTL-свойств на ней"
Верификация автоматных программ
Разработка технологии верификации управляющих программ со сложным поведением, построенных на основе автоматного подхода (PDF)
Егоров К.В., Шалыто А.А. Методика верификации автоматных программ (PDF)
Канжелев С.Ю. Верификация взаимодействия частей реактивной системы, реализованных с помощью автоматного подхода (PDF)
Вельдер С.Э., Шалыто А.А. Методы верификации моделей автоматных программ (PDF)
Обсуждение доклада Андрея Клебанова на SYRCoSE 2010 (внешняя ссылка: coldattic.info)
Клебанов А.А., Степанов О.Г., Шалыто А.А. Применение шаблонов требований к формальной спецификации и верификации автоматных программ (PDF)
Вельдер С.Э., Лукин М.А., Шалыто А.А., Яминов Б.Р. Верификация автоматных программ (PDF)
Michael Lukin, Sergey Velder, Anatoly Shalyto, Bulat Yaminov. Verification of automata-based programs (PDF)
В. Ульянцев. Отчет о верификации программы управления часами с будильником (PDF)
Государственный контракт. Этап 1 Промежуточный отчет по этапу I "Выбор направления исследований и базовых компонентов" (PDF)
Отчет о патентных исследованиях по этапу I (PDF)
Государственный контракт. Этап 2 Отчет по контракту о верификации автоматных программ. Второй этап. (PDF)
Государственный контракт. Этап 3 Отчет по контракту о верификации автоматных программ. Третий этап. (PDF)
Государственный контракт. Этап 4 Отчет по контракту о верификации автоматных программ. Четвертый этап. (PDF)
|
