Эксπир
Регистрация / Вход

Разработка технологии верификации управляющих программ со сложным поведением, построенных на основе автоматного подхода

Стадии проекта
Предложение принято
Конкурс завершен
Проект закончен
Проект
02.514.11.4048
Организация
Университет ИТМО
Руководитель работ
Шалыто Анатолий Абрамович
Продолжительность работ
2007 - 2008, 17 мес.
Бюджетные средства
6 млн
Внебюджетные средства
1,24 млн

Разработка технологии верификации программного обеспечения на языках общего назначения, на базе моделей и с учетом специфики предметной области

Предложения

Разработка теоретических основ и технологии создания автоматизированной системы для тестирования трансляции формальных моделей при разработке информационных систем.
Тема
Разработка теоретических основ и технологии создания автоматизированной системы для тестирования трансляции формальных моделей при разработке информационных систем.
Входящий номер
727
Организация
СПИИРАН
Руководитель организации-инициатора
Юсупов Рафаэль Мидхатович
Исследование и разработка методов обнаружения дефектов в программном обеспечении
Тема
Исследование и разработка методов обнаружения дефектов в программном обеспечении
Входящий номер
1930
Организация
ИСП РАН
Руководитель организации-инициатора
Аветисян Арутюн Ишханович

Этапы проекта

1
18.05.2007 - 30.09.2007
• Проведены анализ и сформированы требования к методам верификации автоматных моделей управляющих программ.
• Разработаны базовые методы верификации на моделях, предназначенных для генерации автоматных моделей управляющих программ.
• Проведены патентные исследования.
• Достигнуты технико-экономические показатели.
Развернуть
2
01.10.2007 - 31.12.2007
Излагаются методы автоматизации верификации управляющих программ со сложным поведением, разработанные при проведении научно-исследовательской работы по лоту «Разработка технологий верификации программного обеспечения» шифр «2007-4-1.4-18-02-041» по теме «Разработка технологии верификации управляющих программ со сложным поведением, построенных на основе автоматного подхода», выполняемой в рамках Федеральной целевой научно-технической программы «Исследования и разработки по приоритетным направлениям развития научно-технологического комплекса России на 2007−2012 годы» по государственному контракту № 02.514.11.4048 от 18.05.2007, заключенному между Федеральным агентством по науке и инновациям и Государственным образовательным учреждением высшего профессионального образования «Санкт-Петербургский государственный университет информационных технологий, механики и оптики» на основании решения Конкурсной комиссии Роснауки № 14 (протокол от 28.04.2007 г. № 15). Предложен набор методов, позволяющих автоматизировать верификацию автоматных моделей управляющих программ. Для методов приведены их функциональные особенности и характеристики. Описываются созданные прототипы автоматизированных верификаторов автоматных моделей управляющих программ.
Развернуть
3
01.01.2008 - 30.06.2008
Объектом исследования работы являются методы верификации автоматов управления системами со сложным поведением.
Целью работы является разработка и апробация технологии верификации автоматных программ. Целью третьего этапа является апробация и экспериментально исследование методов верификации автоматных моделей управляющих программ, разработанных на предыдущих этапах на примере верификации системы управления моделью банкомата.
С целью апробации методы верификации автоматных программ реализованы в инструментальных средствах FSM Verifier, CTLVerifier, Converter и Unimod.Verifier. В качестве тестовых управляющих систем для верификации были выбраны системы управления двумя банкоматомами.
Произведена реализация и апробации на примере системы со сложным поведением методов верификации автоматных программ, разработанные на втором этапе работ. Была доказана применимость этих методов на практике и их эффективность с точки зрения обнаружения дефектов программного обеспечения.
Развернуть
4
01.07.2008 - 31.10.2008
• Разработаны методические указания и рекомендации по применению методов, разработанных в рамках работ по контракту.
• Описаны прототипы инструментальных средств, созданных на основе разработанных методов и даны методические рекомендации по их применению
• Составлена программная документация на прототип инструментального средства верификации автоматных программ Unimod.Verifier.
• Проведены дополнительные патентные исследования.
Достигнуты технико-экономические показатели.
Развернуть

Программа

Программа "Исследования и разработки по приоритетным направлениям развития научно-технологического комплекса России на 2007-2013 годы"

Программное мероприятие

1.4 Проведение проблемно-ориентированных поисковых исследований и создание научно-технического задела по перспективным технологиям в области информационно-телекоммуникационных систем
Продолжительность работ
2007, 8 мес.
Бюджетные средства
3 млн
профинансировано
Тема
Разработка технологий верификации программного обеспечения
Продолжительность работ
2007 - 2008, 17 мес.
Бюджетные средства
18 млн
Количество заявок
13
Тема
Технология автоматного программирования: применение и инструментальные средства
Продолжительность работ
2005 - 2006, 23 мес.
Бюджетные средства
15 млн
Количество заявок
2
Тема
Анализ принципов построения информационных систем для автоматического обнаружения логических ошибок и шаблонов неэффективного поведения в параллельных приложениях и их реализация в web-среде в виде программного комплекса.
Продолжительность работ
2013, 8 мес.
Бюджетные средства
24 млн
Количество заявок
12
Тема
Разработки в области языков программирования и моделирования программного обеспечения, технологий и инструментальных средств проектирования программ
Продолжительность работ
2007 - 2008, 17 мес.
Бюджетные средства
24 млн
Количество заявок
8
Тема
Организация и проведение международной конференции «Проблемы управления безопасностью сложных систем» (Москва)
Продолжительность работ
2014, 0 мес.
Бюджетные средства
3 млн
Количество заявок
2