Тарасюк О.М., Горбенко А.В.

Министерство образования и науки Украины, Национальный аэрокосмический университет им. Н.Е. Жуковского «ХАИ», 2009. – 214 с.

ISSN/ISBN/UDC:  978-966-96770-3-7

В книге изложены материалы для лекционного курса, посвященного формальным методам разработки, верификации и анализа надежности программного обеспечения и информационно-управляющих систем (ИУС) для критических приложений. Анализируются требования к программному обеспечению, методы формулирования и спецификации требований, а также процесс управления требованиями. Рассматривается задача гармонизации и профилирования требований на примере компьютерных сетей ИУС критического применения. Дается описание формальных методов спецификации требований, разработки и верификации программного обеспечения, использующие аппарат строгого математического (логического) анализа и доказательства теорем. Представлен обзор формальных методов анализа надежности и рисков безопасности.

Лекционный курс соответствует программе дисциплины «Формальные методы разработки критического программного обеспечения» (Formal Methods of Critical Software Development), подготовленной для аспирантов в рамках проекта TEMPUS-MASTAC. Этот проект, финансируемый Европейским Союзом по программе TEMPUS (JEP_26008_2005) «MSc and PhD Studies in Aerospace Critical Computing», посвящен разработке и внедрению учебных курсов для подготовки магистров и докторов философии (кандидатов наук) по направлению аэрокосмического критического компьютинга.

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

Библ. - 63 наименований, рисунков - 43, таблиц - 21.