Финальные модели спецификации . Финальные модели спецификации Игорь Бурдонов <*****@***ru>,. Александр Косачев <*****@***ru> (стр. 9 )

S-R→SR-determ→rts(S)-delete→prts(S)-final→ frts(S, safe by).

Для конечности prts(S) достаточно конечности исходной LTS S (конечность множества достижимых переходов) и семейства R. При этих условиях для конечности frts(S) достаточно конечности регулярности отношения safe by. Заметим, что мы не требует конечности алфавита L и конечности семейства Q.

Заключение

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

Финальная RTS как модель спецификации обладает целым рядом полезных для тестирования свойств, выгодно отличающих ее от LTS-модели, R - и p-моделей, а также от RTS для R - и p-моделей:

Детерминизм. RTS детерминирована, следовательно, каждая трасса, по которой нужно генерировать тесты, заканчивается в одном состоянии. Безопасные трассы. Безопасные трассы спецификации – это все ее простые трассы, заканчивающиеся в состояниях, отличных от ω и γ. Безопасные кнопки. Кнопка P безопасна по safe by в финальной RTS F после неразрушающей трассы σ тогда и только тогда, когда она безопасна по safe in в конечном состоянии трассы s: P safe by tr(F) after σ ⇔ P safe in s, где F after σ = {s}.

Также предложены алгоритмы преобразования LTS-модели с заданным отношением safe by в финальную RTS-модель. Если конечна исходная LTS S и семейство R, а отношение safe by регулярно, то финальная RTS конечна и строится за конечное время.

В то же время множество финальных трасс, хотя и достаточно, но, вообще говоря, не необходимо для генерации тестов. Это объясняется тем, что среди безопасных трасс спецификации могут встречаться неконформные трассы, то есть трассы, которых не может быть ни в одной конформной реализации. Понятно, что по таким трассам не нужно генерировать тесты. Такие трассы можно удалить из множества трасс, по которым генерируются тесты с помощью ∇-пополнения. Исследованию неконформных трасс спецификации и построению алгоритмов, удаляющих такие трассы из спецификации, посвящены наши работы [16],[17].

Доказательства утверждений

Доказательство Теорема 2:

Пусть бγс∈Ψ.

Тогда бγс∈ptr(Ψ). Имеем SafeγΔ(Ψ)=∅=SafeγΔ(ptr(Ψ)).

Утверждение доказано.

Пусть бγс∉Ψ.

Будем вести доказательство индукцией по трассе σ.

База индукции.

Из бγс∉Ψ следует т∈SafeγΔ(Ψ).

Из бγс∉Ψ следует бγс∉ptr(Ψ), что влечет т∈SafeγΔ(ptr(Ψ)).

Шаг индукции. Пусть σ∈SafeγΔ(Ψ)∩SafeγΔ(ptr(Ψ)) и P∈R∪Q. Докажем, что P safeγΔ Ψ after σ ⇒ P safeγΔ ptr(Ψ) after σ).

Допустим обратное. Тогда либо σ⋅бΔс∈ptr(Ψ), либо σ⋅бz,γс∈ptr(Ψ) для некоторого z∈P. Поскольку ptr(Ψ)⊆Ψ, имеем σ⋅бΔс∈Ψ, либо σ⋅бz,γс∈Ψ для некоторого z∈P. Но это противоречит условию P safeγΔ Ψ after σ. Следовательно, наше допущение не верно, и импликация доказана.

Докажем, что P safeγΔ Ψ after σ ⇐ P safeγΔ ptr(Ψ) after σ).

Допустим обратное. Тогда либо σ⋅бΔс∈Ψ, либо σ⋅бz,γс∈Ψ для некоторого z∈P. Поскольку σ∈SafeγΔ(Ψ), имеем либо бΔс∈fs(Ψ,σ), либо бz,γс∈fs(Ψ,σ) для некоторого z∈P. Но тогда либо σ⋅бΔс∈ptr(Ψ), либо σ⋅бz,γс∈ptr(Ψ) для некоторого z∈P. Но это противоречит условию P safeγΔ ptr(Ψ) after σ. Следовательно, наше допущение не верно, и обратная импликация доказана.

Для u∈L∪R докажем σ⋅бuс∈SafeγΔ(Ψ) ⇒ σ⋅бuс∈SafeγΔ(ptr(Ψ)).

Поскольку σ⋅бuс∈SafeγΔ(Ψ), найдется такое P∈but(u), что P safeγΔ Ψ after σ. По доказанному в п.2.2.1 P safeγΔ ptr(Ψ) after σ). Поскольку σ⋅бuс∈SafeγΔ(Ψ), имеем σ⋅бuс∈ptr(Ψ). Следовательно, σ⋅бuс∈SafeγΔ(ptr(Ψ)).

Для u∈L∪R докажем σ⋅бuс∈SafeγΔ(Ψ) ⇐ σ⋅бuс∈SafeγΔ(ptr(Ψ)).

Поскольку σ⋅бuс∈SafeγΔ(ptr(Ψ)), найдется такое P∈but(u), что P safeγΔ ptr(Ψ) after σ. По доказанному в п.2.2.2 P safeγΔ Ψ after σ). Поскольку σ⋅бuс∈SafeγΔ(ptr(Ψ)), имеем σ⋅бuс∈ptr(Ψ). Поскольку ptr(Ψ)⊆Ψ, имеем σ⋅бuс∈Ψ. Следовательно, σ⋅бuс∈SafeγΔ(Ψ).

Доказательство Теорема 3:

Прямая импликация. Пусть ptr(Ψ)=Ψ.

Докажем, что SafeγΔ(Ψ) = {σ∈Ψ∩(L∪R)*|σ⋅бγс∉Ψ}.

Если бγс∈Ψ, то ptr(Ψ)={т, бγс}. Тогда Ψ={т, бγс} и утверждение очевидно. Пусть бγс∉Ψ. По определению σ∈SafeγΔ(Ψ) влечет σ∈Ψ∩(L∪R)*.

Поскольку бγс∉fs(Ψ,σ), а ptr(Ψ)=Ψ, имеем σ⋅бγс∉Ψ.

Следовательно, SafeγΔ(Ψ) ⊆ {σ∈Ψ∩(L∪R)*|σ⋅бγс∉Ψ}.

Покажем обратную вложенность. Допустим противное: существует трасса σ∈Ψ∩(L∪R)* такая, что σ⋅бγс∉Ψ, но σ∉SafeγΔ(Ψ).

Поскольку бγс∉Ψ, имеем т∈SafeγΔ(Ψ). Следовательно, у трассы σ есть префикс μ⋅бuс такой, что μ∈SafeγΔ(Ψ), но μ⋅бuс∉SafeγΔ(Ψ).

Следовательно, либо u=Δ, либо u=γ, либо u∈L∪R и u safeγΔ Ψ after μ. Случаев u=Δ и u=γ быть не может, так как μ⋅бuс≤σ∈(L∪R)*.

Следовательно, u∈L∪R и u safeγΔ Ψ after μ.

Если μ⋅бu,γс∉Ψ, то бuс∉fs(Ψ,μ), поэтому μ⋅бuс∉ptr(Ψ)=Ψ, что противоречит префикс-замкнутости Ψ, поскольку μ⋅бuс≤σ∈Ψ.

Если μ⋅бu,γс∈Ψ, то возможны два варианта: 1) μ⋅бuс=σ и 2) μ⋅бuс<σ. Случай 1 противоречит σ⋅бγс∉Ψ. В случае 2 найдется такое v∈L∪R, что μ⋅бu, vс≤σ. Но бu, vс∉fs(Ψ,μ), поэтому μ⋅бu, vс∉ptr(Ψ)=Ψ, что противоречит префикс-замкнутости Ψ, поскольку μ⋅бu, vс≤σ∈Ψ.

Мы пришли к противоречию, следовательно, наше допущение не верно и обратная вложенность доказана.

Обратная импликация. Пусть выполнены условия обратной импликации.

Докажем, что ptr(Ψ)=Ψ.

Пусть бγс∈Ψ.

Тогда Ψ={т, бγс} и ptr(Ψ)={т, бγс}.

Пусть бγс∉Ψ.

Тогда SafeγΔ(Ψ)={σ∈Ψ∩(L∪R)*|σ⋅бγс∉Ψ}, трассы из Ψ допустимы и после отказа в них нет разрушения.

Поскольку по определению ptr(Ψ)⊆Ψ, нам нужно доказать обратную вложенность. Допустим, это не так: существует трасса σ∈Ψ такая, что σ∉ptr(Ψ). Поскольку по определению предфинальности SafeγΔ(Ψ)⊆ptr(Ψ), имеем σ∉SafeγΔ(Ψ). Поскольку бγс∉Ψ, имеем т∈SafeγΔ(Ψ). Следовательно, трассу σ можно представить в виде σ=μ⋅λ таком, что μ∈SafeγΔ(Ψ) максимальный безопасный префикс σ, но λ∉fs(Ψ,μ).

Поскольку все трассы из Ψ допустимы, возможны только следующие случаи: 1) λ=λ1⋅бΔс, либо 2) λ=λ1⋅бγс, либо 3) λ=λ1, где λ1∈(L∪R)*.

Поскольку SafeγΔ(Ψ)={σ∈Ψ∩(L∪R)*|σ⋅бγс∉Ψ}, в этих случаях имеет место: 1) λ1=т и λ=бΔс, 2) λ1=т и λ=бγс, 3) λ=бuс, где u∈L∪R и μ⋅бu,γс∈Ψ.

Случай 1 противоречит λ=бΔс∉fs(Ψ,μ).

В случае 2 трасса μ не может быть пустой, так как бγс∉Ψ, и не может заканчиваться отказом, так как в трассах из Ψ после отказа нет разрушения. Следовательно, трасса μ заканчивается действием, за которым в Ψ следует разрушение, что противоречит μ∈SafeγΔ(Ψ).

Рассмотрим случай 3. Поскольку в трассах из Ψ после отказа нет разрушения, должно быть u∈L. Но тогда λ=бuс∈fs(Ψ,μ), что неверно.

Мы пришли к противоречию, следовательно, наше допущение не верно и обратная вложенность доказана.

Необходимость условий теоремы для обратной импликации показывается следующими примерами. В каждом из этих примеров нарушено только одно условие обратной импликации. Выполнены все условия, кроме условия на множество неразрушающих трасс при бγс∈Ψ.

Пример Ψ={т, бPс, бzс, бz,γс}, где P∈R и z∈P.

SafeγΔ(Ψ)={т} ≠ {т, бPс}={σ∈Ψ∩(L∪R)*|σ⋅бγс∉Ψ},

ptr(Ψ)={т, бzс, бz,γс} ≠ Ψ.

Выполнены все условия, кроме условия Ψ={т, бγс} при бγс∈Ψ.

Пример Ψ={т, бγс, бuс}, где u∈L∪R∪{Δ,γ}. ptr(Ψ)={т, бγс} ≠ Ψ.

Выполнены все условия, кроме допустимости трасс.

Пример 1 Ψ={т, бΔс, бΔ,uс}, где u∈L∪R∪{Δ,γ}.