Liniowa właściwość czasu

W sprawdzaniu modeli , gałęzi informatyki , liniowe właściwości czasowe są wykorzystywane do opisu wymagań stawianych modelowi systemu komputerowego . Przykładowe właściwości obejmują „automat sprzedający nie wydaje napoju, dopóki nie zostaną wprowadzone pieniądze” (właściwość bezpieczeństwa ) lub „program komputerowy ostatecznie się kończy” ( właściwość żywotności ). Właściwości uczciwości można wykorzystać do wykluczenia nierealistycznych ścieżek modelu. Na przykład w modelu dwóch sygnalizacji świetlnych właściwość żywotności „oba sygnalizacja świetlna jest nieskończenie często zielona” może być prawdziwa tylko przy bezwarunkowym ograniczeniu uczciwości „każda sygnalizacja świetlna zmienia kolor nieskończenie często” (aby wykluczyć przypadek, w którym jedna sygnalizacja świetlna jest „nieskończenie szybszy” niż drugi).

Formalnie liniowa właściwość czasu jest językiem ω nad zbiorem potęg „twierdzeń atomowych”. Oznacza to, że właściwość zawiera sekwencje zestawów propozycji, z których każda jest znana jako „słowo”. Każdą właściwość można przepisać jako „ P i Q występują oba” dla pewnej właściwości bezpieczeństwa P i właściwości żywotności Q . Niezmiennikiem dla systemu jest coś, co jest prawdziwe lub fałszywe dla określonego stanu. Właściwości niezmienne opisują niezmiennik, który musi spełniać każdy osiągalny stan modelu, podczas gdy właściwości trwałości mają postać „ostatecznie na zawsze zachowa się jakiś niezmiennik”.

Logiki czasowe , takie jak liniowa logika czasowa, opisują typy liniowych właściwości czasu za pomocą wzorów.

Ten artykuł dotyczy zdaniowych właściwości czasu liniowego i nie może obsłużyć predykatów dotyczących stanów programu, więc nie może zdefiniować właściwości takiej jak: bieżąca wartość y określa, ile razy x przełącza się między 0 a 1 przed zakończeniem. Bardziej ogólny formalizm zastosowany we właściwościach związanych z bezpieczeństwem i żywotnością może sobie z tym poradzić.

Definicja

Niech AP będzie zbiorem zdań atomowych. Słowo nad $}}$ AP ( zbiór mocy AP ) jest nieskończoną sekwencją zbiorów zdań, takich jak ${\ Displaystyle w: = \ {a \} \ {a, b \} \ pusty zbiór \ {a, b \} ^ {\ omega}} ($ dla zdań atomowych ${\ Displaystyle AP = \ {a, b \}}$ ). Właściwość czasu liniowego (LT) względem AP jest podzbiorem, tj. Zbiorem słów ${\ Displaystyle (2 ^ {AP}) ^ {\ omega}} .$ Przykładem właściwości LT nad zbiorem $.$ zawierających często ” Słowo w jest w tym zbiorze, ponieważ a jest zawarte w ${\ Displaystyle \ {a, b \}}$ , co występuje nieskończenie często. Słowo, którego nie ma w tym zestawie, to $\ Displaystyle x: = \ {a \} (\ {b \} \ pusty zbiór) ^ {\ omega}}$ { jako jedyne występuje raz (w pierwszym zestawie).

Właściwość LT jest $)$ ω ( odwrotnie

Oznaczamy przez pref ( w ) skończone przedrostki w (tj. ${\ Displaystyle \ {\ {a \},\{a\}\{a,b\},\{a\}\{a,b\}\emptyset ,...\}}$ w powyższym przypadku). Zamknięcie własności LT P to:

$\ Displaystyle zamknięcie (P): = \ {\ sigma \in (2^{AP})^{\omega }\mid pref(\sigma )\subseteq pref(P)\}}$

Aplikacje

Struktura Kripkego nad ${\ Displaystyle \ {p, q \}}$ . Nie spełnia właściwości LT „nieskończenie często q ”, ze względu na ścieżkę ${\ Displaystyle s_ {1} s_ {2} s_ {3} ^ {\ omega}}$ . Spełnia właściwość „nieskończenie często p ”, ponieważ wszystkie możliwe ścieżki wchodzą lub ${\ displaystyle s_ {1}}$ lub ${\ displaystyle s_ {3}}$ nieskończenie często.

Korzystając z teorii maszyn skończonych , program lub system komputerowy można modelować za pomocą struktury Kripkego . Właściwości LT opisują następnie ograniczenia dotyczące śladów (wyjść) struktury Kripkego. Na przykład, jeśli dwie sygnalizacje świetlne na skrzyżowaniu są reprezentowane przez strukturę Kripkego, to twierdzenia atomowe mogą być możliwymi kolorami każdego światła i może być pożądane, aby ślady spełniały właściwość LT „sygnalizacja świetlna nie może być jednocześnie zielona na w tym samym czasie” (aby uniknąć kolizji samochodowych).

Jeśli każdy ślad struktury Kripkego TS jest śladem TS ' , to każda właściwość LT, którą spełnia TS ' , jest spełniona przez TS . Jest to przydatne w sprawdzaniu modelu, aby umożliwić abstrakcję: jeśli uproszczony model systemu spełnia właściwość LT, to rzeczywisty model systemu również go spełni.

Klasyfikacja liniowych właściwości czasowych

Właściwości bezpieczeństwa

Właściwość bezpieczeństwa ma nieformalną postać „nie dzieje się nic złego”. Na przykład, jeśli system modeluje bankomat (bankomat), wówczas taką właściwością jest „nie należy wydawać pieniędzy, dopóki nie zostanie wprowadzony kod PIN”. Formalnie właściwość bezpieczeństwa jest właściwością LT taką, że każde słowo naruszające tę właściwość ma „zły przedrostek”, dla którego żadne słowo z tym przedrostkiem nie spełnia tej właściwości. To jest,

${\ Displaystyle \ forall \ sigma \ in (2 ^ {AP} )^{\omega}\setminus P\ \exists {\text{ przedrostek skończony}}\ {\hat {\sigma }}:P\cap \{\sigma '\mid {\hat {\sigma }}\ {\text{jest przedrostkiem}}\\sigma '\}=\pustyzbiór}$

W przykładzie z bankomatem minimalny zły prefiks to skończony zestaw wykonywanych kroków, w którym pieniądze są wydawane w ostatnim kroku, a kod PIN nie jest wprowadzany na żadnym etapie. Aby zweryfikować właściwość bezpieczeństwa, wystarczy wziąć pod uwagę tylko skończone ślady struktury Kripkego i sprawdzić, czy któryś z takich śladów nie jest złym przedrostkiem.

Właściwość LT P jest właściwością bezpieczeństwa wtedy i tylko wtedy, gdy ${\ displaystyle close (P) = P}$ .

Właściwości niezmienne

Właściwość niezmienna to rodzaj właściwości bezpieczeństwa, w której warunek odnosi się tylko do bieżącego stanu. Na przykład przykład bankomatu nie jest niezmiennikiem, ponieważ nie możemy stwierdzić, czy właściwość została naruszona, widząc, że bieżący stan to „wydaj pieniądze”, tylko widząc, że bieżący stan to „wydaj pieniądze”, a żaden poprzedni stan nie został „odczytany” SZPILKA". Przykładem niezmiennika jest warunek dotyczący sygnalizacji świetlnej „oba sygnalizatory świetlne nie mogą być jednocześnie zielone” powyżej. Innym jest „zmienna x nigdy nie jest ujemna” w modelu programu komputerowego.

Formalnie niezmiennik ma postać:

${\ Displaystyle P = \ {A_ {0} A_ {1} .... \ w (2 ^ {AP}) ^ {\ omega }\mid \forall j\in \mathbb {N} :A_{j}\ {\text{satisfies}}\ \Phi \}}$

dla jakiejś formuły logiki zdań . ${\ displaystyle \ Phi}$ .

Struktura Kripkego spełnia niezmiennik wtedy i tylko wtedy, gdy każdy osiągalny stan spełnia niezmiennik, co można sprawdzić za pomocą przeszukiwania wszerz lub w głąb . Właściwości bezpieczeństwa można zweryfikować indukcyjnie za pomocą niezmienników.

Właściwości żywotności

Właściwość żywotności ma nieformalnie postać „w końcu dzieje się coś dobrego”. Formalnie P jest właściwością żywotności, jeśli ${\ Displaystyle pref (P) = (2 ^ {AP}) ^ {*}},$ tj. dowolny skończony ciąg może być kontynuowany ważny ślad. Przykładem właściwości liveness jest poprzednia właściwość LT „zbiór słów zawierających a nieskończenie często”. Żaden skończony przedrostek słowa nie może dowieść, że słowo to nie spełnia tej właściwości, ponieważ słowo może mieć nieskończenie wiele a s.

Jeśli chodzi o programy komputerowe, przydatne właściwości żywotności obejmują „program ostatecznie się kończy”, aw przypadku obliczeń współbieżnych „każdy proces musi ostatecznie zostać obsłużony”.

Właściwości trwałości

Właściwość trwałości jest właściwością żywotności postaci „w końcu na $”$ . Oznacza to, że właściwość postaci:

${\ Displaystyle P = \ {A_ {0} A_ {1} ... \ w (2 ^ {AP}) ^{\omega }\mid \exists N\in \mathbb {N} :\forall n\geq N:A_{n}\ {\text{satisfies}}\ \Phi \}}$

Związek między właściwościami bezpieczeństwa i żywotności

$}$ niż $Displaystyle (2 ^ {AP}) ^ {\ omega$ zbiór wszystkich słów powyżej ) nie jest jednocześnie ( ZA bezpieczeństwo i właściwość życia. Chociaż nie każda właściwość jest właściwością bezpieczeństwa lub właściwością żywotności (rozważ „ a występuje dokładnie raz”), każda właściwość jest przecięciem właściwości bezpieczeństwa i właściwości żywotności.

W topologii zbiór wszystkich słów można wyposażyć w metrykę : ${\ Displaystyle (2 ^ {AP}) ^ {\ omega}}$

${\ Displaystyle d (w, x): = \ inf \ {2 ^ {- | s |} \ mid s \ w pref (w )\cap pref(x)\}}$

Wtedy właściwość bezpieczeństwa jest zbiorem zamkniętym , a właściwość żywotności jest zbiorem gęstym .

Właściwości uczciwości

Właściwości uczciwości to warunki wstępne nałożone na system w celu wykluczenia nierealistycznych śladów. Bezwarunkowa sprawiedliwość ma postać „każdy proces ma swoją kolej nieskończenie często”. Silna sprawiedliwość ma postać „każdy proces ma swój obrót nieskończenie często, jeśli jest włączany nieskończenie często”. Słaba sprawiedliwość ma postać „każdy proces ma swój obrót nieskończenie często, jeśli jest stale włączany z określonego punktu”.

W niektórych systemach ograniczenie uczciwości jest definiowane przez zbiór stanów, a „uczciwa ścieżka” to taka, która nieskończenie często przechodzi przez pewien stan w ograniczeniu uczciwości. Jeśli istnieje wiele ograniczeń uczciwości, to uczciwa ścieżka musi przechodzić nieskończenie często przez jeden stan na ograniczenie. Program „dość spełnia” właściwość LT P w odniesieniu do zestawu warunków rzetelności, jeśli dla każdej ścieżki albo ścieżka nie spełnia warunku uczciwości, albo spełnia P . Oznacza to, że właściwość P jest spełniona dla wszystkich uczciwych ścieżek.

Właściwość uczciwości jest możliwa do zrealizowania dla struktury Kripkego, jeśli każdy osiągalny stan ma uczciwą ścieżkę rozpoczynającą się od tego stanu. Dopóki zestaw warunków uczciwości jest możliwy do zrealizowania, nie mają one znaczenia dla właściwości bezpieczeństwa.

Logika czasowa

Logiki czasowe , takie jak logika drzewa obliczeniowego (CTL), mogą być używane do określania niektórych właściwości LT. Wszystkie liniowej logiki czasowej (LTL) są właściwościami LT. Na podstawie argumentu zliczania widzimy, że dowolna logika, w której każda formuła jest skończonym ciągiem, nie może reprezentować wszystkich właściwości LT, ponieważ musi istnieć policzalnie wiele formuł, ale istnieje niezliczona liczba właściwości LT.

Notatki

•   Alpern, B.; Schneidera, FB (1987). „Rozpoznawanie bezpieczeństwa i żywotności” . Obliczenia rozproszone . 2 (3): 117. CiteSeerX 10.1.1.20.5470 . doi : 10.1007/BF01782772 .
•   Baier, Christel ; Katoen, Joost-Pieter (2008). Zasady sprawdzania modeli . MIT Press. ISBN 9780262026499 .
•   Clarke, Edmund M .; Grumberg, Orna ; Kroening, Daniel (2018). Sprawdzanie modeli . MIT Press. ISBN 9780262038836 .
• D'Silva, Vijay; Kroening, Daniel ; Weissenbacher, Georg (2008). „Przegląd zautomatyzowanych technik formalnej weryfikacji oprogramowania”. Transakcje IEEE dotyczące wspomaganego komputerowo projektowania układów scalonych i systemów . 27 (7): 1165–1178.
• Finkbeiner, Bernd; Torfah, Hazem (2017). „Gęstość właściwości w czasie liniowym”. Notatki z wykładów z informatyki . Zautomatyzowana technologia weryfikacji i analizy. Tom. 10482. Zygmunt.
•   Kern, Christoph; Greenstreet, Mark R. (1999). „Formalna weryfikacja w projektowaniu sprzętu: ankieta”. Transakcje ACM dotyczące automatyzacji projektowania systemów elektronicznych . Stowarzyszenie Maszyn Komputerowych. 4 (2). doi : 10.1145/307988.307989 . ISSN 1084-4309 .

Dalsza lektura

• Emerson, E. Allen (1990). „Logika czasowa i modalna”. Podręcznik informatyki teoretycznej . B. _
• Pnueli, Amir (1986). „Zastosowania logiki temporalnej do specyfikacji i weryfikacji systemów reaktywnych: przegląd aktualnych trendów”. Bieżące trendy w współbieżności : 510–584.