Презентация 17 (Лекции), страница 5

. . , , . . .} , {. . . , , . . .} , →, ρ):{p, q}∅{q}{p}{p, q}{p, q}{p}Размеченные системы переходовТрасса LTS M = (S, S0 , →, ρ) — это любая последовательностьсостояний вычисления видаtr = s1 → s2 → s3 → . . .Размеченные системы переходовТрасса LTS M = (S, S0 , →, ρ) — это любая последовательностьсостояний вычисления видаtr = s1 → s2 → s3 → . . .Начальная трасса: s1 ∈ S0Размеченные системы переходовТрасса LTS M = (S, S0 , →, ρ) — это любая последовательностьсостояний вычисления видаtr = s1 → s2 → s3 → . . .Начальная трасса: s1 ∈ S0Tr (M) — множество всех трасс LTS MРазмеченные системы переходовТрасса LTS M = (S, S0 , →, ρ) — это любая последовательностьсостояний вычисления видаtr = s1 → s2 → s3 → .

. .Начальная трасса: s1 ∈ S0Tr (M) — множество всех трасс LTS MTr0 (M) — множество всех начальных трасс LTS MРазмеченные системы переходовТрасса LTS M = (S, S0 , →, ρ) — это любая последовательностьсостояний вычисления видаtr = s1 → s2 → s3 → . . .Начальная трасса: s1 ∈ S0Tr (M) — множество всех трасс LTS MTr0 (M) — множество всех начальных трасс LTS MI (tr ) — темпоральная интерпретация (N, ≤, ξ), такая что длялюбого момента времени n верно:ξ(n) = ρ(sn )Размеченные системы переходовПример{p, q}s1∅s2{q}s3s4s5s6s7{p}{p, q}{p, q}{p}Размеченные системы переходовПример{p, q}s1∅s2{q}s3s4s5s6s7{p}{p, q}{p, q}{p}s1Размеченные системы переходовПример{p, q}s1∅s2{q}s3s4s5s6s7{p}{p, q}{p, q}{p}s1s5Размеченные системы переходовПример{p, q}s1∅s2{q}s3s4s5s6s7{p}{p, q}{p, q}{p}s1s5s2Размеченные системы переходовПример{p, q}s1∅s2{q}s3s4s5s6s7{p}{p, q}{p, q}{p}s1s5s2s3Размеченные системы переходовПример{p, q}s1∅s2{q}s3s4s5s6s7{p}{p, q}{p, q}{p}s1s5s2s3s3Размеченные системы переходовПримерТрасса tr :{p, q}s1∅s2{q}s3s4s5s6s7{p}{p, q}{p, q}{p}s1s5s2s3s3...Размеченные системы переходовПример{p, q}s1∅s2{q}s3s4s5s6s7{p}{p, q}{p, q}{p}Начальная трасса tr :s1s5s2s3s3...Размеченные системы переходовПример{p, q}s1∅s2{q}s3s4s5s6s7{p}{p, q}{p, q}{p}{p, q}{p, q} ∅s1s5s2{q} {q}s3s3 .

. .Размеченные системы переходовПример{p, q}s1∅s2{q}s3s4s5s6s7{p}{p, q}{p, q}{p}Интерпретация I (tr ):{p, q}{p, q} ∅123{q} {q}45 ...Размеченные системы переходовКак построить LTS, описывающую распределённую систему?Размеченные системы переходовКак построить LTS, описывающую распределённую систему?Начнём с простого: покажем, как можно построить LTS дляпоследовательной программы πРазмеченные системы переходовКак построить LTS, описывающую распределённую систему?Начнём с простого: покажем, как можно построить LTS дляпоследовательной программы πIсостояния LTS — это состояния вычисления программы πРазмеченные системы переходовКак построить LTS, описывающую распределённую систему?Начнём с простого: покажем, как можно построить LTS дляпоследовательной программы πIсостояния LTS — это состояния вычисления программы πI(состояние вычисления включает в себя состояниеуправления и состояние данных)Размеченные системы переходовКак построить LTS, описывающую распределённую систему?Начнём с простого: покажем, как можно построить LTS дляпоследовательной программы πIсостояния LTS — это состояния вычисления программы πII(состояние вычисления включает в себя состояниеуправления и состояние данных)начальные состояния LTS — это всевозможные состояния, скоторых может начинаться вычисление πРазмеченные системы переходовКак построить LTS, описывающую распределённую систему?Начнём с простого: покажем, как можно построить LTS дляпоследовательной программы πIсостояния LTS — это состояния вычисления программы πI(состояние вычисления включает в себя состояниеуправления и состояние данных)Iначальные состояния LTS — это всевозможные состояния, скоторых может начинаться вычисление πIпереход в LTS соответствует шагу вычисления программы πРазмеченные системы переходовКак построить LTS, описывающую распределённую систему?Начнём с простого: покажем, как можно построить LTS дляпоследовательной программы πIсостояния LTS — это состояния вычисления программы πI(состояние вычисления включает в себя состояниеуправления и состояние данных)Iначальные состояния LTS — это всевозможные состояния, скоторых может начинаться вычисление πIпереход в LTS соответствует шагу вычисления программы πI(например, hπ, θi →I hπ 0 , θ0 i)Размеченные системы переходовКак построить LTS, описывающую распределённую систему?Начнём с простого: покажем, как можно построить LTS дляпоследовательной программы πIсостояния LTS — это состояния вычисления программы πI(состояние вычисления включает в себя состояниеуправления и состояние данных)Iначальные состояния LTS — это всевозможные состояния, скоторых может начинаться вычисление πIпереход в LTS соответствует шагу вычисления программы πII(например, hπ, θi →I hπ 0 , θ0 i)атомарное событие соответствует отношению над значениямипеременных и состояния управления программыРазмеченные системы переходовКак построить LTS, описывающую распределённую систему?Начнём с простого: покажем, как можно построить LTS дляпоследовательной программы πIсостояния LTS — это состояния вычисления программы πI(состояние вычисления включает в себя состояниеуправления и состояние данных)Iначальные состояния LTS — это всевозможные состояния, скоторых может начинаться вычисление πIпереход в LTS соответствует шагу вычисления программы πI(например, hπ, θi →I hπ 0 , θ0 i)Iатомарное событие соответствует отношению над значениямипеременных и состояния управления программыIсобытие включается в метку состояния LTS ⇔ состояниевычисления удовлетворяет соответствующему отношениюРазмеченные системы переходовПримерВернёмся ещё раз к примеру с сетевым принтеромРазмеченные системы переходовПримерВернёмся ещё раз к примеру с сетевым принтеромПредположим, что в контроллере принтера есть однобитовыйрегистр R, доступный на чтение и запись всем компьютерам всетиРазмеченные системы переходовПримерВернёмся ещё раз к примеру с сетевым принтеромПредположим, что в контроллере принтера есть однобитовыйрегистр R, доступный на чтение и запись всем компьютерам всети:R = true⇔принтер свободенРазмеченные системы переходовПримерВернёмся ещё раз к примеру с сетевым принтеромПредположим, что в контроллере принтера есть однобитовыйрегистр R, доступный на чтение и запись всем компьютерам всети:R = true⇔принтер свободенТогда программа π взаимодействия компьютера с принтеромможет выглядеть так:while (true) {L1 : while (!R);L2 : R = false;L3 : SEND_DATAL4 : R = true;}Размеченные системы переходовПримерLTS для программы π будет выглядеть так:(функция разметки опущена)hL1 , {R/true}ihL2 , {R/true}ihL3 , {R/false}ihL4 , {R/false}ihL1 , {R/false}iРазмеченные системы переходовLTS и окружение программыПрограмма в распределённой системе может взаимодействоватьс другими программами: общие переменные, обменсообщениями, сигналы, .

. .Размеченные системы переходовLTS и окружение программыПрограмма в распределённой системе может взаимодействоватьс другими программами: общие переменные, обменсообщениями, сигналы, . . .Такое взаимодействие выражается в том, что состояниевычисления программы может измениться (под воздействием еёокружения)Размеченные системы переходовLTS и окружение программыПрограмма в распределённой системе может взаимодействоватьс другими программами: общие переменные, обменсообщениями, сигналы, . .

.Такое взаимодействие выражается в том, что состояниевычисления программы может измениться (под воздействием еёокружения)Например, регистр R в последнем примере может быть изменёнлюбым компьютером сетиРазмеченные системы переходовLTS и окружение программыПрограмма в распределённой системе может взаимодействоватьс другими программами: общие переменные, обменсообщениями, сигналы, . . .Такое взаимодействие выражается в том, что состояниевычисления программы может измениться (под воздействием еёокружения)Например, регистр R в последнем примере может быть изменёнлюбым компьютером сетиЧтобы учесть такое изменение, следует добавить в LTSпереходы, отвечающие всем возможностям окружения повлиятьна состояние вычисления программыРазмеченные системы переходовПример: LTS для программы π с окружением, способнымпроизвольно переключать значение регистра RhL1 , {R/true}ihL1 , {R/false}ihL2 , {R/true}ihL2 , {R/false}ihL3 , {R/false}ihL3 , {R/true}ihL4 , {R/false}ihL4 , {R/true}iРазмеченные системы переходовLTS и взаимодействие программПредположим, что для программ π1 , π2 построены LTSs и чтоэти программы взаимодействуют между собойРазмеченные системы переходовLTS и взаимодействие программПредположим, что для программ π1 , π2 построены LTSs и чтоэти программы взаимодействуют между собойКак построить LTS, описывающую взаимодействие π1 , π2 ?Размеченные системы переходовLTS и взаимодействие программПредположим, что для программ π1 , π2 построены LTSs и чтоэти программы взаимодействуют между собойКак построить LTS, описывающую взаимодействие π1 , π2 ?Один из наиболее популярных способов описаниявзаимодействия программ — этосемантика чередующихся вычислений:(interleaving semantics)Размеченные системы переходовLTS и взаимодействие программПредположим, что для программ π1 , π2 построены LTSs и чтоэти программы взаимодействуют между собойКак построить LTS, описывающую взаимодействие π1 , π2 ?Один из наиболее популярных способов описаниявзаимодействия программ — этосемантика чередующихся вычислений:(interleaving semantics)Iсовокупное состояние вычисления — это состояния π1 , π2 , вкоторых общие переменные изменяются синхронно (иучтены другие взаимосвязи состояний, если они есть)Размеченные системы переходовLTS и взаимодействие программПредположим, что для программ π1 , π2 построены LTSs и чтоэти программы взаимодействуют между собойКак построить LTS, описывающую взаимодействие π1 , π2 ?Один из наиболее популярных способов описаниявзаимодействия программ — этосемантика чередующихся вычислений:(interleaving semantics)IIсовокупное состояние вычисления — это состояния π1 , π2 , вкоторых общие переменные изменяются синхронно (иучтены другие взаимосвязи состояний, если они есть)переход в LTS, описывающей взаимодействие программ,состоит в (произвольном) выборе одной из программ π1 , π2и выполнении следующего оператора этой программыРазмеченные системы переходовПримерРассмотрим LTSs, описывающие две (одинаковые) программывзаимодействия с сетевым принтером:π0π 00hL01 , trueihL01 , falseihL1 , trueihL02 , trueihL2 , trueihL03 , falseihL3 , falseihL04 , falseihL4 , falseihL1 , falseiРазмеченные системы переходовПримерРассмотрим LTSs, описывающие две (одинаковые) программывзаимодействия с сетевым принтером:π0π 00hL01 , trueihL01 , falseihL1 , trueihL02 , trueihL2 , trueihL03 , falseihL3 , falseihL04 , falseihL4 , falseihL1 , falseiСчитаем регистр R общей переменной программ π 0 , π 00Размеченные системы переходовПримерLTS, описывающая взаимодействие π 0 , π 00 согласно семантикечередующихся вычислений, выглядит так:hL01 , L001 , tihL04 , L001 , fihL03 , L001 , fihL02 , L001 , tihL01 , L002 , tihL01 , L003 , fihL02 , L002 , tihL02 , L003 , fihL02 , L004 , fihL03 , L002 , fihL03 , L003 , fihL04 , L002 , fihL03 , L004 , fihL04 , L003 , fihL03 , L001 , tihL04 , L001 , tihL04 , L004 , fihL01 , L004 , tihL01 , L003 , tihL03 , L002 , tihL04 , L002 , tihL01 , L001 , fihL02 , L004 , tihL02 , L003 , tihL01 , L004 , fiПостановка задачи model checkingПостановка задачи model checkingНа данный момент имеются:Iформальный язык описания темпоральных спецификаций:LTLПостановка задачи model checkingНа данный момент имеются:IIформальный язык описания темпоральных спецификаций:LTLформальная модель, описывающая поведениераспределённых систем: LTSПостановка задачи model checkingНа данный момент имеются:IIформальный язык описания темпоральных спецификаций:LTLформальная модель, описывающая поведениераспределённых систем: LTSКак проверить, удовлетворяет ли распределённая систематемпоральной спецификации?Постановка задачи model checkingНа данный момент имеются:IIформальный язык описания темпоральных спецификаций:LTLформальная модель, описывающая поведениераспределённых систем: LTSКак проверить, удовлетворяет ли распределённая систематемпоральной спецификации?Достаточно записать спецификацию в виде LTL-формулы ϕ иубедиться, что для каждой начальной трассы tr LTS M = M(Π),описывающей систему Π, верно:I (tr ) |= ϕПостановка задачи model checkingНа данный момент имеются:IIформальный язык описания темпоральных спецификаций:LTLформальная модель, описывающая поведениераспределённых систем: LTSКак проверить, удовлетворяет ли распределённая систематемпоральной спецификации?Достаточно записать спецификацию в виде LTL-формулы ϕ иубедиться, что для каждой начальной трассы tr LTS M = M(Π),описывающей систему Π, верно:I (tr ) |= ϕПоследний факт будем для краткости обозначать так: M |= ϕПостановка задачи model checkingЗадача model checking для выбранных формализмовформулируется так:для заданных LTL-формулы ϕ и LTS Mпроверить условие M |= ϕПостановка задачи model checkingЗадача model checking для выбранных формализмовформулируется так:для заданных LTL-формулы ϕ и LTS Mпроверить условие M |= ϕА как это сделать?Постановка задачи model checkingЗадача model checking для выбранных формализмовформулируется так:для заданных LTL-формулы ϕ и LTS Mпроверить условие M |= ϕА как это сделать?То есть:Есть ли алгоритм, проверяющий условие M |= ϕ,и если есть, то как он работает?Конец лекции 17.