Книги, научные публикации
ПРОГРАММНАЯ ИНЖЕНЕРИЯ МОДЕЛИРОВАНИЕ И АВТОМАТИЧЕСКАЯ ПРОВЕРКА ПО AsmL О.Р. Набиуллин, аспирант, Нижегородский филиал ГУ ВШЭ, nabiulin Э.А. Бабкин, доктор PhD, профессор, заведующий кафедрой
информационных систем и технологий, Нижегородский филиал ГУ ВШЭ, babkin Целью данной статьи является описание подхода связанного с использованием форма лизма Абстрактных Машин Состояний (ASM) и среды SpecExplorer, разработанной в Microsoft Research.
Введение В первой части данной статьи описывается фор усложнением программного обеспечения ус мализм абстрактных машин состояний и его реали ложняются и подходы к разработке и анализу зация AsmL. Во второй части описывается методо Скорректности создаваемых продуктов. Одним логия предлагаемая средой SpecExplorer. Третья из новых подходов является использование моделей часть содержит пример AsmL модели и её деталь не только для анализа требований и архитектуры, но ное описание. В четвертой части авторы приводят и для анализа непосредственно продукта. От статиче заключение и обзор альтернативных инструментов.
ских моделей (UML, Booch и т.д.) происходит пере ход к исполняемым (executable) моделям. Целью дан Исполняемые спецификации ной статьи является описание подхода связанного Формализм абстрактных машин состояний, опи с использованием формализма Абстрактных Машин санный в [4], является чисто математическим объек Состояний (ASM) и среды SpecExplorer, разработан том. Однако структура ASM такова, что возможна ной в Microsoft Research [1]. его реализация в виде языка программирования. Су Исполняемые модели не являются совершено ществует несколько альтернативных реализаций, на новым явлением, к таким моделям можно отнести пример [7] или [8]. Основной идеей ASM является сети Петри [2], модели на языке Promela [3], и мно хранение состояния объекта как некоторого набора гие другие. Абстрактных Машин Состояний значений ассоциированных с локациями (location)1.
(в дальнейшем просто ASM) это математический Также ASM определяет механизм частичных обнов формализм, разработанный [4]. Одной из импле лений, как основной способ эволюции системы, и ментаций этого формализма в виде языка програм математическую нотацию правил, по которым изме мирования является AsmL [5;
6]. По синтаксису няются значения. Одним из ключевых моментов яв этот язык является некоторой смесью Python ляется одновременность выполнения действий.
и Visual Basic. Это объектно ориентированный, Среда SpecExplorer, разработанная в Microsoft динамический слабо типизированный язык. От Research [1], содержит реализацию ASM в виде дельно стоит отметить, что AsmL являясь.Net язы ком имеет доступ к любому совместимому с.Net 1 На данный момент не существует, канонического пере коду в т.ч. ко всем стандартным сервисам.Net вода терминов связанных с ASM. В спорных случаях анг лийский вариант термина приводится в скобках.
Framework.
56 БИЗНЕС-ИНФОРМАТИКА №4(06)Ц2008 г.
ПРОГРАММНАЯ ИНЖЕНЕРИЯ языка AsmL [.Net]. С точки зрения синтаксиса ограничениями (constraints) и поведением, какие AsmL представляет собой некий синтез языков должны быть присущи всем корректным реализа Python, Delphi и Visual Basic, и при этом содержит циям системы. Другими словами, исполняемые высокоуровневые конструкции, близкие к матема спецификации должны быть так же ясны относи тическим (определение множеств;
квантификация тельно свободы данной конкретным реализациям выражений, pattern matching). С точки зрения па системы, которая описывается, как и относительно радигмы программирования AsmL является объ ограничений.
ектно ориентированным языком, в тоже время до В качестве примера, исполняемые специфика пуская как функциональное, так и императивное ции не ограничивают порядок выполнения опера программирование. ций до тех пор, пока он не является важным, в то AsmL входит в семейство.Net языков и имеет время как сегодняшний программы реализуют по доступ к любому.Net совместимому коду. Тем не следовательный порядок выполнения операций, менее предполагается, что модели написанные на как решение уровня реализации (в отличие от уров AsmL минимально пользуются средствами не вхо ня проектирования).
дящими в язык и его стандартную библиотеку, т.к. Это можно проследить на примере:
использование внешних API сокращает возможно сти по анализу модели. Более подробно анализ var A = [3, 10, 5, 7, 1] AsmL моделей будет рассмотрен ниже. Помимо indices = {0, 1, 2, 3, 4} AsmL, SpecExplorer предлагает методологию авто матической проверки соответствия модели проек Main() тируемой системе. step until fixpoint AsmL [6] это язык для создания спецификаций choose i in indices, j in indices для программного обеспечения, основанный на where i < j and A(i) > A(j) формализме абстрактных машин состояний. Он ис A(i) := A(j) пользуется для создания понятных (human read A(j) := A(i) able), исполняемых моделей работы системы таким step образом, чтобы обеспечить минимальность и завер WriteLine(A) // prints [1, 3, 5, 7, 10] шенность, с учетом заданного уровня абстракции.
Спецификации на AsmL называются исполняемыми Листинг 1 Сортировка спецификациями. Эта исполняемая спецификация использует аб Так же, как и традиционные спецификации, ис страктную машину состояний для сортировки через полняемые спецификации являются описанием то алгоритм обмена.
го, как работают компоненты программного обеспе Машина выполняет последовательные шаги, чения. В отличие от традиционных спецификаций которые меняют местами значения А, элементы ко исполняемые спецификации имеют единственное, торого обозначаются индексами i и j, такими что i недвусмысленное значение. Это значение проявляет меньше j, и значения A(i) и A(j) не совпадают с по себя в виде абстрактной машины состояний (ASM), рядком сортировки. Это продолжается до тех пор, математической модели изменения системы, состо пока никаких дополнительных обновлений не воз яния времени выполнения (runtime state). никает, то есть, до тех пор, пока последователь Спецификации на AsmL могут быть запущены ность не станет отсортированной. Как последний как программы, например, чтобы симулировать по шаг, печатается отсортированная последователь ведение некоторой системы или проверить поведе ность. Состояние машины на каждом этапе полно ние реализации на соответствие спецификации. стью характеризуется значением последовательнос Однако предполагается, что в отличие от обычных ти A на этом шаге.
программ, исполняемые спецификации должны Эта спецификация минимальна. Первый мо быть минимальными. Другими словами, несмотря мент заключается в том, что выражение choose не на то, что они верны в описании, без упущений, говорит о том, как два индекса выбираются, только всего, что является частью на выбранном уровне то, что выбранные значения должны быть различ детализации, они эквивалентно верны в том остав ными индексами элементов, нарушающих порядок лении неспецифицированным того, что осталось за сортировки. Таким образом, многие алгоритмы рамками этого уровня детализации. сортировки, в том числе и quicksort, и пузырьковая Таким образом, в отличие от программ, испол сортировка, будут соответствовать тому, что мы няемые спецификации ограничивают себя теми указали.
БИЗНЕС-ИНФОРМАТИКА №4(06)Ц2008 г. ПРОГРАММНАЯ ИНЖЕНЕРИЯ Кроме того, наш пример не говорит о том, как Рассмотрим пример. Есть три компонента A, B, происходит операция обмена значениями. Значе C. Исходные зависимости:
ния переменных изменяются, как атомарная тран закция. Это оставляет реализации решение о том, A: [] как осуществлять последовательный обмен, напри B: [A] мер, с использованием копирования во временный C: [A, B] элемент.
Предположим, что, пользователь пытается запу Методология стить компонент C. Система должна запустить по Подход, предлагаемый средой SpecExplorer следовательно компоненты A, B и C. В случае если (Microsoft), состоит из следующих шагов: все компоненты запущены, и пользователь пытает 1. Создание высокоуровневой модели системы ся остановить компонент B, система должна снача с использованием языка AsmL (также возможно ла остановить компонент C, так как в его список за использование Spec#, но его рассмотрение выходит висимостей входит B, и только потом B. В реальной за рамки данной работы). задаче компонентом являются как отдельные про 2. Исследование поведения модели путем про граммы, так и совокупности программ, но с точки гонки по фиксированным (пользовательским) зрения предлагаемой модели данное различие несу и произвольным (автоматическим) сценариям. щественно. Выбранный уровень абстракции пред 3. Автоматическая генерация сценариев с целью полагает работу программы как взаимодействие с их дальнейшего воспроизведения. некоторым числом абстрактных компонент. В даль 4. Автоматическая проверка продукта на соот нейшем модель может быть уточнена с учетом этих ветствие модели. различий. Механизм итеративного уточнения мо делей описан в (Borger E., 2003).
Обеспечивает ожидае Целью моделирования на первоначальном этапе 1) Модель 7) Журнал мые результаты для (поведенческая проверки является фиксация требований к системе в виде спецификация) соответствия формальной спецификации и проверка результата Исследуется Spec Explorer на логическую непротиворечивость. Следующим этапом будет являться автоматическая проверка со 2) Найденные Генери сценарии Обеспечивает ответствия модели и реальной программы, что вы руют (возможные реальные 4) Тестовые ходит за рамки данной статьи.
запуски как результаты сценарии конечная машина для состояний) Запускаются Модель Визуалируются Рассмотрим модель проектируемой системы:
Класс Comp является абстракцией компонента 3) Графичес- 5) Пользо системы. Его характеристиками являются: имя кие вательская 6) Тестируемая представле- обёртка Вызывает компонента, список зависимостей (имен), а также реализация ния (API driver) текущий статус (запущен/нет).
Рис. 1 Методология SpecExplorer>
ПРОГРАММНАЯ ИНЖЕНЕРИЯ require forall d in FindDependants(name) holds not SetWillStart(n, true) FindComp(d).running step running := false Start(name) Check() as Boolean return running Листинг 4. Запуск компонента Depends(name as String) as Boolean Запуск компонента - это двухфазная операция.
return name in deps На первой фазе мы помечаем компоненты, предна значенные к запуску, на втором непосредственно Листинг 2. Класс Comp стартуем всю цепочку.
Язык AsmL поддерживает программирование по контракту, что выражается с помощью конструкций Start(name as String) require. В случае если произойдет вызов метода let c = FindComp(name) Comp.Stop в тот момент, когда компонент еще не if not c.running then запущен, система сгенерирует ошибку. Такая ошиб step ка означает, что модель внутренне не согласована, WriteLine(лStarting л + c.name) и, либо ограничение установлено неверно, либо су step ществует такая последовательность действий, кото try рая приводит к незаконному вызову Stop. Каж step дый компонент однозначно определяется своим StartSeq(c.deps) именем, причем предполагается, что двух компо step нентов, обладающих одним именем нет. Состояние if GetWillStart(name) then компонента определяется булевой переменной run c.Start() ning, означающей запущен компонент в данный else момент или нет. Допущение данной модели состоит WriteLine(лSkipped л + name + л (failed dependency)) в том что, предполагается если сбой возникает, то catch он возникает в момент запуска компонента. Удачно e as Exception:
стартовавший компонент в дальнейшем работает Failed(name) стабильно. Как видно из кода функции Comp.Start при запуске компонента возможен сбой. В этом StartSeq(l as Seq of String) случае генерируется исключение. Предусловиями require AllowedSequence(l) для запуска компонента являются утверждения: var i = 1. Он не запущен. step while i < Size(l) 2. Все компоненты, от которых он зависит, рабо Start(l(i)) тают. i += Известные компоненты описываются следую щей последовательностью: Листинг 5. Запуск компонента (продолжение) Как видно из метода Start(name as String) на вы var components as Seq of Comp = [ соком уровне состояние компонента проверяется во new Comp(лcore, []), время исполнения (runtime). Вкупе с требованием new Comp(лmv, [лcore]), чтобы Comp.Start вызывался для не запущенных new Comp(лlogo, [лcore, mv]), компонентов, обеспечивается проверка утвержде new Comp(лautomation, [лcore]), ния что ни один компонент не будет запущен дваж new Comp(лnxos, [лcore])] ды. В противном случае в процессе автоматического исследования (exploration) модели будет сгенериро Листинг 3. Список компонентов вано исключение. Причем исключение сгенериро Теперь определим высокоуровневые действия, ванное нарушением контракта всегда останавливает применимые к системе: выполнение модели, в отличие от пользовательских исключений, таких как в методе Comp.Start.
[Action] Вспомогательная функция AllowedSequence StartA(name as String) проверяет упорядоченную последовательность let c = FindComp(name) компонентов на предмет непротиворечивости, т.е.
step отсутствие компонентов, которые могли бы быть forall n in c.deps + [name] запущены прежде своих зависимостей.
БИЗНЕС-ИНФОРМАТИКА №4(06)Ц2008 г. ПРОГРАММНАЯ ИНЖЕНЕРИЯ function AllowedSequence(l as Seq of String) as Boolean if c.running then return forall i in Indices(l), j in Indices(l) Stop(l(i)) where i < j i += holds not (l(j) in GetDependencies(l(i))) [Action] Stop(name as String) Листинг 6 Функция AllowedSequence let c = FindComp(name) Как можно видеть из кода этой функции язык require c.running AsmL допускает формулирование условий практи step чески в математической форме (для любых i и j из StopSeq(FindDependants(name)) множества Indicies(l), таких что i < j, выполняется step условие). c.Stop() Чтобы завершить тему запуска компонентов приведем два оставшихся высокоуровневых метода, Листинг 8. Остановка компонентов которые являются отражением исходных требова В данной спецификации использовались вспо ний к системе. Метод StartAll предназначен для за могательные функции, приведенные в Листинг 9.
пуска всех известных компонентов. Метод StartDefault предназначен для запуска некоторого var start_ini as Seq of Boolean = [ подмножества компонентов, которое в реальных true, // core условиях будет задаваться конфигурационным true, // multiviewer файлом. false, // logo_inserter false, // automation [Action] true] // nxos StartAll() require forall c in components holds not c.running var will_start as Seq of Boolean = [ step false, forall c in components false, SetWillStart(c.name, true) false, step false, var i = 0 false] step while i < Size(components) Start(components(i).name) function FindComp(name as String) as Comp i += 1 return the c | c in components where c.name = name [Action] StartDefault() function IsRunning(name as String) as Boolean require forall c in components holds not c.running return FindComp(name).running step forall ci in Indices(components) where start_ini(ci) function GetDependencies(name as String) as Seq of String SetWillStart(components(ci).name, true) return FindComp(name).deps step StartSeq([components(c).name | c in IndexRange(compo- function FindDependants(name as String) as Seq of String nents) where start_ini(c)]) return [c.name | c in components where exists dep in c.deps Листинг 7. Групповой запуск компонентов where dep = name] Помимо запуска компонентов система должна предоставлять возможность остановки уже запу SetWillStart(name as String, val as Boolean) щенных компонентов причем, в случае если оста let index = the ci | ci in Indices(components) where compo навливается компонент от которого зависят другие nents(ci).name = name запущенные, остановить нужно всю цепочку. will_start(index) := val StopSeq(l as Seq of String) function GetWillStart(name as String) as Boolean var i = 0 let index = the ci | ci in Indices(components) where compo step while i < Size(l) nents(ci).name = name let c = FindComp(l(i)) return will_start(index) 60 БИЗНЕС-ИНФОРМАТИКА №4(06)Ц2008 г.
ПРОГРАММНАЯ ИНЖЕНЕРИЯ PrintComponents(l as Seq of Comp) Write(лComponents: л) Write([c.name | c in l]) WriteLine(л.) Листинг 9. Вспомогательные функции.
Исследование модели При исследовании модели Spec Explorer был сконфигурирован следующим образом:
Рис. 4 Граф состояний в реальной системе участвует большее количество компонентов и результирующий граф слишком ве лик, чтобы быть приведенным в иллюстрации.
Несмотря на небольшое число компонентов граф, представленный на рисунке Граф состояний, яв ляется срезом полного графа. Полный граф состоя ний, сгенерированный SpecExplorer приводится на рис. 5 Полный граф состояний - Заключение Приведенные выше выкладки демонстрируют, Рис. 2 Настройка действий как формализм ASM может быть применен для фиксации требований и проверки их на непротиво речивость. Построена модель программной систе мы и продемонстрированы способы автоматичес кого исследования (exploration) этой модели. Выде лены некоторые ключевые моменты подхода ASM, такие как одновременность вычисления выраже ний, последовательные обновления, кодирование состояния с помощью значений переменных. Так же продемонстрированы некоторые возможности среды SpecExplorer, разработанной в Microsoft Research. Следующим шагом будет являться по строение обертки (API Driver) для реальной систе мы с целью автоматической проверки соответствия модели системе.
Рис. 3 Настройка области исследования Язык AsmL существует не только в виде части SpecExplorer, но также доступен в виде open source Группировка running определяется следующим компилятора, расположенного на ресурсе CodePlex AsmL выражением: [9].
Существуют также альтернативные реализации [c.name | c in components where c.running] ASM такие как CoreASM [7] и его предшественник ASM SL (реализованный в инструменте Листинг 10 Группировка состояний AsmWorkbench [8]), а также AsmGofer [10], реализу Автоматическое исследование модели привело ющий семантику ASM как подмножество языка к следующему графу состояний (рис. 4): Haskell.
Количество компонентов в данном графе сокра Исследования проводились при поддержке щено до трех с целью повышения наглядности, фонда РФФИ, грант 07 07 00058 а.
БИЗНЕС-ИНФОРМАТИКА №4(06)Ц2008 г. ПРОГРАММНАЯ ИНЖЕНЕРИЯ 62 БИЗНЕС-ИНФОРМАТИКА №4(06)Ц2008 г.
Рис. 5.
Полный граф состояний ПРОГРАММНАЯ ИНЖЕНЕРИЯ Литература 1. Foundations of Software Engineering. Online: // 2008.
2. Cheung K, Cheung T, Chow K, A petri-net-based synthesis methodology for use-case-driven system design//Journal of Systems and Software, 2006, 79 Issue 6, С. [772Ц790].
3. Del Mar Gallardo M, Merino P, Pimentel E, A generalized semantics of PROMELA for
Abstract
model checking//Formal Aspects of Computing, 2004, 16 Issue 3, С. [166Ц193]..
4. Borger E, Stark R, Abstract State Machines. A Method for High-Level System Design and Analysis, Springer-Verlag, 2003, 448 p.
5. Gurevich Y, Rossman B, Schulte W. Semantic Essence of AsmL: Extended Abstract. In Springer Lecture Notes in Computer Science. Vol.
3188. 2004.
6. The AsmL webpage. Online: // 2008.
7. Farahbod R, Gervasi V, Glasser U, Memon M, Design and Specification of the CoreASM Execution Engine // 2006, SFU-CMPT-TR-2006-09, [58] 8. Del Castillo G. The ASM Workbench. A Tool Environment for Computer-Aided Analysis and Validation of Abstract State Machine Models.
Heinz Nixdorf Institut, Universit?t Paderborn. 2001.
9. AsmL Compiler. Online: // 2008.
10. AsmGofer project page. Online: // 2008.
Яковлев А.А.
АГЕНТЫ МОДЕРНИЗАЦИИ Второе издание ISBN 978-5-7598-0460- 432 с.
60х88/ Экономическое развитие и процессы модернизации, в коночном счёте, Переплёт зависят не от темпов инфляции, валютного курса, размеров Стабилизационного 2007 г.
фонда и даже не от цен на нефть. Все эти макроэкономические параметры важны постольку, поскольку они могут пoвлиять на поведение экономических агентов.
Их предпочтения, их желание (или нежелание) инвестировать в развитие бизнеса и повышать эффективность собственных компаний предопределяют конкурентоспособность собственной экономики и динамику уровня жизни населения.
В этой книге на примере четырех явлений, которые до недавнего времени были своего рода символами российской экономики (лчерный нал, бартер и неплатежи, массовые нарушения прав акционеров и челночная торговля), показано, почему российские предприятия в 1990-е гг. вели себя совсем не так, как того ожидали российское правительство и эксперты из МВФ и Всемирного банка. На обширном эмпирическом материале в книге объясняются мотивы действий экономических агентов, которые внешнему наблюдателю часто казались иррациональными, но на самом деле были вполне логичными в условиях сложившихся иррациональных правил игры.
Что изменилось в 2000-е гг.? Кто сегодня заинтересован в создании правильных стимулов для предприятий? Как можно ускорить модернизацию предприятий и тем самым способствовать модернизации российской экономики?
Ответы на эти вопросы даются с учётом дела ЮКОСа и иных последних событий в социально-политической жизни России. Большое внимание в книге уделено возможностям применения в наших условиях опыта других стран, имеющих сопоставимый с Россией уровень развития институтов государства и рынка и сумевших добиться значимых успехов в своём социально экономическом развитии.
Для широкого круга читателей, интересующихся проблемами экономической политики и управления предприятиями в переходной экономике.
БИЗНЕС-ИНФОРМАТИКА №4(06)Ц2008 г.
Книги, научные публикации