Skąd możemy wiedzieć, że metody formalne działają?

Ważnym celem metod formalnych jest udowodnienie poprawności systemów, za pomocą środków automatycznych lub kierowanych przez człowieka. Wydaje się jednak, że nawet jeśli podasz dowód poprawności, NIE będziesz w stanie zagwarantować, że system nie zawiedzie. Na przykład:

• Specyfikacja może niepoprawnie modelować system lub system produkcyjny może być zbyt skomplikowany, aby modelować, lub system może być wadliwy z powodu sprzecznych wymagań. Jakie techniki są znane w celu sprawdzenia, czy specyfikacja ma jakikolwiek sens?
• Proces sprawdzania może być również wadliwy! Kto wie, że te reguły wnioskowania są prawidłowe i zgodne z prawem? Co więcej, dowody mogą być bardzo duże, a skąd wiemy, że nie zawierają błędów? To jest sedno krytyki w „Procesach społecznych oraz dowodach twierdzeń i programów” de Millo, Liptona i Perlisa. Jak badacze nowoczesnych metod formalnych reagują na tę krytykę?
• W czasie wykonywania występuje wiele niedeterministycznych zdarzeń i czynników, które mogą poważnie wpłynąć na system. Na przykład promienie kosmiczne mogą zmieniać pamięć RAM w nieprzewidywalny sposób, a bardziej ogólnie nie mamy żadnych gwarancji, że sprzęt nie ucierpi na błędach bizantyjskich, wobec których Lamport udowodnił, że jest bardzo trudny do pokonania. Tak więc poprawność statycznego systemu nie gwarantuje, że system nie zawiedzie! Czy są jakieś znane techniki, które odpowiadają za omylność prawdziwego sprzętu?
• Obecnie testowanie jest najważniejszym narzędziem, które mamy do ustalenia, czy oprogramowanie działa. Wydaje się, że powinno to być narzędzie uzupełniające w stosunku do metod formalnych. Widzę jednak głównie badania, które koncentrują się na metodach formalnych lub testach. Co wiadomo na temat łączenia tych dwóch elementów?

Odnośnie 4: Dużo pracy łączy formalne metody i testowanie. „Testowanie metod formalnych” w Google ujawnia sporo pracy. Chociaż istnieje wiele różnych celów takiej pracy, jednym z kluczowych celów jest wygenerowanie bardziej efektywnych pakietów testowych. Ta rozmowa stanowi miłe wprowadzenie oparte na sprawdzeniu modelu.

Także w kwestii bezpieczeństwa oprogramowania , które zostało zredagowane bez pytania: formalne metody muszą ciężej pracować, aby dostarczyć je w tej dziedzinie. Zazwyczaj pisze się specyfikację oprogramowania i sprawdza, czy specyfikacja jest spełniona, a mianowicie, gdy dane wejściowe spełniają warunek wstępny, że dane wyjściowe spełniają warunki końcowe. Aby zapewnić bezpieczne oprogramowanie, należy również sprawdzić, czy oprogramowanie zachowuje się rozsądnie w przypadku danych wejściowych, które nie spełniają warunków wstępnych. (Jest to oczywiście równoważne z ustawieniem warunku wstępnego na wartość true dla wszystkich danych wejściowych.) Przestrzeń wszystkich danych wejściowych jest zwykle znacznie większa niż tylko dobrze sformułowane dane wejściowe, ale zazwyczaj jest to jedno miejsce, w którym nawet funkcjonalnie poprawne oprogramowanie może zostać naruszone, po prostu przez naruszając jego założenia.

Odnośnie do punktu 3: Pewne prace zostały wykonane w celu weryfikacji systemów w ustawieniach, w których awarie są jawnie modelowane, w tym wady logiki: uzasadnianie programów odpornych na awarie. Matthew Meola i David Walker. Europejskie sympozjum na temat programowania, 2010. Prace nad sprawdzaniem modeli probabilistycznych i weryfikacją probabilistyczną z pewnością w pewnym stopniu zajmują się również problemem wad.

Twoje punkty w kolejności:

• Prawidłowość wszystkich specyfikacji jest ostatecznie subiektywna: są postrzegane jako rozwiązanie problemu poprawnie według użytkowników lub nie. Nie da się uciec od tego, że jest to tworzenie oprogramowania i żadna metoda nie ma srebrnej kuli dla tego.
• Wiele pracy wymaga udowodnienia, że ​​proces jest prawidłowy w stosunku do założeń. Zwykle dostępne są informacje dla ekspertów w celu potwierdzenia tych zasad. Każda działalność człowieka jest obarczona błędem, ale bardzo sformalizowane systemy wykorzystujące dobrze zbadane podejścia są znacznie mniej podatne na błędy niż prawie wszystkie inne ludzkie procesy.
• W pewnym momencie każdy system ma tryb awarii poza zakresem tego systemu. Nadal lepiej jest wyeliminować wszystkie przewidywalne źródła błędów, nawet jeśli nie uwzględnisz niektórych nieprzewidywalnych.
• Testowanie i dowodzenie może z łatwością współistnieć. Testowanie jest mniej szczegółowym, bardziej ad hoc procesem, więc może się okazać, że mniej formalne prace zostaną wykonane. Ale możesz zainteresować się narzędziem takim jak QuickCheck, które uzupełnia testami dowody oferowane przez system typu Haskell.

Okazało się, że metody formalne działają od dawna. Bez nich nie poradzilibyśmy sobie ze złożonością projektowania nowoczesnych systemów cyfrowych (mikroprocesorów).

Żadnych mikro statków bez poddania logiki weryfikacji funkcjonalnej równoważności; bez poddawania FPU działaniu FV; bez protokołów spójności pamięci podręcznej podlegających FV (dzieje się tak od 1995 r.).

Pomijając oczywiste różnice między oprogramowaniem a inżynierskimi systemami fizycznymi (np. Mosty, w których można dodać czynniki bezpieczeństwa), pełnią one rolę matematyki inżynierskiej w CS. Jednak korzystanie z FM zawsze zależy od korzyści / kosztów. Testowanie Fuzz przynosi duże zyski w firmach takich jak Microsoft (Google SAGE w jednym slajdzie).

Nawet w obrębie mikroprocesora istnieją podsystemy (np. Rurociągi mikroprocesorowe), w których FV nie miało takiego samego wpływu jak gdzie indziej (np. FPU, gdzie konwencjonalne testy w ogóle nie były wykonywane w wielu przypadkach, gdy formalna ocena trajektorii symbolicznej wykazała brak błędów : Kaivola i in. CAV'09).

Formalne metody są również stosowane w syntezie artefaktów (kod, testy wysokiej jakości, harmonogramy optymalnego rozładowywania banków baterii, ...). Oczywiście wszystkie kwestie poruszone w pytaniu są dość aktualne i podobnie jak w przypadku innych zastosowań technologii, fałszywe reklamy muszą być rozpoznawane i unikane.

Odnośnie 2: jeśli system jest sformalizowany w asystencie dowodu (np. Twelf lub Agda lub Coq), a właściwości solidności i kompletności są weryfikowane, a dowody są wykonywane w tym kodowaniu, nie stanowi to problemu. Być może sformalizowałeś system, który nie opisuje tego , co zamierzałeś, ale przynajmniej nie będziesz mieć niepoprawnych dowodów lub zepsutego systemu, w którym rozumujesz.

Wydaje się jednak, że nawet jeśli podasz dowód poprawności, NIE będziesz w stanie zagwarantować, że system nie zawiedzie.

Tak, być może nie ma gwarancji . Metody formalne mają na celu wyszukiwanie i eliminowanie błędów oraz przekonywanie ludzi.

Jakie techniki są znane w celu sprawdzenia, czy specyfikacja ma jakikolwiek sens?

Możesz być zainteresowany narzędziami do sprawdzania modeli dla specyfikacji systemów formalnych .

Proces sprawdzania może być również wadliwy! Kto wie, że te reguły wnioskowania są prawidłowe i zgodne z prawem?

Myślę, że (z powodu twierdzenia o niekompletności Goedela) wykazanie systemu reguł wnioskowania jest konsekwentnie konieczne odwołuje się do jeszcze potężniejszego zestawu reguł wnioskowania.

Co więcej, dowody mogą być bardzo duże, a skąd wiemy, że nie zawierają błędów?

Mamy nadzieję, że ogromne dowody są sprawdzane przez niewielki moduł sprawdzania dowodów, który może być odczytany i zrozumiany przez ludzi w rozsądnym czasie. Jest to czasami nazywane „kryterium de Bruijna”. Jeśli uważasz, że weryfikator dowodu nie poświadczy niepoprawnego dowodu, musisz tylko sprawdzić weryfikator.

Czy są jakieś znane techniki, które odpowiadają za omylność prawdziwego sprzętu?

Co powiesz na język asemblera odporny na błędy ?

Widzę jednak głównie badania, które koncentrują się na metodach formalnych lub testach. Co wiadomo na temat łączenia tych dwóch elementów?

„Konferencja TAP poświęcona jest zbieżności dowodów i testów” .

Samo wyszukiwanie w „dowodach i testach” ma kilka dobrych trafień.

Jakie techniki są znane w celu sprawdzenia, czy specyfikacja ma jakikolwiek sens?

To zdecydowanie wezwanie do osądu. W inżynierii oprogramowania ludzie opracowali bardzo surową metodologię znajdowania / pisania / potwierdzania specyfikacji. Robią to prawdziwi ludzie i używają nieformalnego (w tym sensie nie matematycznego procesu), więc nadal podlega niekonsekwencji, ale pod koniec dnia odpowiada to, co ludzie chcą zweryfikować, nie mniej więcej.

Czy są jakieś znane techniki, które odpowiadają za omylność prawdziwego sprzętu?

Jasne, istnieje pole weryfikacji zwane weryfikacją środowiska uruchomieniowego, możesz także użyć sprawdzania modelu opartego na wykonaniu w rzeczywistym systemie działającym w całkowicie wirtualnym środowisku, z zastrzeżeniem określonego scenariusza ( włączyłem się w to z V-DS + APMC ). Jest to jednak wyraźnie poważny problem polegający na dodaniu interakcji między systemem a środowiskiem do procesu weryfikacji.

Widzę jednak głównie badania, które koncentrują się na metodach formalnych lub testach. Co wiadomo na temat łączenia tych dwóch elementów?

Wow, dzisiaj będę całkowicie bezwstydny i znów się zacytuję. Wraz ze współautorami pracujemy nad połączeniem sprawdzania i testowania modeli, możesz spojrzeć na listę publikacji byłego doktoranta z naszej grupy lub wyszukać „przybliżone sprawdzenie modelu probabilistycznego” lub „sprawdzenie modelu statystycznego” w dowolnej dobrej wyszukiwarce (praca wykonana przez Younes i in., Sen i in. Lub ja i in. Oraz wiele innych).

Być może bardzo interesują Cię prace Johna Rushby'ego , jednego z projektantów prover twierdzenia PVS, który jest ogólnie zainteresowany dokładnie tymi punktami, o których wspomniałeś. Możesz przeczytać ten klasyczny raport dla FAA na temat stosowania metod formalnych i certyfikacji systemów krytycznych (1993) oraz jego nowsze pisma na temat składania probabilistycznego, formalnego przypadku bezpieczeństwa z różnych dostępnych dowodów (testowanie, dowody, analizy itp.).