Регистрация / Вход
Прислать материал

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

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

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

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

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 млн
профинансировано
Продолжительность работ
2005, 1 мес.
Бюджетные средства
0,36 млн
Организация
ИСП РАН
профинансировано
Тема
Разработка технологий верификации программного обеспечения
Продолжительность работ
2007 - 2008, 17 мес.
Бюджетные средства
18 млн
Количество заявок
13
Тема
Разработка и верификация новых производственных технологий получения материалов (металлических, керамических, полимерных и/или композиционных) различного функционального назначения и изделий из них бионического дизайна на основе многоуровневых моделей формирования их служебных свойств
Продолжительность работ
2017 - 2019, 26 мес.
Бюджетные средства
130 млн
Количество заявок
0
Тема
Технология автоматного программирования: применение и инструментальные средства
Продолжительность работ
2005 - 2006, 23 мес.
Бюджетные средства
15 млн
Количество заявок
2
Тема
Анализ принципов построения информационных систем для автоматического обнаружения логических ошибок и шаблонов неэффективного поведения в параллельных приложениях и их реализация в web-среде в виде программного комплекса.
Продолжительность работ
2013, 8 мес.
Бюджетные средства
24 млн
Количество заявок
12
Тема
Разработки в области языков программирования и моделирования программного обеспечения, технологий и инструментальных средств проектирования программ
Продолжительность работ
2007 - 2008, 17 мес.
Бюджетные средства
24 млн
Количество заявок
8