Формальная спецификация и верификация. Задача о спящем парикмахере

 

Основные типы данных спецификации в SDL - предопределенные и конструируемые типы данных (массив, последовательность и т.д.). Формулы описываются с помощью предикатов, булевых операций, кванторов, переменных и модальностей. Семантика их определения зависит от последовательных действий (поведений), спецификацией процесса и от момента времени их выполнения.

2. Перспективные направления верификации программ

По статистическим данным ежегодно ошибки в ПО США обходятся в 60 млрд. долларов. Для преодоления этих проблем американские специалисты и специалисты из европейских стран по формальным методам и спецификациям программ приняли решение поставить теоретические достижения в этой области на производственную основу. Этому решению предшествовали результаты исследований по формальной верификации моделей ПрО и обращений к функциям на языке API проекта SDV фирмы Microsoft, а также проверка безопасности и целостности БД и др. Кроме того, начали активно применяться формальные языки спецификации (RAISE, Z, VDM и др.) для разработки приложений. В 2005 г. был сформулирован международный проект по формальной верификации ПО.

Идея создания этого проекта  принадлежит Т.Хоару, она обсуждалась  на симпозиуме по верифицированному  ПО в феврале 2005 г. в Калифорнии. Затем  в октябре того же года на конференции IFIP в Цюрихе был принят международный проект сроком на 15 лет по разработке "целостного автоматизированного набора инструментов для проверки корректности ПС".

 

В нем сформулированы следующие  основные задачи:

 

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

 

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

В связи с тем, что комитет  ISO/IEC в рамках стандарта ISO/IEC 12207:2002 провел стандартизацию процессов верификации и валидации ПО и, учитывая цель проекта, проблема создания автоматизированного набора инструментов и репозитария для проверки корректности разных объектов программирования является перспективной.

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

 

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

 

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

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

 

2. Задача о спящем парикмахере

В парикмахерской 5 мест в очереди и одно в кресле парикмахера. Клиент заходит в парикмахерскую, если у него свободно, посетитель садится в кресло, остальные ждут в очереди. Если у парикмахера занято, клиент садится в очередь в зале. Если в зале мест нет, клиент уходит. Если парикмахер ждёт больше определённого времени, он засыпает. Смоделировать процесс с помощью сетей Петри и реализовать на одном из языков программирования.

2.1. Реализация задачи с помощью сетей Петри 

Общий принцип работы сетей Петри:

 

Переходы

Места (зал ожидания, место у парикмахера)

 

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

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

 

Рис. 1.2. Реализация алгоритма с помощью сетей Петри

Конечный автомат

A = (V,Q,R,q₀,I), где V – алфавит конечного автомата,

Q – конечное не пустое множество состояний,

R – множество заключительных состояний,

q₀ – начальное состояние,

I  - программа автомата,

V - множество допустимых символов, которые могут быть поданы на вход автомата.

Конечный автомат можно представить  как машину Тьюринга, но имеющую  следующие особенности:

 

• выделены заключительные состояния,
• машина считывает символы с входной ленты ничего на неё не записывая,
• на каждом шаге автомат, считав символ с ленты и перейдя в новое состояние, обязательно передвигается на один символ вправо,

автомат останавливается в случае достижения конца слова.

Конечный автомат на примере  клиента парикмахерской

 

1. Клиент вошёл в парикмахерскую
2. Сел на скамейку в зале ожидания
3. Сел в кресло парикмахера (подстригается)
4. Уходит

 

Описание алгоритма

В случае если клиент пришел и в  зале есть место, срабатывает первый переход (забирает фишку - занимает место  в зале ожидания), в противном  случае клиент уходит. В случае если парикмахер свободен, клиент идет стричься и отдает место в зале (возвращает фишку) - срабатывает второй переход (забирает фишку – садится в кресло парикмахера), иначе он ждет. Если клиент подстригся, он уходит и освобождает кресло у парикмахера (возвращает фишку).

 

2.2. Реализация алгоритма в Delphi

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

При создании формы в первом листинге с помощью функции CreateProcess() создаётся объект ядра – процесс – «парикмахер». Далее, в процедуре Timer, создаётся несколько процессов «клиент», после чего синхронизация созданных процессов осуществляется таким образом. При создании процесса «парикмахер» создаются два семафора («кресло» и «зал ожидания»). В процедуре Timer мы сканируем семафор на наличие клиента в кресле парикмахера. Если поиск успешен, выводится сообщение о том, что парикмахер стрижет. Иначе – сообщение о том, что клиентов нет. В процедуре Timer есть счётчик ожидания: если значение счётчика по своей величине превзошло 5, выводится сообщение о том, что парикмахер заснул. Работа с двумя созданными семафорами ведется в процессе «клиент». В процедуре Timer этого процесса вызывается функция OpenSemaphore() для обоих семафоров, после чего клиент проходит в зал ожидания (счётчик семафора уменьшается на единицу), если функция WaitForSingleObject() вернёт значение «истина» (т.е. в зале ожидания ещё есть места). Если функция WaitForSingleObject() возвращает значение «ноль», то завершаем работу процессов «клиент». Из зала ожидания клиент, дождавшись освобождения семафора, с помощью функции WaitForSingleObject() переходит в кресло парикмахера. При этом с помощью функции ReleaseSemaphore() освобождается место в зале. После подстрижки клиент освобождает кресло парикмахера (ReleaseSemaphore()) и уходит (завершение процесса).

 

2.3. Листинг

2.3.1. Основная программа для запуска парикмахера и клиента

 

unit Main;

interface

uses

  Windows, Messages, SysUtils, Classes, Graphics, Controls, Forms, Dialogs,

  StdCtrls, ExtCtrls;

type

  TForm1 = class(TForm)

    Button1: TButton;

    Button2: TButton;

    Timer1: TTimer;

    procedure Button1Click(Sender: TObject);

    procedure Timer1Timer(Sender: TObject);

    procedure Button2Click(Sender: TObject);

    procedure FormCreate(Sender: TObject);

  private

    { Private declarations }

  public

    { Public declarations }

  end;

 

var

  Form1: TForm1;

implementation

{$R *.DFM}

 

procedure TForm1.Button1Click(Sender: TObject);

var lpStartupInfo:TStartupInfo;

    lpProcessInformation:TProcessInformation;

begin

   FillChar(lpStartupInfo,Sizeof(lpStartupInfo),#0);

   lpStartupInfo.cb:=SizeOf(lpStartupInfo); 

   if not CreateProcess(nil,PChar('Parik'),nil,nil,False,0,nil,nil,lpStartupInfo,lpProcessInformation) then

     begin                                              

       ShowMessage('Ошибка создания парикмахера');

       exit;

     end;

   timer1.Enabled:=true;

end;

 

procedure TForm1.Timer1Timer(Sender: TObject);

var lpStartupInfo:TStartupInfo;

    lpProcessInformation:TProcessInformation;

begin

   FillChar(lpStartupInfo,Sizeof(lpStartupInfo),#0);    

   lpStartupInfo.cb:=SizeOf(lpStartupInfo);

   if random>0.5 then                                  

      if not CreateProcess(nil,PChar('Man'),nil,nil,False,0,nil,nil,lpStartupInfo,lpProcessInformation) then

         begin                                                     

ShowMessage('Ошибка создания посетителя');

           exit;

         end;

end;

 

procedure TForm1.Button2Click(Sender: TObject);

begin

close;

end;

 

procedure TForm1.FormCreate(Sender: TObject);

begin

Form1.Left:=0;

Form1.Top:=0;

end;

end.

2.3.2. Парикмахер

unit hairdresser;

interface

uses

  Windows, Messages, SysUtils, Classes, Graphics, Controls, Forms, Dialogs,

  StdCtrls, Buttons, ExtCtrls;

 

type

  TForm1 = class(TForm)

    Memo1: TMemo;

    Timer1: TTimer;

    Image1: TImage;

    Button1: TButton;

    procedure FormCreate(Sender: TObject);

    procedure Timer1Timer(Sender: TObject);

    procedure Button1Click(Sender: TObject);

  private

    { Private declarations }

  public

    { Public declarations }

  end;

 

var

  Form1: TForm1;

  room,work:thandle;

  count:integer;

  workhear:thandle;

implementation

{$R *.DFM}

 

procedure TForm1.FormCreate(Sender: TObject);

begin

form1.Left:=500;

form1.Top:=0;

room:=CreateSemaphore(nil,4,4,'WaitRoom');

work:=CreateSemaphore(nil,1,1,'WorkRoom');

memo1.Lines.Add('Начало рабочего дня!');

 count:=0;                         

 Timer1.Enabled:=true;             

end;

 

procedure TForm1.Timer1Timer(Sender: TObject);

var

  Find_client:thandle;

begin

workhear:=OpenSemaphore(SYNCHRONIZE+EVENT_MODIFY_STATE,false,'WorkRoom');

  if WaitForSingleObject(workhear,1)=WAIT_OBJECT_0 then

    begin

      ReleaseSemaphore(workhear,1,nil);

      count:=count+1;

      if count>5 then

        begin

          memo1.Lines.Clear;

          image1.Picture.Graphic.LoadFromFile('sleep.bmp');

          memo1.Lines.Add('Сплю');

        end

      else

        begin

          memo1.Lines.Clear;

          image1.Picture.Graphic.LoadFromFile('smoke.bmp');

          memo1.Lines.Add('Отдыхаю');

        end;

    end

  else

    begin

      count:=0;

      memo1.Lines.Clear;

      image1.Picture.Graphic.LoadFromFile('work.bmp');

      memo1.Lines.add('Работаю');

    end;

  closehandle(workhear);

end;

 

procedure TForm1.Button1Click(Sender: TObject);

begin

close;

end;

end.

2.3.3. Клиент

unit hairy;

interface

uses

  Windows, Messages, SysUtils, Classes, Graphics, Controls, Forms, Dialogs,

  StdCtrls, ExtCtrls;

 

type

  TForm1 = class(TForm)

    Memo1: TMemo;

    Timer1: TTimer;

    procedure FormCreate(Sender: TObject);

    procedure Timer1Timer(Sender: TObject);

  private

    { Private declarations }

  public

    { Public declarations }

  end;

 

var

  Form1: TForm1;

    workhear:thandle;

    roomhear:thandle;

implementation

{$R *.DFM}

 

procedure TForm1.FormCreate(Sender: TObject);

begin

  randomize;

  form1.Top:=random(screen.Height-300)+125;

  form1.Left :=50;

  memo1.Lines.Add('Пришёл');

  Timer1.Enabled:=true;

end;

 

procedure TForm1.Timer1Timer(Sender: TObject);

  begin

roomhear:=OpenSemaphore(SYNCHRONIZE+EVENT_MODIFY_STATE,false,'WaitRoom');

workhear:=OpenSemaphore(SYNCHRONIZE+EVENT_MODIFY_STATE,false,'WorkRoom');

  if WaitForSingleObject(roomhear,2000)=WAIT_OBJECT_0 then

     begin

       form1.Left:=300;

       memo1.Lines.Clear;

       memo1.Lines.Add('Жду в очереди');

       if ((WaitForSingleObject(workhear,infinite)=WAIT_OBJECT_0)) then

         begin

           ReleaseSemaphore(roomhear,1,nil);

           memo1.Lines.Clear;

           form1.Left:=550;

           memo1.Lines.Add('Подстригаюсь');

           sleep(2000);

           ReleaseSemaphore(workhear,1,nil);

           form1.Left:=800;

           memo1.Lines.Clear;

           memo1.Lines.Add('Подстрижен');

           sleep(1000);

           closehandle(roomhear);

           closehandle(workhear);

           close;

         end;

     end

  else

     begin

       memo1.Lines.Clear;

       form1.Left:=0;

       memo1.Lines.Add('Опоздал');

       sleep(500);

       close;

     end;

end;

end.

 

Список литературы

1. Лаврищева Е.М., Петрухин В.А. Методы и средства инженерии программного обеспечения. 2006 г.
2. П.Грогоно, Программирование на языке Pascal, М.:Мир, 1982, с.295, (Тестирование и верификация)
3. codenet.ru
4. ru.wikipedia.org
5. www.refodrom.ru