Машиностроение
Приборостроение
Методическая периодика: проблемы и решения
Организация производства (промышленность)

Ключевые слова
Аннотации
Архив рубрик

регистрация
забыли пароль?

Другие журналы

электронный научно-технический журнал

ИНЖЕНЕРНЫЙ ВЕСТНИК

Издатель: Общероссийская общественная организация "Академия инженерных наук им. А.М. Прохорова".

Методы построения и верификации математических моделей систем реального времени

Инженерный вестник # 12, декабрь 2014
УДК: 519.681.3

Файл статьи:

Kozlov_I.pdf (967.04Кб)

авторы: Андреев А. М., Козлов И. А.

Системы реального времени имеют особенности, которые делают невозможной их проверку с помощью верификаторов общего назначения: при создании таких систем учитываются ограничения на временные характеристики функционирования, а значит и верификатор должен позволять проверять соответствие системы этим ограничениям. В статье рассматривается задача верификации систем реального времени. Предлагается подход к проверке таких систем на основе метода Model Checking. Рассмотрены модели, адекватно отображающие временные свойства систем реального времени. Описываются основные шаги верификации: построение математической модели, формулирование требований к ней, проверка полученной структуры на соответствие спецификации.

Список литературы
1.Кузьмин Е. В., Соколов В. А. О дисциплине специализации «Верификация программ» // Доклады II научно-методической конференции «Преподавание математики в компьютерных науках» Ярославль: ЯрГУ. 2007. С. 91-101
2. Дейкстра Э. Дисциплина программирования / Дал У., Дейкстра Э., Хоор К. Структурное программирование. М.: Мир. 1975. –247 с.
3.Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: Model checking. М.: МНЦМО, 2002. –416 с.
4. SPIN – http://spinroot.com/spin/whatispin.html
5. Symbolic Model Verificator. Carnegie Mellon University.–http://www.cs.cmu.edu/~modelcheck/smv.html
6. Alur R., Courcoubetis C., Dill D. Model-checking in dense real-time // Information and Computation. 104: 2–34, 1993.
7.Шалыто А. А. SWITCH-технология. Алгоритмизация и программирование задач логического управления. СПб.: Наука. 1998. –55 с.
8. Вельдер С.Э, Лукин М.А., Шалыто А.А., Яминов Б.Р. Верификация автоматных программ. СПбГУ ИТМО, 2011. – 240 с.
9.Карпов Ю. Г. MODEL CHECKING. Верификация параллельных и распределённых программных систем. –Спб.: БХВ-Петербург, 2010. –560 с.
10.Шалыто А. А. Программная реализация управляющих автоматов // Судостроительная промышленность. Серия «Автоматика и телемеханика». 1991. Вып. 13.
11. Поликарпова Н.И., Шалыто А.А. Автоматное программирование. 2008. — 167 с.
12.Кузьмин Е.В., Соколов В.А. О некоторых подходах к верификации автоматных программ.- Сборник докладов семинара Go4IT – шаг к новым технологиям Интернета. Москва, Институт системного программирования, 2007. С. 43-48.