Главная » Все файлы » Просмотр файлов из архивов » Файлы формата DJVU » 2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010)

2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010).djvu), страница 5

DJVU-файл 2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010).djvu), страница 5 Математические методы верификации схем и программ (3373): Книга - 10 семестр (2 семестр магистратуры)2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (2. Model Checking. Вериф. парал. и распределенных программных сис2020-08-25СтудИзба

Описание файла

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 долларов за эту работу.

Свежие статьи
Популярно сейчас
Как Вы думаете, сколько людей до Вас делали точно такое же задание? 99% студентов выполняют точно такие же задания, как и их предшественники год назад. Найдите нужный учебный материал на СтудИзбе!
Ответы на популярные вопросы
Да! Наши авторы собирают и выкладывают те работы, которые сдаются в Вашем учебном заведении ежегодно и уже проверены преподавателями.
Да! У нас любой человек может выложить любую учебную работу и зарабатывать на её продажах! Но каждый учебный материал публикуется только после тщательной проверки администрацией.
Вернём деньги! А если быть более точными, то автору даётся немного времени на исправление, а если не исправит или выйдет время, то вернём деньги в полном объёме!
Да! На равне с готовыми студенческими работами у нас продаются услуги. Цены на услуги видны сразу, то есть Вам нужно только указать параметры и сразу можно оплачивать.
Отзывы студентов
Ставлю 10/10
Все нравится, очень удобный сайт, помогает в учебе. Кроме этого, можно заработать самому, выставляя готовые учебные материалы на продажу здесь. Рейтинги и отзывы на преподавателей очень помогают сориентироваться в начале нового семестра. Спасибо за такую функцию. Ставлю максимальную оценку.
Лучшая платформа для успешной сдачи сессии
Познакомился со СтудИзбой благодаря своему другу, очень нравится интерфейс, количество доступных файлов, цена, в общем, все прекрасно. Даже сам продаю какие-то свои работы.
Студизба ван лав ❤
Очень офигенный сайт для студентов. Много полезных учебных материалов. Пользуюсь студизбой с октября 2021 года. Серьёзных нареканий нет. Хотелось бы, что бы ввели подписочную модель и сделали материалы дешевле 300 рублей в рамках подписки бесплатными.
Отличный сайт
Лично меня всё устраивает - и покупка, и продажа; и цены, и возможность предпросмотра куска файла, и обилие бесплатных файлов (в подборках по авторам, читай, ВУЗам и факультетам). Есть определённые баги, но всё решаемо, да и администраторы реагируют в течение суток.
Маленький отзыв о большом помощнике!
Студизба спасает в те моменты, когда сроки горят, а работ накопилось достаточно. Довольно удобный сайт с простой навигацией и огромным количеством материалов.
Студ. Изба как крупнейший сборник работ для студентов
Тут дофига бывает всего полезного. Печально, что бывают предметы по которым даже одного бесплатного решения нет, но это скорее вопрос к студентам. В остальном всё здорово.
Спасательный островок
Если уже не успеваешь разобраться или застрял на каком-то задание поможет тебе быстро и недорого решить твою проблему.
Всё и так отлично
Всё очень удобно. Особенно круто, что есть система бонусов и можно выводить остатки денег. Очень много качественных бесплатных файлов.
Отзыв о системе "Студизба"
Отличная платформа для распространения работ, востребованных студентами. Хорошо налаженная и качественная работа сайта, огромная база заданий и аудитория.
Отличный помощник
Отличный сайт с кучей полезных файлов, позволяющий найти много методичек / учебников / отзывов о вузах и преподователях.
Отлично помогает студентам в любой момент для решения трудных и незамедлительных задач
Хотелось бы больше конкретной информации о преподавателях. А так в принципе хороший сайт, всегда им пользуюсь и ни разу не было желания прекратить. Хороший сайт для помощи студентам, удобный и приятный интерфейс. Из недостатков можно выделить только отсутствия небольшого количества файлов.
Спасибо за шикарный сайт
Великолепный сайт на котором студент за не большие деньги может найти помощь с дз, проектами курсовыми, лабораторными, а также узнать отзывы на преподавателей и бесплатно скачать пособия.
Популярные преподаватели
Добавляйте материалы
и зарабатывайте!
Продажи идут автоматически
5173
Авторов
на СтудИзбе
436
Средний доход
с одного платного файла
Обучение Подробнее