RUS ENG

Верификация больших программных систем

Ключевой проблемой информатики является поиск методов, позволяющих проверить, что программные и аппаратные системы делают то, что они должны делать, т.е. что они работают в соответствии со своей спецификацией. Особенно важна эта проблема для так называемых “реагирующих систем”, т.е. систем, которые состоят из нескольких параллельно функционирующих подсистем, которые взаимодействуют друг с другом и с окружением и реагируют на возникающие события (включение тумблера, поворот руля, получение сообщения). Это цифровые системы логического управления, протоколы коммуникации, драйверы внешних устройств и т.п.

 

Информатика является единственной областью инженерной деятельности, в которой разработчики систем, как правило, не умеют гарантировать качество разработанных ими систем и не отвечают за качество своего продукта. Особенно сложны для анализа параллельные и распределенные системы. В результате в разработанных программах остаются ошибки. В бытовых применениях это не столь страшно: так, по оценкам фирмы Microsoft, в ОС Windows 95 до сих пор остается несколько тысяч ошибок! Однако время от времени становятся известны факты, когда ошибки в автоматизированных системах приводят к огромным материальным потерям и даже к потерям человеческих жизней. Например, из-за ошибок в бортовых системах управления космические аппараты Фобос-1 и Фобос-2 были потеряны в космическом пространстве. В феврале 2010 г. ошибки в программно-аппаратной электронной системе управления автомобилей Toyota Prius привели к многочисленным авариям с несколькими человеческими жертвами и убыткам компании, которые оцениваются почти в 2 миллиарда долларов.

 

Научное и учебное направление “верификация параллельных и распределенных программных систем” на кафедре РВКС занимается проблемой доказательства того, что сложные программные системы работают правильно. Доказательство правильности – очень сложное, трудоемкое дело, требующее фундаментальных знаний и умений, глубокого понимания необходимых формальных моделей и практических программных технологий. Современные результаты в этом направлении позволили разработать методы верификации, которые уже сейчас применяются разработчиками бортовых систем управления авиационных и космических систем, медицинской аппаратуры, военной техники – везде там, где цена ошибки может быть слишком высокой. Знание теории и техники верификации программных систем существенно повышает конкурентоспособность наших выпускников на рынке труда и в научном сообществе.

 

В 2010 г. вышла монография Ю.Г.Карпова по верификации с отзывами академика В.П.Иванникова (Московский Университет и Московский Физико-технический институт) и профессора Р.Л.Смелянского (Московский Университет). Это первая (и пока единственная) монография в России, посвященная этой проблеме.