�ݺ�ߣ

Верификация Опыт встраивания верификатора NuSMV в систему IronHand Докладывает : Большаков О.С. Рыбинск, 2010

Верификация – анализ корректности программных систем относительно спецификации, в которой задаются исследуемые свойства. Виды верификации: тестирование метод доказательства теорем (theorem proving) метод проверки модели (model checking).

Model Checking (проверка модели) Общая схема

Верификаторы : CPN-Tools ( C PN Group, University of Aarhus) - Модель представляется в виде сетей Петри - Только графическая оболочка - Медленная работа Spin ( Bell Labs ) - Текстовый язык Promella - Open Source NuSMV (Carnegy Mellon University)

NuSMV (New Symbolic Model Verifier) Open Source (GNU LGPL) Написан на ANCI C, совместим с POSIX ( Portable Operating System Interface for Unix ) Продолжение закрытого верификатора SMV (Carnegy Mellon University) Входной язык – текстовый язык SMV Возможность задания модели в виде синхронных / асинхронных конечных автоматов

Схема верификации c NuSMV

Пример модуля на SMV MODULE main VAR request : boolean; state : { ready, busy } ; ASSIGN init(state) := ready; next(state) := case state = ready & request = 1 : busy; 1 : { ready, busy } ; esac;

Модель двоичного счетчика Рассмотрим модель счетчика от 000 до 111 и так далее по циклу Для этого организуем систему из трех счетчиков в связь через переносы бита carry_in :

Модель двоичного счетчика MODULE counter_cell(carry_in) VAR value : boolean; ASSIGN init(value) := 0; next(value) := (value + carry_in) mod 2; DEFINE carry_out := value & carry_in; MODULE main VAR bit0 : counter_cell(1); bit1 : counter_cell(bit0.carry_out); bit2 : counter_cell(bit1.carry_out);

MODULE counter_cell(carry_in) VAR value : boolean; ASSIGN init(value) := 0; next(value) := (value + carry_in) mod 2; DEFINE carry_out := value & carry_in; MODULE main VAR bit0 : process counter_cell(1); bit1 : process counter_cell(bit0.carry_out); bit2 : process counter_cell(bit1.carry_out);

MODULE counter_cell(carry_in) VAR value : boolean; ASSIGN init(value) := 0; next(value) := (value + carry_in) mod 2; DEFINE carry_out := value & carry_in; FAIRNESS running MODULE main VAR bit0 : process counter_cell(1); bit1 : process counter_cell(bit0.carry_out); bit2 : process counter_cell(bit1.carry_out);

Темпоральные логики Темпоральная логика – модальная логика, позволяющая формализовать высказывания, зависящие от времени LTL (Linear Tree Logic) CTL (Computation Tree Logic)

Темпоральные логики LTL - спецификация: -- FUTURE X ltl_expr -- ne X t state G ltl_expr -- G lobally F ltl_expr -- F inally ltl_expr U ltl_expr -- U ntil ltl_expr V ltl_expr -- releases -- PAST Y ltl_expr -- previous state Z ltl_expr -- not previous state not H ltl_expr -- H istorically O ltl_expr -- O nce ltl_expr S ltl_expr -- S ince ltl_expr T ltl_expr -- T riggered

Темпоральные логики CTL - спецификация: EG ctl_expr -- Exists Globally EX ctl_expr -- Exists neXt state EF ctl_expr -- Exists Finally AG ctl_expr -- forAll Globally AX ctl_expr -- forAll neXt state AF ctl_expr -- forAll Finally E [ ctl_expr U ctl_expr ] -- Exists until A [ ctl_expr U ctl_expr ] -- forAll until

Списки Команд Фрагмент списков команд

Формат спецификации Если МП-11.Стол.Поднят И МП-11.ВерхняяРука.Выдвинута ИЛИ МП-11.НижняяРука.Выдвинута И МП-9С.Стол.Поднят И МП-9С.Рука.Выдвинута Не возникает МП-11.Стол.Поворот ИЛИ МП-9С.Стол.Поворот Интуитивное задание проверяемого свойства:

Декомпозиция системы на модули

Схема кода на SMV -- i- ый модуль MODULE Modulei(tact_num) VAR st: 0..100; ASSIGN init(st) := 0; next(st) := case … . 1 : st; esac; FAIRNESS running

Схема кода на SMV - - Счетчик тактов MODULE MTactCounter(st0, st1, …, sti, stn) VAR tact_num : 0..300; cycle_num : 0..300; ASSIGN init(tact_num) := 1; next(tact_num) := case tact_num = 1 & st1 = … & st2 = … & … & stn = … : 2; tact_num = 2 & st1 = … & st2 = … & … & stn = … : 3; tact_num = m : m+1; 1 : tact_num; esac; init(cycle_num) := 0; next(cycle_num) := case … esac; FAIRNESS running

Схема кода на SMV // главный модуль MODULE main VAR tactCounter : process MTactCounter(m0.st, m1.st, …mi.st, … mn.st); m0 : process Module0(tactCounter.tact_num); m1 : process Module1(tactCounter.tact_num); … mi : process Modulei(tactCounter.tact_num); … mn : process Modulen(tactCounter.tact_num); FAIRNESS running

Задание спецификации SPEC AG ! ( ( m 1. st >= 0 & m 1. st <= 5) & ( m 2. st >= 7 & m 2. st <= 10) ) Пример задания свойства:

Верификация в IronHand

Спасибо за внимание!

�ݺ�ߣ

верификация

Recommended

More Related Content

What's hot (20)

Viewers also liked (20)

Similar to верификация (20)

More from Alexander Petrov (20)

верификация