Форум АСУ в Україні

форум з автоматизації для викладачів, студентів та спеціалістів
Сьогодні: 12 листопада 2019, 21:08

Часовий пояс UTC + 2 годин [ DST ]




Створити нову тему Відповісти  [ 11 повідомлень ]  На сторінку 1, 2  Далі
Автор Повідомлення
 Тема повідомлення: Model checking - метод верифікації ПЗ
ПовідомленняДодано: 01 жовтня 2014, 19:38 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
Model Checking

Основа методу верифікація описана тут:
E. Clarke, Jr., O. Grumberg, D. Peled, Model Checking, The MIT Press, 1999. (Російський переклад тут http://www.twirpx.com/file/1231649/)
Clarke_Grumberg_Peled_ModelChecking написав:
Проверка на модели (Model Checking) — это автоматический метод верификации параллельных систем с конечным числом состояний. Он обладает рядом преимуществ по сравнению с традиционными подходами к задаче верификации, основанными на моделировании, тестировании и дедуктивном анализе.
https://ru.wikipedia.org/wiki/%D0%9F%D1 ... 0%B5%D0%B9
Верификация программ на моделях Лекция №2 Моделирование программ Константин Савенков (лектор)
Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем
Миронов А.М. Верификация программ методом Model Checking.
Верификаия программ и темпоральные логики
Захаров. Формальная верификация методом проверки моедлией
Clarke_Grumberg_Peled_ModelChecking написав:
Процесс верификации моделей программ
Применение метода проверки на модели состоит из нескольких этапов, каждый из которых подробно рассматривается в
соответствующих разделах этой книги.
Моделирование
Первая задача заключается в приведении проектируемой системы к такому формальному виду, который был бы приемлем для
инструментальных средств верификации моделей программ. Во многих случаях это просто задача компиляции. В других случаях, при ограничениях по времени и объему памяти, моделирование может потребовать абстракции, чтобы избавиться от несущественных деталей, не относящихся к делу.
Спецификация
Перед проведением верификации нужно сформулировать свойства, которыми должна обладать проектируемая системы. Обычно спецификации задаются на языке формальной логики. Для аппаратуры и программного обеспечения, как правило, применяют
темпоральную логику, позволяющую описывать, как поведение системы протекает во времени.
Важным вопросом спецификации является полнота. Метод проверки на модели дает возможность убедиться, что модель проектируемой системы соответствует заданной спецификации, однако определить, охватывает ли заданная спецификация все свойства, которыми должна обладать система, невозможно.
Верификация
В идеальном случае верификация проводится полностью автоматически. Однако на практике она часто требует содействия
человека. Одной из сторон деятельности человека является анализ результатов верификации. Если результаты проверки
отрицательные, то пользователю нередко предоставляют трассу, содержащую ошибку. Она строится в качестве контрпримера для проверяемого свойства и может помочь проектировщику проследить, где возникает ошибка. В этом случае анализ ошибочной трассы может повлечь за собой модификацию системы и повторное применение алгоритма проверки на модели.
Ошибочная трасса может появиться и вследствие некорректного моделирования системы, а также в результате использования
неправильной спецификации (в таких случаях говорят о ложном опровержении). Трасса, демонстрирующая ошибку, может оказаться весьма полезной для выявления этих двух проблем. Наконец, не исключена возможность, что решение задачи верификации не будет завершено из-за большого размера модели, не позволяющего разместить ее в памяти компьютера. В таком случае, возможно, будет необходимо провести верификацию повторно, изменив параметры инструментального средства, реализующего проверку на модели, или упростив саму модель (скажем, за счет более сильной абстракции).
Image

Карпов написав:
Model checking — это совокупность моделей, приемов и алгоритмов, позволяющих проверить, что формула темпоральной логики (CTL*, CTL или LTL), выражающая некоторое свойство поведения динамической системы во времени, выполняется (является истинной) на модели системы с конечным числом состояний (структуре Крипке).


Догори
 Профіль  
 
 Тема повідомлення: Re: Model checking - метод верифікації ПЗ
ПовідомленняДодано: 04 жовтня 2014, 09:13 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
Курс + відео
http://savenkov.lvk.cs.msu.su/mc.html


Догори
 Профіль  
 
 Тема повідомлення: Re: Model checking - метод верифікації ПЗ
ПовідомленняДодано: 08 жовтня 2014, 10:09 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
Темпоральна логіка
Вікіпедія
Wiki
Захаров. Формальная верификация методом проверки моедлией
Верификаия программ и темпоральные логики
Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем
Використовується разом з булевою логікою
Цитата:
Temporal logics include
  • Interval temporal logic (ITL)
  • μ calculus. which includes as a subset
    - Hennessy-Milner logic (HML)
    - CTL*, which includes as a subset
    --- Computational tree logic (CTL)
    --- Linear temporal logic (LTL)
    --- Metric Interval Temporal Logic (MITL)
    --- Signal Temporal Logic (STL)

LTL Wiki
CTL Wiki
Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем написав:
Для верификации технических систем свойства их поведения должны быть выражены формально логическими утверждениями, которые обеспечат простую, лаконичную и недвусмысленную их запись. В этой главе показано, что обычная логика высказываний является неадекватной для формулировки утверждений о поведении технических систем, т. е. об изменении их состояний во времени. Для спецификации таких свойств необходимы логические утверждения, истинность которых зависит от времени. Соответствующие логики называются темпоральными. Достаточно мощные, выразительные и в то же время простые темпоральные логики были построены как простые расширения обычной логики высказываний.
В этой главе вводятся две темпоральные логики: LTL — темпоральная логика линейного времени, и CTL — темпоральная логика ветвящегося времени. Эти логики очень просты, что отличает действительно полезные математические модели. Формулы этих логик являются удобным языком для выражения свойств параллельных программных систем и, как частный случай, встроен
ных систем.


Догори
 Профіль  
 
 Тема повідомлення: Re: Model checking - метод верифікації ПЗ
ПовідомленняДодано: 08 жовтня 2014, 10:10 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
Модель-чекери
Модель-чекери - програми для верифікації.
NuSMV
http://conf.mirea.ru/CD2012/pdf/p5/6.pdf написав:
Для окончательной верификации используется стандартное средство NuSMV – программа с открытым исходным кодом, распространяемая по лицензии GPL (General Public License).Это средство было предложено К.Л. МакМилланом как открытая заме-
на SMV. Программа находится в открытом доступе, имеется возможность загрузки для операционных систем Windows и Linux. Предназначена для формальной верифи-кации моделей, написанных на языке SMV, а конкретно – диалекте NuSMV.


Догори
 Профіль  
 
 Тема повідомлення: Re: Model checking - метод верифікації ПЗ
ПовідомленняДодано: 10 жовтня 2014, 16:09 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
Темпоральна логіка
F (Future) - утверждение Fq истинно в момент времени t (t |=Fq ) , если для какого-то момента времени t' в будущем q станет истинным
P (Past) - утверждение Pq истинно в момент времени t (t |=Pq) , если для какого-то момента времени ' t в прошлом утверждение q было истинным.
G (Globally) - утверждение Gq истинно в момент времени t (t |=Gq) , если для любого момента времени t' в будущем утверждение q истинно
H (History) - утверждение Hq истинно в момент времени t (t |=Hq) , если для любого момента времени t' в прошлом утверждение q истинно
Зображення

X (NextTime) - утверждение Xq истинно в момент времени t , если q истинно в следующий момент t +1:
U (Until) - Утверждение pUq истинно в момент времени t , если q истинно в некоторый будущий момент времени, а во всем промежутке от момента t до t' истинно p : когда-нибудь q , а до тех пор p
Зображення

⇒ - імплікація "якщо...то"
¬ - заперечення "НЕ"
∨ - дизюнкція"АБО"
∧ - конюнкція"ТА"

-----------------------------
 всегда в будущем: Gq
 хотя бы раз в будущем: Fq
 никогда в будущем: ¬Fq
 бесконечно много раз в будущем: GFq
 с какого-то момента постоянно: FGq


Догори
 Профіль  
 
 Тема повідомлення: Re: Model checking - метод верифікації ПЗ
ПовідомленняДодано: 10 жовтня 2014, 16:57 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
Темпоральная логика линейного времени (LTL)
1) В логике линейного времени оперируют атомарными предикатами (атомарное утверждение) — это утверждение, которое может принимать истинное или ложное значение и от структуры которого мы абстрагируемся.
2) В темпоральную логику включено минимальное число темпоральных операторов - U и X, все остальные выражаются через них. Через темпоральный оператор U можно определить темпоральные операторы F и G . Поэтому операторы F и G называются "выводимыми" в логике LTL.
3)В качестве интерпретации формул темпоральной логики рассматривается дискретная во времени бесконечная линейная направленная в будущее последовательность "миров", в каждом из которых существует своя интерпретация атомарных утверждений (рис. 2.4).
Зображення
В последовательности миров время можно считать изоморфным натуральному ряду 0, 1, 2, ..., все миры в цепочке можно считать пронумерованными, и в каждом мире логические переменные (атомарные предикаты) принимают конкретные истинностные значения — либо истину, либо ложь.
Направленность последовательности миров от прошлого к будущему позволяет проводить рассуждения об относительном времени, в терминах "до" и "после". На рис. 2.4 дан пример такой интерпретации. На последовательности миров w0,w1,w2, ,wn, … … задано множество атомарных предикатов { p, q, r} . В мире w0 атомарные предикаты p и q истинны, а r — ложен, в мире w1 утверждения q и r истинны, а p — ложно, и т. п.
Как происходит переключение от одного мира к следующему, теория не рассматривает, от этого она абстрагируется.

Формула линейной темпоральной логики Ф выполняется на последовательности миров w0,w1,w2,…, если Ф истинна в начальном мире w0 этой последовательности.
Формулы LTL построены из атомарных предикатов с помощью булевых операций и темпоральных операторов.Для темпоральных формул их истинностные значения в каждом мире определяются по значениям истинности их аргументов в цепочке миров, начинающейся с этого мира.
Формула линейной темпоральной логики (Linear Temporal Logic) LTL это:
• атомарное утверждение (атомарный предикат) p,q,…;
• или формулы LTL, связанные логическими операторами , ¬ ∨;
• или формулы LTL, связанные темпоральными операторами , X U.
Прошлое в логике LTL не рассматривается.


Догори
 Профіль  
 
 Тема повідомлення: Re: Model checking - метод верифікації ПЗ
ПовідомленняДодано: 10 жовтня 2014, 17:02 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
Реагирующие системы (reactive systems)
Темпоральная логика и метод model checking используются, в основном, для спецификации свойств и верификации именно реагирующих систем. Свойства, которые интересуют разработчиков таких систем, обычно выражают возможные последовательности событий, возникающие при функционировании систем во времени.
Реагирующие системы — это класс информационных систем, основной функцией которых является поддержание взаимодействия с окружением, а не преобразование информации.
Вычисление реагирующей системы — это бесконечная последовательность состояний, которые система проходит во времени.
Поведение реагирующей системы — это все возможные ее вычисления.
Будем обозначать вычисления греческими буквами π , σ и т. п., например: σ = s0s1s2s3…. Из одного состояния в другое система переходит в некоторые дискретные моменты времени 0, 1, 2, t t t …, выполняя операции. Начальное состояние вычисления часто помечается стрелкой (рис. 2.7).
Зображення
Зображення

Если некоторая темпоральная формула истинна в состоянии s0 вычисления, то говорят, что она истинна для всего вычисления, начинающегося в этом состоянии (рис. 2.9).
Зображення
На рис. 2.9 формула qUp выполняется на всем представленном там вычислении, а формула Gr на нем не выполняется. Формула Gr выполняется на вычислении, начинающемся с s1 . Если темпоральная формула не выполняется в состоянии, то ее, как и ложный в этом состоянии атомарный предикат, не будем указывать в этом состоянии.
В качестве атомарных предикатов в реагирующих системах могут использоваться любые утверждения, принимающие значение "истина" или "ложь" в состояниях системы.


Догори
 Профіль  
 
 Тема повідомлення: Re: Model checking - метод верифікації ПЗ
ПовідомленняДодано: 10 жовтня 2014, 18:55 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
Формальное определение LTL
Истинность формулы ϕ логики LTL на вычислении 0 1 2 σ = s s s … (обозначается σ |= ϕ ) определяется индуктивно по структуре формулы ϕ :
• σ |= p , если атомарный предикат p истинен в начальном состоянии вычисления σ ;
• σ |= ¬ϕ ≡ σ |≠ ϕ — если формула ϕ не выполняется на σ ;
• σ |= ϕ1 ∨ ϕ2 ≡ σ |= ϕ1 ∨ σ |= ϕ2 — если на σ выполняется или формула ϕ1 , или формула ϕ2 ;
• σ1 |=Xϕ ≡ σ |=ϕ — если ϕ выполняется на вычислении σ1 = s1 s2 s3 …;
• σ1 |=ϕ1Uϕ2 ≡ (∃k ≥ σ) =(σk |=ϕ2 ∧ (∀j:0 ≤ j < k) σj |=ϕ1) — если когда-то в будущем состоянии вычисления σ (включая настоящее) выполнится формула ϕ2 , а до ее выполнения во всех состояниях вычисления σ будет выполняться ϕ1 .


Догори
 Профіль  
 
 Тема повідомлення: Re: Model checking - метод верифікації ПЗ
ПовідомленняДодано: 12 жовтня 2014, 11:36 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
Структура Крипке
Структура Крипке имеет конечное множество состояний и (непомеченных) переходов между ними, причем каждое состояние помечено множеством истинных в этом состоянии атомарных предикатов.
Структура Крипке M — это пятерка M = (S, S0,R, AP, L) , где:
• S — конечное непустое множество состояний;
• S0 ⊆S — непустое множество начальных состояний;
• R⊆S ×S — тотальное отношение на S , т. е. множество переходов, удовлетворяющее требованию: (∀s∈S )(∃s '∈S )( s, s ')∈R (из любого состояния есть переход);
• AP — конечное множество атомарных предикатов;
• L:S → 2 в степени AP — функция пометок (каждому состоянию отображение L сопоставляет множество истинных в нем атомарных предикатов).
Вычислением структуры Крипке M называется любая бесконечная цепочка σ = q0 q1 q2 q3... , такая, что q0∈S0 и (qi, qi+1) ∈ R.
Формально вычисление структуры Крипке M можно представить как отображение σ :N →S , где N — множество натуральных чисел, т. е. σ(i ) — это некоторое состояние структуры Крипке.
Траекторией структуры Крипке M , индуцированной вычислением σ = q0 q1 q2 q3 ... называется бесконечная цепочка L(σ) = L(q0) L(q1) L(q2) L(q3) ... , т. е. бесконечная цепочка подмножеств атомарных предикатов, истинных в соответствующих состояниях вычисления σ .
Формально, траектория — это отображение натурального ряда в множество 2 в степени AP.
Траектории структуры Крипке иногда называют трассами. Траектории являются последовательностями подмножеств атомарных предикатов — наблюдаемых свойств (событий, соотношений между переменными и т. п.), которые могут выполниться (произойти) в анализируемых системах. Именно эти последовательности являются важными для анализа. Формулы темпоральной логики описывают свойства траекторий.
В структуре Крипке в каждом состоянии указаны атомарные предикаты из конечного множества AP атомарных предикатов, которые истинны (выполняются) в этом состоянии. Каждое такое подмножество атомарных предикатов можно считать символом, помечающим состояние структуры Крипке.
Слова - в теории формальных языков конечные цепочки, построенные над конечным словарем.
ω-слова - бесконечные цепочки называются.
Поэтому траектории структуры Крипке называются также ее ω-словами.
Множество всех ω-слов структуры Крипке M называется ω-языком, допускаемым M .
Зображення
Рис. 2.12, а задает структуру Крипке с четырьмя состояниями {s0, s1, s2, s3} , одним начальным состоянием s0 , множеством атомарных предикатов { p, q, r} и функцией пометок L : L(s0) = {p,q} , L( s1) ={q, r} , L( s2) ={r} , L(s3) = { } .
Одно из вычислений структуры Крипке рис. 2.12, а — s0 s3 s1 s2 s2 s3... .
Траекторией структуры Крипке рис. 2.12, а при вычислении s0 s3 s1s2 s2 s3... является следующая цепочка: {p,q} {} {q,r} {r} {r}... .
Вычисления, показанные на рис. 2.12, в индуцируют следующие траектории (ω-слова) — бесконечные цепочки подмножеств множества атомарных предикатов, которые выполняются в последовательно проходимых состояниях:
п1 = {p,q} {q,r} {r} {} ... ;
п2 = {p,q} {q,r} {r} {r}... ;
п3 = {p,q} {} {q,r} {r} {} ... ;
п4 = {p,q} {} {q,r} {r} {r} ... .

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

Model Checking и структура Крипке
Стандартными шагами доказательства того, что поведение реагирующей системы обладает некоторым свойством, являются следующие:
1. Для верифицируемой системы строится адекватная модель Крипке M, т. е. система переходов с конечным числом состояний. Поведения реальной системы представляются разверткой (деревом вычислений) построенной структуры Крипке.
2. С помощью переменных и параметров верифицируемой системы выражаются интересующие разработчика атомарные предикаты структуры Крипке — логические выражения, которые могут принимать значения "истина" или "ложь" в каждом состоянии системы.
3. Проверяемое свойство выражается формулой ϕ темпоральной логики с использованием атомарных утверждений, темпоральных операторов и кванторов пути.
4. Проверяется истинность утверждения M |= ϕ (т. е. утверждения, что структура Крипке является моделью формулы ϕ ) с помощью полностью автоматизированной процедуры.
Метод верификации, реализующий эти шаги, и называется model checking.


Догори
 Профіль  
 
 Тема повідомлення: Re: Model checking - метод верифікації ПЗ
ПовідомленняДодано: 12 жовтня 2014, 13:40 
Офлайн
Викладач

З нами з: 29 листопада 2013, 17:11
Повідомлення: 4993
Расширенная темпоральная логика ветвящегося времени CTL*
В расширенной темпоральной логикой ветвящегося времени CTL* (Extended Computational Tree Logic) - в дополнение к
темпоральным операторам U(Until) и X(NextTime), введен квантор пути E. В CTL* могут присутствовать как формулы пути (характеризующие некоторое вычисление), так и формулы состояния, характеризующие состояние.
В дополнение к определению формул логики LTL, в логике CTL* добавляется только один квантор E — "существует такой путь, что... " ("возможное выполнение").
Для удобства вводится также квантор пути A (от All) как сокращенное обозначение:Aϕ=¬E¬ϕ. Формула Aϕ понимается так: "на всех путях из данного состояния формула пути ϕ истинна" ("неизбежное выполнение").
Формулы Eϕ и Aϕ являются формулами состояния, они характеризуют состояние структуры Крипке.
В практике верификации распространение получили два подмножества логики CTL*:
  • Логика линейного времени LTL. любую формулу пути ϕ логики LTL можно представить в логике CTL* формулой состояния Aϕ (на всех путях из начального состояния формула ϕ выполняется) явным добавлением перед ϕ квантора пути A . Именно в этом смысле логика LTL может рассматриваться как подмножество CTL*, хотя природа времени в этих логиках различна: в логике LTL — линейное время, в логике CTL* — ветвящееся время. Логика LTL и в своей нотации, и в концепциях очень проста, что делает ее весьма популярной в применениях.
  • Логика CTL (Computational Tree Logic) — логика ветвящегося времени. В этой логике допустимы только формулы, в которых каждый темпоральный оператор X , U , F и G (характеризующий некоторое вычисление) предваряется квантором пути — A или E , что превращает любую темпоральную формулу пути в формулу, характеризующую состояние. Формулы этой логики, как и формулы расширенной логики CTL*, интерпретируются на деревьях вычислений структуры Крипке, в каждом узле которых существует не одно-единственное будущее, а несколько альтернатив будущего. Следовательно, время в этих логиках представляется ветвящейся структурой в каждом текущем состоянии.

Зображення


Догори
 Профіль  
 
Відображати повідомлення за:  Сортувати за  
Створити нову тему Відповісти  [ 11 повідомлень ]  На сторінку 1, 2  Далі

Часовий пояс UTC + 2 годин [ DST ]



Хто зараз онлайн

Зараз переглядають цей форум: Немає зареєстрованих користувачів і 1 гість


Ви не можете створювати нові теми у цьому форумі
Ви не можете відповідати на теми у цьому форумі
Ви не можете редагувати ваші повідомлення у цьому форумі
Ви не можете видаляти ваші повідомлення у цьому форумі
Ви не можете додавати файли у цьому форумі

Знайти:
Вперед:  
cron
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group
Вы можете бесплатно создать форум PHPBB2 на MyBB2.ru, Также возможно создать форум бесплатно PHPBB3 на Getbb.ru
Український переклад © 2005-2007 Українська підтримка phpBB