2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 3
Текст из файла (страница 3)
— "за их рань в превращении метода Моде! сйес(анп днз-русски — "проверка модели7 в высокоэффектштую техниеогию еерификаьжц широко исиаеьзуемую в иидуюнрии разработки программного обеслечения и аппаратных средств". дйн(е! сйесйтй — зто формаяьиая проверка того, выполняется ли заданная логическая формула на двиной структуре. Структура представляет собой молель разрабатываемой оистемы, логическая формула описывает требования к поведению системы. Этот метод уже сегодня широко используется во всем мире лля проверки слшкных обьектов — как программного обеспечения, так н аппаратуры. Он позволяет существенно повысить степень увереншмтн разработчиков в правильности функцноннрованиа интегральных схем, протоколов коммуннющнн, драйверов устройств, бортовых систем управления для автомобилей, самолвюв, космических аппаратов.
Премия Тьюринга рассматриваетоя мировым сообществом как Нобелевакая премия в области информатики. Она вручается юкегодно с 1966 г. за выдающийся вклад в усовершенствование компьютерных технологий. Премия Тью. ринга за 2007 г., похшлуй, впервые отметила ученых, вклад которых состоял не столько в рыработке удивительно кряаивой теории, имеющей важное практическое применение, сколько в доведении этой теории до уровня "высокоэффективной промышленной технологии". Президент АСМ Стюарт Фельдман сказал: "Эню великий пример того, как технааогия, юменивииж промышленность, родилось ю чисто теоретических иссшдований". Новые научные результаты были сразу изстребованы пракппюй. Без концептуального прорыва в теории верификации, беэ испояьэованил этих новых результатов разрабатываемые сегодня программнью н аппаратные продукты беспрецедентной сложности не могли бы быть созданы с достаточным уровнем надежности, а компании-разработчики в перспективе раэорилнсь бы, выплачивая неустойки эа ущерб, нанесенный ошибочным функционированием их разработок.
Однако едва лн не большее значение метод пюбе! сйесЫпб приобрел в последние годы в связи с возмвкностью применения его результатов и идей ао многих областях, шсьма далеких от области верификации технических систем, для которой этот метод был первоначвяьио разработан. Даннал книга посвящена изложеншо этих новых идей и описанию нх применений. В книге рассказывается о новых результатах в области верификации, полученных с помощью метода воде! сйесй|п~, и приводятся примеры использования этого метода в самых разных областях.
Эта область теоретической информатики была разработана сравнительно недавно, но она уже привела к "прорывным" практическим результатам н вызвааа значительный интерес из-за своей изащности и эффективности. Верификация программных систем — фундаментальный раздел информатн.
ки, основанный на формальных мепцюх. Трудность изучения н восприятия формальных методов часто является следствием оторванности таких формалюмов ст практики. Среди программистов широко распространено мнение, чго формальные методы не имеют никакого реального применения к решению практических проблем, что зго просто необязательное прилшкение к рутинным приемам техники программирования, которые одни только и нужны программисту. Подход тоИе! сйесйиб опровергает это мнение.
Несмотря на то, что полученные здесь результаты базируются на таких абстракциях, как темпоральные логики и структуры Кринке, бесконечные языки и автоматы Бюхи, неподвижные точки операторов, а также на других "страшных" формализмах, материализация этих абстра«тных понятий дала удивительные практические результаты.
На их основе созданы и работшот автоматические системы верификации, позволяющие рюработчикам систем методом "иахплния яяолкй' (рпэЬ Ьшгол) проверять бортовые системы управления космических аппаратов, встроенные программы военной техники, мобильных телефонов, медицинской аппаратуры. Пугь от этих абстракций к практическим задачам информатики удивишльно прям н очевиден. Некоторые ученые называют зго направление "реабилитацией формальлыг мевкхзое": здесь формальнме модели позволшш получить результаты, без применения которых невозможно выполншь любую прэктическую рюрабатку программных н аппаратных систем для шйъезньи, критических применений. Матерная книги будет полезен трем категориям читателей.
Во-первых, зто шудвнэы, обучающиеся по направлению "Информатика". Изучение теории н методов, обьелиненных под общим термином воде! ейесМпй, вюпочено в учебные шшны многих иностранных университетов. Тшюй интерес вызван тем, что этот раздел представляет наиболее значнзаль. ные результаты в области верификации с тех пор, как эта проблема впервые баяла поставлена 40 лет назад.
Интерес вьпван таске простотой и логической ясностью этих результатов, в также возможностью их практического приме. пения. Этот новый раздел теоретической информатики станет, несомненно, обязательной частью базового фундаментавьного образования е области информатики.
"Формвчьные методы должны стать частью обраювания каждого исследователя в облвстн информатики и кюкдого разработчика ПО так же, ° ак другие ветви прикладной математики являются необходимой частью обраювання в других инженерных областях", — говоритса в отчете ХАЗА. Хои техника применения этого подхода проще, чем теория, верификация систем требует достаточно высокой квалификации исполнителей. Спецналнстй ° этой области весьма востребованы. Во-вторых, это научные работники. В отличие от многих теоретических рн».
лшюв вычислительной науки, которые стали уже юшсснкой, данное напрввшние является "горячей" областью исследований, здесь продолжается акшвиш исследовательская рабата, которая направвена на расширение возможностей верификации технических систем н на применение этого подхода к широкому кругу других задач. Богатство применений этой новой техники в совершенно разных обгшсшх, огромное число открытых проблем не могут оставить равнодушным ни одного исследователя. В книге прююдятся прнмерм того, квк эти новые идеи используются для решение многих проблем ° различных областях.
Третьей категорией читателеям, которые могут извлечь пслюу нз данной книги, являлися инженеры-разработчики новых систем. "Формальные методы обеспечивают интеллекгуальную основу нашей области, они помогают оформить наши мысли и направить их на плодотворный пуп. при решении ироблем; они обеспечивает нотацию при документировании требований н разработки, позволяют выразить мысли при общении разработчиков в точной и ясной манере, онн обеспечивают нас инсгрументальными средствамн для анализа свойств систем", — говорится в упомянутом выше отчете ХАЗА. Раздел формальной верификации, основанный на мегоде тсгге! сдесйлб, достиг уровня зрелоеги. Он предоставляет разработчику программных и алпарп них систем теоретические основы, ясную методику, простую нотацию н эффективный инструментарий для верификации систем.
Материал данной книги достаточен для того, чтобы любой программист, заботящийся о качестве результатов своего труда, смог немедленно применить изложенные здесь методы для проверки сваей разработки и повышения степени доверня к ней, используя доступный инструментарий н технику "рнзЬ Ьопон". Дпя понимания книги необходимы только начальные знания в обласгн дне° ретноп математики: логики высказываний и теории автоматов в сбьеме ваадных университетских курсов, а также первоначальный опыт прогжзммированнв.
В одной вводной книге невозмакно изложить все, яли плясе большую часть вопросов, относящихся к данной области. Автор постарачся по возможности просто и компакпю раскрыть основные иден и принципы этого напшэвлення. Интересующиссв читатели без труда смогуг найти литературу, относящуюся к лругнм Рюделам этой области, и после про пения данной книги разобраться в ней.
К насюящему времени формяльнав вернфивщия уже стаха этапом технологического цикла прн создании сложных встроенных систем во многих фирмах-разработчиках программно-апцарвтиых систем для критических применений. Но среди названий этих фирм трудно найти российские. Курсы по формальным моделям, темпоральным логикам и верификации спши традиционными во всех ведущих универсиштвх мира — но нх читают только в ничтожно махом числе вузов России. Существует обширная литерюура, посвященная исследованиич в этой области, но на русском языке такой литературы почти нет.
Исследования проводятся во всех рашигых странах — кроме России, где этими проблемами эаниммотся только в двух-трех научнмх группах. Результаты этого очевидны. Например, компания "Сухой" с гордостью рапортует о заключенных контрактах на поставку ее истребителей за рубеж, но на экспортируемые самолеты ставится электроника, сделанная не в России, а во Франции. Именно ао Франции работзег один из трех лауреатов премии Тьюринга 2007 г., в нескольких лабораториях Франции ведутся интенсивные исследования в области верификации и разработаны технологии созданна надюкных бортовых систем. Очевидно, что зарубежная авионика может имать лишь очень ограниченное применение в отечественной боевой авшщин н в других критических областях.
Автор будет считюь сваю задачу выполненной, если его книга хотя бы а малой степени изменит существующее положение в отечественной науке и образовании в этой области. Следует признаться, однако, что забота об отечественной науке составила лишь домо мотивации лля написания этой книги. Намного более сильным быяо желание автора поделиться с читателем тем восхищением, которое вызывают ишщество формальных молелей н их удивительная мощь при решении важнейших насущных практических проблем информатики.
Структура книги Представленный в книге материал макет состашпь основу одно- нли дву»- семестрового университетского курев по верифшшщш параллельных н раг прсделенных программ. Структура представленного мщеривла слеяующая. 1 лава 1 является вводной. В ней описывжотся некоторые примеры ошибок в программных системах и их последствия. Показываеюя, что именно царап лельные н распределенные программы являются сложными для их понима. ния и анализа, что формальная верификация являеюя важнейшим средством выявления тонких ошибок в параллельных системах.
Приводится общая оке. ма верификации и рассматривается метод любе! сйес(ппй как один из подхо дов к формальной верификации. Здесь же анализнрукпся сильные н слабые стороны верификации н тестированнв, этих двух классических методов повышения уровня доверия к разработкам. Приводятся примеры успешншп применения верифюации к практическим разрабопам программного обеспечения и аппаратуры: коммуникационным протоколам, бортовым сисшмам управления космическими аппаратами и т. п.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
