Методы и средства инженерии программного обеспечения

       

Формальные методы


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

                                                                                   

За многие годы своего существования (более 20–лет) такие известные формальные методы, как VDM, Z, RAISE [43–46]  используются редко, эпизодически в реальных проектах, более всего в университетских и академических организациях и до промышленного производства фактически не дошли.

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

Наука формального проектирования ПС получила значительный прогресс при создании обобщенного UML, который доведен до стандарта, отодвинув на второй план такие средства спецификации, как RAISE, VDM и др.

Далее рассматриваются некоторые техники спецификации моделей  программ и методы формального доказательства.

 

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

Каждому модулю модели соответствует сервис как provider, так и потребителя (consumer) услуг. Дуга графу от модуля M к N определяет интерфейс, который может предоставлять модуль N для  модуля M.

Базисом формального метода представления модели есть спецификация интерфейсов модулей для двух выше указанных пользователей сервисов.
Интерфейс удовлетворяет следующим свойствам:

– разделенность  (separable) модулей с точки зрения проектирования и спецификации, интерфейс которых не требует описания среды модуля;

– композиционность  (сомроsіtіоn),  когда модули  соединяются через  композиционную теорию в систему  с гарантированными связями между ними.

Данная теория базируется на модели интерфейса для взаимодействия  модулей системы между собою через сетевые  протоколы (TCP, UDP и др.). Каждый протокол  передает разным модулям этой модели  параметры  для нахождения нужного сервиса.

 Модель интерфейса задает связь модуля со средой в виде дискретного   события (event), которое возникает только тогда, когда модуль и среда  действуют вместе, и создают  событие, рассматриваемое со стороны  интерфейса. Иными словами, интерфейс  специфицируется  в виде  множества  последовательностей  событий для наблюдения за поведением  модулей модели.



        

Предположим, что S определяет спецификацию модуля  M, которая включает в себя все возможные случаи его поведения и  задает разные ситуации, которыми могут быть:

– событие интерфейса или состояние наблюдателя системы;

– анализ  является  конечным или представлен неопределенной последовательностью;

– формализм определения этой последовательности;

– условия  выполнения события.

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

Формальный метод и спецификация  RAISE.   RAISE– метод и RSL–спецификация (RAISE Spesification Language)  [45, 46]  были разработаны в 1985–1998гг. как результат предварительного исследования формальных методов. Метод содержит нотации, техники и инструменты  для использования формальных методов  при конструировании ПС и доказательстве их правильности.  Метод имеет программную поддержку  в виде набора инструментов и методик, которые постоянно  развиваются и используются для конструирования и  доказательства правильности программ.


описанных в RSL и ЯП (С++ и Паскаль).

Язык RSL содержит абстрактные параметрические типы данных (алгебраические спецификации)  и конкретные типы данных  (модельно–ориентированные), подтипы,  операции для задания последовательных и  параллельных программ, предоставляет аппликативный и императивный стиль спецификации абстрактных программ, а также  формальное конструирование программ в других ЯП  и доказательства их правильности. Синтаксис этого языка близок  к синтаксису  языков С++ и Паскаль.

В  RSL–языке имеются предопределенные абстрактные типы данных и конструкторы сложных типов данных, такие как произведение (product), множества (sets), списки (list), отображения (map), записи (record) и т.п. Далее рассмотрим, для примера,   некоторые конструкторы сложных типов данных.

1. Произведение типов – это упорядоченная конечная последовательность типов   Т1, Т2 , …, Тn   произведения  (product)  Т1 ´ Т2 ´, …, ´ Тn  .  Представитель типа имеет вид (v1, v2 , …, vn ), где каждое  vi    есть значением типа   Тi.  Компонент произведения можно   получить get и переслать set, т.е.

            get component  (i, d) = getvalue (i, d),

            set  component  (d, i, val)  = d ÞÑ  (I ® val).

Количество компонентов  произведения d  находится таким образом:

            size (d) = id  Ñ (null (couter  inc(counter))).

Конструктор произведения d1 и d2  строит произведение d1 ´ d2   вида

         product  (d1 , d2  ) =  id Ñ (size (d1)  Þ couter 1)  Ñ (null (couter 2) inc couter 2))).

Для каждого конкретного типа product (Т1 ´Т2

´, …, ´ Тn) можно построить конструктор значения этого типа из отдельных компонентов произведения  таким образом:

            make product (value 1, …, value n) = (value i Þ 1)  Ñ… Ñ  (value n Þ n),

где каждое значение value i  имеет тип Тi  ,  а результирующее значение – тип произведения Т1 ´Т2 ´, …, ´ Тn .



2.  Списки типов – это последовательность значений одного типа списка list Т,  могут быть конечным списком типов Тk  и неконечными списком типов T n . в качестве структур данных типа списку может быть бинарное дерево, в котором  есть голова  (head) и сын ( tail), следует за ним в списке и  хвост. Операциями  для списка  является операция hd взятия первого элемента списка, т.е. головы  и операция  tl – хвоста остальные элементы. 

Функция   Caddr (I) = L  Þ tail  Þtail  Þ Head   выбирает из списка I –элемент.        Индекс элемента помогает выбрать нужный элемент списка        Index(I, idx) =  L (idx) =

        while (Ø is null(idx))do((L  Þ tail  ÞL) Ñdec(idx)) L  Þ Head. Для определения количества элементов в списке выполняется функция

         len (L) = (ld Ñ null (result))

         while (L  Þ) do (( L  Þ tail  Þ tail  ÞL) Ñ inc (result))

         result Þ

 Элемент списка  находится так:

           elem (L) = (ld Ñ empty (result))

          while (L  Þ) do (( L  Þ tail  ÞL) Ñ

           ( result ­ ( LÞ head Þ) Þ elem ) Þ result)

          result Þ.

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

3. Отображение – это структура (map), которая ставит в соответствие значениям одного типа значение другого типа. С другой стороны, отображение  является бинарным отношением  декартового произведения двух множеств, как совокупности  двухкомпонентных пар, в которой  первый компонент  arg  содержит  элементы аргументов отображения, а другой  компонент  res  соответствующие элементы значений этого отображения. 

В языке представлены разные допустимые операции  над отображениями: наложение,  объединение,  композиция,  срез  и др. Среди этих видов отношений рассмотрим только композицию отображений.(m1, m2).

     (ld Ñ (compose (m1, m2) Þ m)) apply (m, elem)



      apply to composition (m1, m2, elem) =

       (ld Ñ (image (elem, m1) Þ s) restrict  (m2, s) Þ map

       (ld Ñ (map  getname  elem Þ name)) getvalue (name,  map).

При этом используются функции:

     Apply (m, elem) = image (elem, m)  elem Þ,

     Apply (m, elem) = getvalue (elem, m)  elem Þ.

4. Запись – это совокупность именованных полей. Этот тип соответствует типу record в языке Паскаль и struct   в языке С++. В языке RAISE определено два конструктора типа, record, shurt record, которые описываются в виде – type  record id =

        type mk_id (short _record id ) ::=

        destr_id1 : type_expr1 « recon_id

                 . . .

       destr_idn : type_exprn « recon_id.

Идентификатор  mk_id является конструктором типа  record, для которого даны деструкторы destr_idn , как функции получения значения компонентов записи.

5. Объединение  – это конструктор Union,   обеспечивающий объединение  типов

         type id = id1 , id2 ,…,  idn

при котором  тип id  получает одно из значений в списке элементов.

Конструктор этого типа имеет вид:

          type id =  id_from_ id1 (id_to_ id1: id1) ½… ½ id_from_ idn (id_to_ idn: idn)/

Операции над самим типом не определены  в языке RAISE.

Рассмотренные формальные структуры данных языка RAISE позволяет математически описывать и конструировать новые структуры данных в проектируемых программах.  Их проще проверять на правильность  методами верификации. 


Содержание раздела