2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010).djvu), страница 5
Описание файла
DJVU-файл из архива "2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010).djvu", который расположен в категории "". Всё это находится в предмете "математические методы верификации схем и программ" из 10 семестр (2 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр DJVU-файла онлайн
Распознанный текст из DJVU-файла, 5 - страница
Потери от аварии были огромными. Кроме прямых потерь — утраты ракеты (затраты на ее разработку превышали 7 млрд долларов) и установленного на борту научного оборудования стоимостью более полумиллиарда долларов, ущерб составили и упущенная выгода от несостоявшихся запланированных запусков, и потеря на долгие годы репупщии ракеты как надакного средспш выведения полезной нагрузки на околоземную орбиту. Непрямые потери составили около 2 млрд долларов, (3 25 декабря 2004 г. после семилетнего полета космический зонд Гюйгенс отделился от автоматической международной межпланетной сшнцнн "Кассини" н начал спуск в атмосферу Титана — спутника Сатурна. 15 января 2005 г, зонд впервые в истории начал передмшть информацию с поверхности Титана.
Ошибка в бортовой прогрпиме зонда привела к тому, что половина переданной информации была потеряна. Затраты на рюработку зонда составили около 2,5 млрд долларов. (3 20 мвя 2000 г. Сообщение Ассошизйтед Пресс: "ХАЗА потеряло связь с марсоходом "Феникс". Выполнение задач, запланированных на второй день нахождения на Марсе американского космического аппарата "Феникс", отломана из-за возникших неполадок.
Связь с "Фениксом" утеряна". Стоимость проекта — 420 мли долларов. Г) В 4994 г. при разработке процессора 1пю) Релйпш была допущена ошибка во встроенной программе деления: несколько констант вспомогательного массива не были иннцнализнрованы, Ошибка была обнаружена уже после того, как дефектные процессорм поступили в продажу, и компанией "Интел" все они были заменены. Потери компании составили сотни миллионов долларов. (3 В декабре 2007 г.
в новых четырехъядериых процессорах АМО Рйепош (Вагсе)опа) и Орытол, произведенных по новой, 65-нанометровой технологии, выявлена ошибка реааишции буфера быстрого преобразования адреса кзш-памяти третьего уровня. Ошибка мшкег приводить к зависанию системы. (3 26 февраля 2009 г. Агентство В(оошЬегб сообщает. "Японское недрам(слепне крупнейшего швейпврского банка ОВ$ из-за компьютерной ошибки чуп, было не потратило 3 триллиона иен (31 млрд долларов) нв выкуп облигаций компании Сврсош. Финансовая организация объяснила, по собираввсь рззместнть заказ на покупку облигаций на сумму в 30 млн иен (310 000 долларов), но нз-за системной ошибки к заказу добавились нязь нулей".
Гибче 1 Финансовые потери от ошибок в программах только в США оцениваются в десяткн миллиардов долларов в год. Например, в 2002 г. этн потери оценены в 59,6 млрд долларов (52). Необходнмосп более тщателыюй проверки п трам паратных снстем приводит к задержквм в выполненнн проектов, м и ап проверки про- увеличению временн вывода продукта на рынок (йше-го-щагйег), а это грознт потерямн из-за конкуренцин н в связи со срывамн сроков поставки. Иногда ошибки в автоматических системах прнводят не только к матерналь- ным потерям, но н к потерям человеческих жнзней.
П В 1982 г. канадской компанией Агощю Епегйу оТ Смидл (яб, был зашущен в сершо меднцннскнй аппарат Тугае-25, предназначенный для облучения раковой опухоли потоком электронов. В прнборе использовалось новое программное обеспечение встроенной снсгемы упракчення процессом об- ПО, вне лучення. Несмотра на "тщательное тестирование", которому подверг лось , в нем остались ошнбкн: в редко встречающихся режимах, в которые носта прибор мог войти прн некоторых входных управляющнх последовател- ьостах, ннтенснвность сблученна жираствла на 2 порядка. Прибор эксп бо нек плуатнровался в разных клнннках несколько лет. За время эксплущв цнн рн ра некоторые больные получнлн передозировки облучення, двое пациентов умерлн, несколько чшювек остались инвалидами.
П 20 декабря 1995 г. в катастрофе самолета "Боинг-757" (Колумбня, рейс нз Майамн в Кали) погнблн 159 человек. Расследование показало, ной ката 3 казала, что прнчнно катасгро()ы была ошибка а одном символе программной системы управления полетом. Изготовитель бортового компьютера, компания Нопеуме!1 А!г Тгапзрогг Яумегпз и разработчик ПО компания )ерреяеп Запбегвоп о( Бпй)езчооб были признаны виновными в гнбели людей. Родственникам жертв аварии было выплачено 300 млн долларов. П Февраль 2008 г. Сообщение СМИ: "Амернканскнй спутник-шпион вышел нз-под контроля н мажет в конце февраля упасть на Землю.
Обломки спутника, по ннформацнн источника в правительстве США, могут содержать опасные материалы, а точно установить, где именно ушщет аппарат, пока не прсдставляегся возможным". П 23 марта 2003 г. система "Ранг!ог" ошибочно ндептнфнцнроаала брптвнскнй бомбардировщик "ТогпаЬ" гик приближающуюся вражескую ракету н автоматически произвела залп, Погибли два пилата. 2 апреля 2003 г. системой "Рагпог" уничтожен американский нстребнтел Р-16, гнб. В обо х гн .
о нх случаях прнчнной явнлнсь ошнбкн в бортовой системе автоматического обнаружения цели н наведения, П. 1! апреля 2008 г., сообщение СМИ; "В результате операции во время патрульного рейда вертолет США, "спутав цель", нанес удар по бронемвщн- нам, принадлшяащим ВВС США. Ранение получили нять человек — двое американских военнослулшших и трое мирных иракцев".
Во время войны в Ираке в США появился термин "дружественный огонь" (84епб1у бее). До 24% всех потерь живой силы в 1-й Иракской войне произошло из-за этой причины. Выводы многочисленных комиссий по расследованию подобных инцидентов однозначны: главная причина "дружественного огня" — все жпрастающая сложность технологий ХХ1 века, используемых в военных системах, и ошибки в программном и аппаратном обеспечении автоматического управления в военных системах.
К этой же теме относится заметка в РС йгеея от 28.04.2008 г., озаглавленная так: "Боевой робот азбулшоелзгя лротив хозяев": "В Ираке проводился эксперимент по эксплуатации усовершенствованных моделей боевых роботов "Та1оп", оснащйнных пулемвтом М249 н управляемых дистанционно. Один из ожидавших приказа аппаратов по непонятной причине "ожил" и стал самостоятельно шевелить манипулятором, в котором было установлено заряженное оружие". ГЗ 2 сентября 1988 г. на борт советской межпланетной станции "Фобос-1", отправленной на Марс, была передана с Земли неверная команда. Бортовым компькпером эта команда была жюпринвта квк команда иа отключение системы ориентации и стабилизации. Эта ошибка бортовой системы управления, которая обюаиа выявлять некорректные внешние команды н лолжным образом реагировать на них, привела к тому, что станция "Фобос-1" потерялась а космосе. Через полгода была потерана связь и с ее лублером — станцией "Фобос-2".
Наиболее вероятная причина этой второй неудачи — также программная ошибка. В результате просторы Вселенной сейчас бороздят безмолвные, бесполезные для человечества советские панцин "Фобос-1" и "Фобос-2". Приведенные примеры показывают, что ошибки в сложных программных и аппаратных системах не являются чем-то исключигельным, они повторяются регулярно в разработках сложных систем.
Их иепссредственнымн причинами являютсл и некорректные спецификации, и неправильное понимание спецификаций разработчиками, взаимное непонимание в коллективе разработчиков, непредвиденные события, режимы н условна работы, несогласованность параллельных ветвей программ и многое другое. В наше время, когда все чаще человеческая жизнь зависит от функцмонироаания автоматических систем, проблема гарантии привяпьности программных и аппаратных компонентов этих систем приобретвет первостепенное значение.
Надежность и предсказуемость поведения таких систем являются более важными свойствами, чем производительность, моднфицнруемость и т. п. Вернфиющия, как один из основных методов повышения качееша систем, становится вшкнейшей областью информатики. 1.2. Примеры ошибочных программ Параллельные и распределенные программы становятся все более распространенными. В современная автомобиле существует целая сеть свюаииых микропроцессоров, в новых "мерседесах" их около 50.
Пронзводнпли соревнуются в выпуске многовдерных процессоров для персональных компьютеров, но реально их возросшая вычислительная мощность мшкст быть использована только прн программировании параллельно выполняемых процессов. В 113б1 происходящий сейчас поворот программирования в сторону параллелспма назван "революцией" с лозунгом: "Добро пожаловать в мир параллельной обработки". Но именно этот мнр чреват проблемами, жпникаюцсими вследствие необходимости синхронизации параллельных процессов.
В мире параллельной обработки разработчик должен контролировать не последовательности возможных собмтий, как в последовательном программировании, а жпможные комбинации частично упорядоченных событий, что значительно слолшее. Многочисленные примеры показывмот, что нетривиальные многопоточные программы непостнясимы для человеческого мсцга. С ошибками, возможными в параллельных программах, может сегодня столкнуться каждый.
В качестве примера трудновыявляемых ошибок в параллельных программах приведем несколько простых программ. Прмыпр 1.1 В период обучения в вузе студенты чжто работшот. Студент А посгупил иа работу в компанию ЗойТесй и разработал бухгшперскую программу БухСофт, которую его компания использует сама и продает. Студент открыл депозитный банковасий счет Х„, с начальным капиталом О, на который бухгалтерская программа БухСафт! компании БойТесй должна перевести ему 3000 долларов за эту работу.