Wybuchnie, nie wybuchnie?

Osłabły już wspomnienia awarii elektrowni atomowej w Czarnobylu. Była ona jednak szokiem dla mieszkańców Europy. Wspominam czarnobylską tragedię jednak nie po to, by krytykować słabości klasycznej sztuki inżynierskiej. Chciałbym natomiast zwrócić uwagę na zagadnienia inżynierii oprogramowania.

Osłabły już wspomnienia awarii elektrowni atomowej w Czarnobylu. Była ona jednak szokiem dla mieszkańców Europy. Wspominam czarnobylską tragedię jednak nie po to, by krytykować słabości klasycznej sztuki inżynierskiej. Chciałbym natomiast zwrócić uwagę na zagadnienia inżynierii oprogramowania.

Na całym świecie przyjęta jest zasada, że w elektrowni atomowej funkcjonują trzy systemy komputerowe. Jeden "duży" steruje pracą całej elektrowni, a w szczególności reaguje na sytuacje awaryjne. Z góry jednak się przyjmuje, że system ten jest zbyt duży, by można mu było dostatecznie ufać. Z tego względu instaluje się dwa dodatkowe systemy, których jedynym zadaniem jest wyłączenie reaktora w razie awarii.

W zależności od kraju stosuje się różne, skarjnie odmienne metodyki. W Niemczech na przykład oba systemy awaryjnego wyłączania elektrowni są identyczne, co wynika z założenia, że tym sposobem zmniejsza się prawdopodobieństwo identycznej usterki obydwu. W Kanadzie z kolei systemy są zupełnie różne, dla uniknięcia podobnych błędów projektowo-implementacyjnych.

W końcu lat 80. w Darlington nie opodal Toronto powstała nowa elektrownia atomowa, pierwszy tego typu obiekt w Kanadzie wyposażony w całkowicie skomputeryzowane systemy wyłączające. Były to stosunkowo niewielkie programy, liczyły po kilka tysięcy linii kodu. Jeden zapisany był w Pascalu, drugi w Fortranie. Skąd jednak można było mieć pewność, że systemy awaryjne są skuteczne? Przecież wiadomo, że nie sposób sprawdzić poprawności takich programów tylko za pomocą testów. O pomoc zwrócono się do uczelni. Jeden z najbardziej znanych informatyków, David Longe Parnas podjął wyzwanie i postanowił sprawdzić w praktyce opracowane przez siebie metody weryfikacji i specyfikacji programów.

Zadanie było bardzo trudne. Okazało się, że dokumentacja specyfikacji i wzmagań oprogramowania była niejednorodna, niespójna, i niekompletna. Dzięki temu, że opóźnienie otwarcia elektrowni było bardzo kosztowne, właściciel obiektu, Ontario Hydro był gotów spełniać wszystkie "widzimisię" profesora.

Powstały trzy zespoły. Jeden z nich jeszcze raz pisał specyfikację badanych systemów używając do tego specjalnego podejścia tabelarycznego. Drugi zespół abstrahował z gotowych programów opis ich zachowania i zapisywał go również w postaci tabelarycznej. Trzeci porównywał oba opisy i albo uznawał, że dany fragment programu spełnia specyfikację, albo stwierdzał niezgodność. W tym drugim przypadku dwa pierwsze zespoły weryfikowały wcześniej opracowane tabele i przedstawiały nowe propozycje. Gdy liczba iteracji była zbyt duża, podejrzewano niezgodność implementacji ze specyfikacją. Tak było w kilku przypadkach.

Praca zespołów Parnasa była wykonywana bez wspomagających narzędzi programistycznych, więc zajęła bardzo dużo czasu i wiele kosztowała. W efekcie jednak uzyskano zmodyfikowane oprogramowanie systemów awaryjnego wyłączania elektrowni o znacznie większej wiarygodności. Na tyle dużej, że elektrownia uznała licencję.

Historia ta skłania mnie do dwu refleksji. Po pierwsze, pokazuje, w jak niebezpiecznym świcie żyjemy, nie zdając sobie nawet z tego sprawy. W wielu dziedzinach naszej aktywności nad bezpieczeństwem "czuwają" systemy informatyczne. Fakt że nie są one zweryfikowane wynika częściowo z kosztów, a także z niedojrzałości inżynierii oprogramowania. Dotkliwie brakuje powszechnie przyjętych metod projektowania i weryfikacji produktów informatycznych.

Po drugie, opisywany powyżej przykład pokazuje, jak różne jest na świecie podejście do wyższych uczelni. W Kanadzie rządowa agncja nie miała wątpliwości, do kogo udać się po rzetelną ekspertyzę. Muszę z żalem stwierdzić, że w Polsce jest bardzo mało podobnych przypadków.


TOP 200