Десять заповедей формальных методов

I Да будет у тебя адекватная нотация.
II Не применяй формальных методов всуе.
III Оценивай затраты.
IV Да будет у тебя наставник, являющийся по зову твоему.
V Не оставляй традиционных методов своих.

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

О формальных методах (ФМ) пишут как об одной из методик, позволяющих при условии правильного применения получать системы, обладающие высочайшей степенью целостности. Ряд стандартов рекомендуют ФМ для создания систем с повышенными требованиями к безопасности и защите информации [4, 11]; число таких стандартов, вероятно, будет расти [9].

Однако, хотя число проектов, разрабатываемых с применением ФМ, быстро растет, эта практика, к сожалению, по-прежнему остается скорее исключением, чем нормой [10]. Виной здесь серьезное непонимание [12] того, во что обходится использование ФМ, с какими сложностями связано и в какой степени окупается [8, 26].

Обратившись к обзорам промышленного применения ФМ при решении "реальных" (в противопоставление "игрушечным") задач [2, 17, 18], несложно убедиться, что проекты, основанные на ФМ, вполне способны укладываться и в график, и в бюджет и завершаться созданием правильно работающего программного (аппаратного) обеспечения, которое хорошо структурировано, легко обслуживается, очень нравится заказчику и полностью удовлетворяет всем его требованиям (см., к примеру, описания разработок в [28]).

Чем же обусловлен успех проекта, основанного на ФМ? Вопрос этот настолько субъективен, что смешно и пытаться ответить на него однозначно. Тем не менее нам удалось выявить ряд факторов, оказывающих, как мы полагаем, значительное влияние на успех ФМ-проекта. Опираясь на наблюдения (собственные и чужие) над недавно завершенными и разрабатываемыми в настоящее время проектами, как удачными, так и не очень, мы сформулировали десять правил - "заповедей", следование которым должно, по нашему ощущению, значительно повысить вероятность успеха и достижения высшей степени совершенства в овладении ФМ.

Десять заповедей

I Да будет у тебя адекватная нотация.

Язык спецификаций - основной инструмент разработчика на начальных стадиях проектирования системы. Разумеется, поскольку речь идет об ФМ-проектах, мы предполагаем, что нотация, применяемая на этом этапе, будет иметь хорошо определенную формальную семантику.

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

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

Что же касается языков с небольшим "словарем", то они дают в целом более длинные спецификации, более высокий уровень абстрагирования и почти индифферентны к будущей реализации. Таков, к примеру, язык CSP (Communicating Sequential Processes - коммуникация последовательных процессов), разработанный К. Хоором [30, 31]. Единицами первого класса там являются только процессы (или конвейеры и буферы, рассматриваемые как частные случаи процесса). Спецификации на CSP в результате могут оказаться весьма длинными, но благодаря тому, что изучить необходимо очень небольшое число конструкций, их всегда можно сразу понять. Аналогичным образом коммуникационные примитивы CSP не имеют уклона в сторону какой-либо реализации, а каналам могут с равным успехом физически соответствовать кабели, шины, очереди сообщений и даже просто переменные, доступные нескольким процессам.

Однако словарь - не единственное, что следует учитывать. Некоторые языки спецификаций хуже других подходят для определенных классов систем. Скажем, использовать для написания спецификаций параллельной системы язык, основанный на моделировании, такой как Z [46] или VDM, - все равно что забивать шурупы молотком: это осуществимо, но, разумеется, лучше обращаться с ними иначе. Алгебры процессов - например CSP или CCS [37] - в общем случае являются более удачным вариантом, но в них слишком мало внимания уделяется статическим аспектам систем. В ряде исследований делается попытка объединить алгебры процессов с языками моделирования, как в [47] и [52], либо расширить языки моделирования, добавив учет параллелизма и факторов времени, как в [34].

Для получения удачной промышленной программы важно, чтобы выбранная нотация принадлежала к числу общепринятых и имела солидную пользовательскую базу. Обычно создание формальной нотации - от появления замысла до начала реального промышленного применения - занимает не меньше десяти лет. Именно столько времени нужно на разработку ее исследователями, изучение студентами, испытание в режиме научно-промышленной эксплуатации, написание учебников, подготовку курсов для технических специалистов, признание пользовательским сообществом и т. д. На пути внедрения формальной нотации в промышленность немало препятствий, и каждое может оказаться роковым.

Серьезным этапом принятия нотации является выработка международного стандарта. Конечно, здесь мы имеем дело с проблемой курицы и яйца, поскольку разработчики желают, чтобы такой стандарт появился, но вовсе не жаждут принимать участие в дорогостоящем и длительном процессе его подготовки. Тем не менее существование стандарта, обеспечивающего в достаточной степени единообразный и совместимый набор инструментальных средств для поддержки нотации, играет очень большую роль. Можно заметить, что необходимость соответствия стандарту для языков спецификаций осознается слабее, чем для языков программирования, поскольку первые, в отличие от вторых, по определению не являются исполняемыми (в противном случае они были бы языками программирования!). Правда, в литературе обсуждаются достоинства и так называемых "исполняемых языков спецификаций"; подробнее об этом можно прочесть в [21, 27].

II Не применяй формальных методов всуе.

Не следует использовать ФМ только затем, чтобы, как это не раз случалось, удовлетворить прихоть начальства или потрафить коллегам. Точно так же как приход "объектной ориентации" вовлек множество фирм в ненужные расходы на переделку их систем в объектно-ориентированном духе, ФМ тоже могут использоваться без всякой на то необходимости. На самом деле первое, что следует определить, - это действительно ли вам нужны ФМ: из-за новых требований к секретности, из-за стандарта, на соблюдении которого настаивают заказчики, из-за слишком большой сложности и т. д.

Даже самые яростные сторонники ФМ вынуждены признать, что существуют области, в которых ФМ оказываются хуже более общепринятых методов. Так, считается, что они плохо подходят для проектирования пользовательского интерфейса, при котором важную роль играют неформальные соображения; впрочем, в нескольких программах, имевших определенный успех, формальная спецификация интерфейса все-таки была проведена [19].

Применять ФМ ко всем компонентам системы и излишне, и дорого. Даже в системе CICS - совместном проекте вычислительной лаборатории Оксфордского университета и корпорации IBM, удостоенном Королевской премии за достижения в технике, - с помощью ФМ разработано лишь около десятой части. Эта десятая часть вылилась в сотни тысяч строк кода и тысячи страниц спецификаций, позволила снизить затраты на 9% по сравнению с разработкой традиционными методами (подтверждено независимой проверкой) и часто упоминается в качестве одного из самых значительных примеров применения ФМ [41].

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

1. Формальная спецификация

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

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

Эта техника очень хорошо зарекомендовала себя при разработке программной архитектуры для семейства осциллографов [22] и в таких разнообразных видах деятельности, как формальное описание алгоритма для системы голосования [38], описание структуры документов [16, 29] и выявление внутренних противоречий в построении WWW [44].

2. Формальная разработка и проверка

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

В этом случае допускаются как формальные, так и неформальные, но строгие доказательства. Разработка каждой из прикладных систем, описываемых в [28], включала строгие доказательства некоторого уровня.

3. Доказательства, проверяемые на машине

С появлением инструментов поддержки, в частности, программ для доказательства теорем и проверки доказательств, стала возможна механическая проверка непротиворечивости и обоснованности доказательств.

Для некоторых классов систем машинная проверка доказательств действительно очень важна. Естественно включить сюда системы с повышенными требованиями к безопасности и защите. Фактически за такую проверку ратуют в своих стандартах многие организации. Так, Европейское космическое агентство настаивает на применении формальных доказательств (перед тестированием) везде, где это возможно, и рекомендует независимую проверку доказательств как способ уменьшить вероятность ошибки человека [9]; дело, видимо, идет к выдвижению требования машинной проверки.

Некоторые ФМ включают системы доказательства теорем в качестве одного из компонентов. Это в первую очередь HOL [24], Larch [25] (с компонентом LP - Larch Prover), Nqthm [13], OBJ [23] и PVS [40]. Кроме того, существуют системы доказательства и среды поддержки, включающие подобные системы, для таких методов как B [1] (B toolkit фирмы B-Core), CSP [31] (FDR фирмы Formal Systems (Europe) Ltd.), RAISE [43] (CRI), VDM [33] (VDM Toolbox фирмы IFAD) и Z [46] (Balzac/Zola фирмы Imperial Software Technology, ProofPower фирмы ICL).

Интересна идея разработки систем доказательства для использования с определенным методом. Так, программы доказательства теорем для Z были созданы в средах EVES [45], HOL [6] и OBJ [35].

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

III Оценивай затраты.

ФМ весьма дороги при интенсивном, а также при первом применении. Эффективное овладение ими требует серьезной подготовки, для введения их в технологический процесс разработки, как правило, нужны многие часы учебных занятий и услуги сторонних консультантов, программные средства поддержки также недешевы. Но, если оставить в стороне начальные расходы, легко показать, что ФМ-проекты могут обходиться столь же дешево, а то и дешевле, чем проекты, разработанные с применением обычных методов.

Это убедительно продемонстрировали, например, два ФМ-проекта, реализованных в Великобритании соответственно в 1990 и 1992 гг. и удостоившихся Королевской премии за достижения в области техники. В процессе изучения проектов, выдвинутых на премию, комиссия исследовала их финансовую выгодность. По ее оценке в первом проекте (узел вычислений с плавающей точкой Inmos для суперкомпьютера Transputer T800) формальная разработка микрокода с помощью алгебраических методов с компьютерной поддержкой позволила сэкономить 12 месяцев на тестировании [36]. Во втором проекте (гигантская система обработки транзакций IBM CICS) переписывание части спецификаций на языке Z сэкономило 9% стоимости разработки за счет уменьшения числа ошибок и повышения качества результирующего кода [32, 41].

Из того, что сколько-то ФМ-проектов не уложились в смету, не следует, что такие проекты вообще более дороги; это лишь показывает, что мы пока не очень опытны в оценке предполагаемых затрат [8].

Существует несколько моделей оценки стоимости и продолжительности разработки. Но в большинстве своем они предполагают разработку традиционными (структурными) методами и исходят из числа строк исполняемого кода в окончательной реализации (весьма субъективный показатель). Попытки получить показатели для формальных спецификаций также делались (например, [49]), но ни одна из них еще не развилась до модели, позволяющей реально оценить стоимость проекта.

В настоящее время мы должны опираться на модели, разработанные до того, как начали широко применяться формальные методы. Видимо, самая знаменитая из них - модель COCOMO, разработанная Б. Бёмом [3], где различные факторы получают вес в соответствии с их влиянием на разработку более ранних проектов в той же организации. Промежуточная модель дополняет базовую, уточняя значения 15 атрибутов, которые считаются ключевыми составляющими стоимости.

Многие из факторов, учитываемых Бёмом, существенно влияют и на стоимость разработки систем при использовании ФМ. ФМ применяются в системах с высочайшими требованиями к безошибочности и надежности, причем, как правило, сложных (или в особо сложных компонентах больших систем), а значит, вес таких показателей как RELY (Required Software Reliability - требуемая надежность системы) и CPLX (Product Complexity - сложность продукта) имеет тенденцию оказываться очень высоким. Часто это системы реального времени, поэтому показатель TIME (Execution Time Constraints - ограничения на время выполнения) также должен существенно влиять на стоимость проекта. Оставшиеся "компьютерные атрибуты" (Computer Attributes) Бёма, по-видимому, влияют слабее, то же относится и к "кадровым атрибутам" (Personnel Attributes). В действительности список последних следовало бы, вероятно, дополнить такими атрибутами как SEXP (Specification Language Experience - владение языком спецификаций), MCAP (Mathematical Capability - математические способности), FMEX (Formal Methods Experience - владение формальными методами) и DEXP (Domain Experience - знание предметной области).

Из атрибутов проекта (Project Attributes), как представляется, остаются в силе все. MODP (Modern Programming Practices - практический опыт современного программирования), похоже, не изменится, а вот влияние TOOL (Software Tools - программные инструменты) сильно возрастет благодаря более полезным инструментальным средствам и средам разработки [8]. Здесь также должны понадобиться дополнительные атрибуты, такие как DFOR (доля - в процентах - части системы, которая формально специфицируется или анализируется) и PROF (требуемая степень строгости доказательств).

Естественно ожидать, что использование ФМ значительно увеличит вес многих из перечисленных атрибутов. Но это не означает дороговизны ФМ как таковых, а лишь отражает тот факт, что они используются в системах с повышенными требованиями к надежности, которые сами по себе дороги, особенно если при "корректной" работе необходимо обеспечить строгую секретность.

Определение значений атрибутов также представляет собой непростую задачу. Согласно модели это должно делаться на основе информации о предыдущих проектах, разрабатывавшихся в аналогичной среде, других проектах в той же организации и похожих проектах в других организациях. Даже для случая более традиционных методов разработки получить такую информацию не всегда легко. В случае же ФМ сложности увеличиваются: реализованных проектов пока еще слишком мало для определения тенденций, к тому же многие проекты непоказательны, так как относятся к узкоспециальным областям, работа для которых, скорее всего, не будет систематической. Усиление интереса к внедрению ФМ [48] и к соответствующим обзорам [17, 18] рано или поздно позволит нам получить все необходимые детали. В работе [28] мы предприняли попытку свести воедино ряд имеющихся данных так, чтобы это было полезно для разработки промышленных проектов.

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

IV Да будет у тебя наставник, являющийся по зову твоему.

В большинстве успешно осуществленных к настоящему времени ФМ-проектов принимали участие сторонние эксперты-консультанты, имеющие опыт использования формальной техники. Научиться работать с ФМ без такой помощи, по-видимому, очень сложно, и она будет нужна до тех пор, пока в фирме не появятся собственные эксперты.

Эксперты помогали, в частности, при разработке IBM CICS [32] и узла вычислений с плавающей точкой Inmos для Transputer [36]. В IBM они провели не один месяц. Там были организованы учебные курсы, и постепенно значительное число сотрудников IBM освоили применение ФМ. Со временем в IBM накопилась "критическая масса" специалистов, т. е. корпорация стала самодостаточной в отношении использования ФМ, и необходимость в постоянных консультация сторонних экспертов отпала.

В Inmos подход был иным: там консультанты-математики прилагали к решению задачи свой опыт, а инженеры - свой. Однако хорошая организация взаимодействия между двумя группами обеспечила успех. Если же математики и инженеры не смогут оценить роль и проблемы друг друга, успех невозможен. Компания наняла нескольких человек с достаточными математическими знаниями и подготовкой для разработки и формальной проверки важнейших частей проекта. Когда требовалось, для решения конкретных проблем здесь также привлекались сторонние консультанты.

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

V Не оставляй традиционных методов своих.

В имеющиеся средства разработки программ вложены немалые деньги и усилия, и было бы в высшей степени неразумно все их разом заменить на ФМ. Желательно включать ФМ в процесс проектирования более экономичным способом. Один из способов здесь - исследовать, каким образом можно было бы эффективно сочетать имеющийся ФМ с имеющимся структурным методом, уже применяющимся в разработках. Одну из попыток создать такое сочетание представляет собой метод под названием SAZ - комбинация SSADM и Z [42]. Конечно, и у структурных, и у формальных методов есть свои сильные и слабые стороны, а их сочетание в идеале должно извлекать максимум из обоих. К примеру, ФМ позволяют постепенно уточнять спецификацию, а структурная спецификация больше скажет неспециалисту.

Альтернативное решение состоит в том, чтобы использовать ФМ для анализа существующего процесса. В ряде случаев возможно наладить двустороннюю связь между командой разработчиков, применяющей традиционные методы, и отдельной командой, которая начиная с ранних стадий проекта будет анализировать спецификации, выявляя таким путем многие ошибки еще до того, как исправлять их станет слишком дорого. Опыт успешного и, очевидно, не связанного с большими затратами применения для этой цели языка Z описан в [15].

В методе Cleanroom формальная нотация применяется для разработки программ, не основанной на исполнении [20]. Метод весьма успешно применялся как для высоконадежных, так и для обычных программ и позволил значительно снизить число ошибок. Программы создаются отдельно с использованием неформальных доказательств (часто только в уме), а затем сертифицируются (а не тестируются). Если при этом обнаруживается слишком много ошибок, считается, что надо изменить не программу, а процесс разработки. Прагматическое обоснование подхода состоит в том, что реальные программы слишком велики, чтобы можно было формально доказывать их правильность, поэтому прежде всего их нужно правильно писать. Возможность сочетания Cleanroom и ФМ исследовалась в [39].

Иногда оказывается возможным эффективно и с пользой комбинировать разные ФМ. Так, имеется опыт применения инструментальной поддержки HOL [24] для языка Z [6]. Это позволило сочетать относительно легко читаемую нотацию Z с механической проверкой доказательств в HOL и таким образом повысить надежность разработки.

В управлении ФМ-проектом роль технических аспектов, по-видимому, выше, чем обычно. Формальный подход предполагает, что код появляется на гораздо более поздней стадии цикла разработки. В спецификации же вкладывается значительно больше сил, чем при разработке стандартными методами. Число ошибок, устраняемых на этом этапе, также больше, но продвижение не столь очевидно, как в более типичных проектах. Один из способов обеспечить обратную связь, особенно для заказчика, состоит, вероятно, в быстрой разработке прототипа по спецификациям [14].

(Окончание в следующем номере)

ЛИТЕРАТУРА

1. Abrial J.-R. Assigning Meanings to Programs. Prentice Hall International Series in Computer Science, 1995.

2. Austin S., Parkin G.I. Formal Methods: A Survey. National Physical Laboratory, Queens Road, Teddington, Middlesex, TW11 0LW, UK, March 1993.

3. Boehm B.W. Software Engineering Economics. Prentice Hall, 1981.

4. Bowen J.P. Formal Methods in Safety-Critical Standards // Proc. Software Engineering Standards Symposium (SESS'93), Brighton, UK, 30 August - 3 September 1993. IEEE Computer Society Press, 1993, p. 168-177.

5. Bowen J.P. (ed.). Towards Verified Systems. Elsevier, Real-Time Safety-Critical Systems series, 1994.

6. Bowen J.P., Gordon M.J.C. Z and HOL // [7], p. 141-167.

7. Bowen J.P., Hall J.A. (eds.). Z User Workshop, Cambridge 1994. Springer-Verlag, 1994.

8. Bowen J.P., Hinchey M.G. Seven More Myths of Formal Methods. Technical Report PRG-TR-7-94, Programming Research Group, Oxford University Computing Laboratory, June 1994.

9. Bowen J.P., Hinchey M.G. Formal Methods and Safety-Critical Standards // IEEE Computer, August 1994.

10. Bowen J.P., Stavridou V. The Industrial Take-up of Formal Methods in Safety-Critical and Other Areas: A Perspective // [51], p. 183-195.

11. Bowen J.P., Stavridou V. Safety-Critical Systems, Formal Methods and Standards // Software Engineering Journal, 1993, v. 8, N 4, р. 189-209.

12. Bowen J.P., Stavridou V. Formal Methods: Epideictic or Apodeictic? // Software Engineering Journal, 1994, v. 9 N 1, p. 2.

13. Boyer R.S., Moore J.S. A Computational Logic Handbook. Academic Press, 1988.

14. Breuer P.T., Bowen J.P. Towards Correct Executable Semantics for Z // [7], p. 185-209.

15. Aujla S., Bryant A., Semmens L.: A Rigorous Review Technique: Using Formal Notations within Conventional Development Methods // Proc. Software Engineering Standards Symposium (SESS'93), Brighton, UK, 30 August - 3 September 1993. IEEE Computer Society Press, 1993, p. 247-255.

16. Cahill A., Hinchey M.G., Relihan L. Documents are Programs // Proceedings ACM SIGDOC'93, 11th International Conference on System Documentation, Waterloo, Canada, 5-8 October 1993. New York: ACM Press, 1993, p. 43-55.

17. Craigen D., Gerhart S., Ralston T. An International Survey of Industrial Applications of Formal Methods. Atomic Energy Control Board of Canada, U.S. National Institute of Standards and Technology, and U.S. Naval Research Laboratories, NIST GCR 93/626. National Technical Information Service, 5285 Port Royal Road, Springfield, VA 22161, USA, 1993.

18. Craigen D., Gerhart S., Ralston T. Applications of Formal Methods: Observations and Trends // [28].

19. Dix A. Formal Methods for Interactive Systems. Academic Press, Computers and People Series, 1991.

20. Dyer M. The Cleanroom Approach to Quality Software Development. John Wiley & Sons, Series in Software Engineering Practice, 1992.

21. Fuchs N.E. Specifications are (Preferably) Executable // IEE/BCS Software Engineering Journal, 1992, v. 7, N 5, p. 323-334.

22. Garlan D., Delisle N. Formal Development of a Software Architecture for a Family of Instrumentation Systems // [28].

23. Goguen J.A., Winkler T. Introducing OBJ3. Technical Report SRI-CSL-88-9, SRI, Menlo Park, USA, August 1988.

24. Gordon M.J.C., Melham T.F. (eds.). Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993.

25. Guttag J.V., Horning J.J. Larch: Languages and Tools for Formal Specification. Springer-Verlag, Texts and Monographs in Computer Science, 1993.

26. Hall J.A. Seven Myths of Formal Methods // IEEE Software, 1990, v. 7, N 5, p. 11-19.

27. Hayes I.J., Jones C.B. Specifica-tions are not (Necessarily) Executable // IEE/BCS Software Engineering Journal, 1989, v. 4, N 6, p. 330-338.

28. Hinchey M.G., Bowen J.P. (eds.). Applications of Formal Methods. Prentice-Hall International Series in Computer Science, 1995.

29. Hinchey M.G., Cahill A. Towards a Canonical Specification of Document Structures // Proceedings of ACM SIGDOC'92, 10th International Conference on System Documentation, Ottawa, Canada, 13-16 October 1992. New York: ACM Press, 1992, p. 297-307.

30. Hinchey M.G., Jarvis S.A. Concurrent Systems: Formal Development in CSP. McGraw-Hill International Series in Software Engineering, 1995.

31. Hoare C.A.R. Communicating Sequential Processes. Prentice Hall International Series in Computer Science, 1985.

32. Houston I.S.C., King S. CICS Project Report: Experiences and Results from the Use of Z in IBM // Prehn S., Toetenel W.J. (eds.). VDM'91: Formal Software Development Methods. Springer-Verlag, LNCS 551, 1991, p. 588-596.

33. Jones C.B. Systematic Software Development Using VDM: 2nd edition. Prentice Hall International Series in Computer Science, 1991.

34. Lamport L. TLZ // [7], p. 267-268.

35. Martin A. Encoding W: A Logic for Z in 2OBJ // [51], p. 462-481.

36. May D., Barrett G., Shepherd D. Designing Chips that Work // Hoare C.A.R., Gordon, M.J.C. Mechanized Reasoning and Hardware Design. Prentice Hall International Series in Computer Science, 1992.

37. Milner R. Communication and Concurrency. Prentice Hall International Series in Computer Science, 1989.

38. Mukherjee P., Wichmann B.A. Formal Specification of the STV Algorithm // [28].

39. Normington G. Cleanroom and Z // Bowen J.P., Nicholls J.E. Z User Workshop, London, 1992. Springer-Verlag, 1993, p. 281-293.

40. Owre S., Rushby J.M., Shankar N. PVS: A Prototype Verification System // Kapur D. (ed.). Automated Deduction - CADE-11. Springer-Verlag, LNAI 607, 1992, p. 748-752.

41. Phillips M. CICS/ESA 3.1 Experiences // Nicholls J.E. (ed.). Z User Workshop, Oxford, 1989. Springer-Verlag, 1990, p. 179-185.

42. Polack F., Mander K.C. Software Quality Assurance using the SAZ Method // [7], p. 230-249.

43. The RAISE Language Group: The RAISE Specification Language. Prentice Hall, 1992.

44. Relihan L., Cahill A., Hinchey M.G. Untangling the (World-Wide) Web // Proc. SIGDOC'94, Banff, Canada, October 1994.

45. Saaltink M. Z and Eves // Nicholls J.E. (ed.). Z User Workshop, York 1991. Springer-Verlag, 1992, p. 233-242.

46. Spivey J.M. The Z Notation: A Reference Manual: 2nd edition. Prentice Hall International Series in Computer Science, 1992.

47. Toetenel H. VDM + CCS + Time = MOSCA // 18th IFAC/IFIP Workshop on Real-Time Programming - WRTP'92, Bruges, Belgium, 23-26 June 1992. Pergamon Press, 1992.

48. Weber-Wulff D. Selling Formal Methods to Industry // [51], p. 671-678.

49. Whitty R. Structural Metrics for Z Specifications // Nicholls J.E. Z Users Meeting, Oxford 1989. Springer-Verlag, 1990, p. 186-191.

50. Wing J.M. A Specifier's Introduction to Formal Methods // IEEE Computer, 1990, v. 23, N 9, p. 8-24.

51. Woodcock J.C.P., Larsen P.G. (eds.). FME'93: Industrial-Strength Formal Methods. Springer-Verlag, LNCS 670, 1993.

52. Woodcock J.C.P., Morgan C.C. Refinement of Statebased Concurrent Systems // Bjorner D., Hoare C.A.R., Langmaack H. (eds.). VDM and Z - Formal Methods in Software Development. Springer-Verlag, LNCS 428, 1990, p. 340-351.