Nowa metoda testowania systemów sterowania komputerowego

Nowa metoda testowania systemów sterowania komputerowego

Naukowcy ze Szkoły Nauk Komputerowych Carnegie Mellon University opracowali nowa metodę systematycznego wykrywania błędów w lotniczych systemach unikania kolizji, sterowania bardzo szybkimi pociągami oraz innymi, złożonymi urządzeniami sterowanymi komputerowo, określanymi wspólnie mianem systemów cyber-fizycznych (CPS).

Koncepcja opracowana wspólnie przez Edmunda M. Clarke’a oraz Andre Platzera, profesorów nauk komputerowych Carnegie Mellon University, pozwoliła wykryć błędy w lotniczych manewrach unikania kolizji. Pozwoliła również udoskonalić Europejski System Sterowania Pociągiem (ETCS).

„Inżynierowie w coraz większym stopniu polegają na komputerach zwiększających bezpieczeństwo i precyzję systemów fizycznych, które współdziałają z realnym światem.” – stwierdził Clarke. „Systemy stają się coraz bardziej skomplikowane, a niewiele testowane, co praktycznie uniemożliwia wykrycie pewnych niuansów, które mogą prowadzić do katastrofalnych błędów. Nasza metoda jako pierwsza może zagwarantować, że te złożone cyber-fizyczne systemy będą działać właściwie, albo wygeneruje przykłady ilustrujące ich słabe strony.” – dodał.

W przypadku systemów unikania kolizji w powietrzu, Platzer i Clarke wykorzystali swoja metodę do przeanalizowania tzw. manewrów kołowych. Gdy dwa samoloty są na kursie kolizyjnym, jedną z technik pozwalających uniknąć kolizji jest nakazanie przez system pilotom, by skręcili w prawo i zatoczyli łuk tak, by znów móc bezpiecznie wrócić na kurs. Jednakże naukowcy z Carnegie Mellon pokazali, że jeżeli samoloty zbliżają się do siebie pod określonymi kątami, manewr wymijania w rzeczywistości wyprowadza samoloty na nowy kurs kolizyjny.

Podobnie, jak ma to miejsce w stworzonej przez Clarke’a metodzie Sprawdzania Modelu, która jest dziś najczęściej wykorzystywaną techniką wykrywania i diagnozowania błędów w złożonych systemach komputerowych, nowa metoda analizuje system pod kątem podstaw logiki.

Zasadnicza różnica polega na tym, że Sprawdzanie Modelu może przebadać każdy możliwy stan w systemie skończonym i dyskretnym, jak chip komputerowy. Jednakże CPS funkcjonujące w realnym świecie uzależnione są od nieskończonej liczby zmiennych. Nawet jeśli uda się rozwiązać równania różniczkowe opisujące te systemy, a często po prostu się nie da, najczęściej i tak niemożliwością jest wykorzystanie wyników do przewidywania zachowań systemu. Dlatego Platzer i Clarke opracowali algorytmy, które rozkładają systemy tak, by wydobyć z nich różne stałe. Te stałe natomiast mogą być wykorzystywane do badania logiczności całych CPS.

„Jeśli projekt systemu jest zdrowy, tak jak w przypadku Europejskiego Systemu Sterowania Pociągiem (ETCS), czy poprawionego systemu kontroli lotów, nasza metoda może tego dowieść.” – powiedział Plater. Natomiast, gdy istnieją wady, metoda te wiarygodnie generuje przykłady je ilustrujące. „Znalezienie kontrprzykładów jest proste. Trudniej udowodnić to, że zostały naprawione.” – dodał.

„Błędy w takich złożonych systemach cyber-zifycznych jak samochody, samoloty, chipy, czy urządzenia medyczne, są bardzo kosztowne w naprawie, a mogą zagrażać ludzkiemu życiu.” – wyjaśnił Plater. „W transporcie, procent nakładów na rozwój łożonych na projektowanie i testowanie nowego oprogramowania sterującego już dziś przekracza 50 i stale rośnie.”

(lk)