Przemysł medyczny

Weryfikacja oprogramowania medycznego

Zabezpieczenie oprogramowania urządzeń medycznych przed poważnymi błędami w trakcie pracy

Testowanie i weryfikacja jakości oprogramowania jest definiowane jako zbiór działań, które prowadzą do ograniczenia ryzyka związanego z błędami oprogramowania. Najnowocześniejsze stymulatory serca mogą zawierać wewnętrzne oprogramowanie składające się z około 80 tysięcy linii kodu, a w pompy infuzyjne nawet 170 tysięcy linii kodu. Dlatego inżynierowie projektujący urządzenia medyczne muszą zwracać szczególną uwagę na strategię walidacji oprogramowania.

Wczesna integracja analizy statycznej kodu i technik formalnej weryfikacji w procesie tworzenia oprogramowania medycznego, a także proces walidacji mogą znacząco zredukować ilość błędów w oprogramowaniu. Te techniki mogą także dowieść poprawności i wykazać nieobecność błędów, które mogłyby pozostać niewykryte podczas tradycyjnego testowania oprogramowania, a tym samym spełnić wymagania agencji dopuszczających urządzenia medyczne do obrotu, np. FDA.

Wykrywanie błędów w oprogramowaniu medycznym

Polyspace Bug Finder jest narzędziem do statycznej analizy kodu używanym do sprawdzania fragmentów lub całości oprogramowania, aby w kodzie źródłowym C lub C++ znaleźć z maksymalną dokładnością błędy numeryczne, programistyczne lub problemy z przepływem danych. Program ten wykorzystuje metody polegające na analizie przepływu sterowania i danych w kodzie źródłowym i pozwala na właściwą selekcję i usunięcie błędów w oprogramowaniu na wczesnym etapie projektu.

Wykazanie braku błędów wykonania (Run-time errors)

Polyspace Code Prover wykorzystuje analizę statyczną kodu i metodę interpretacji abstrakcyjnej do udowodnienia, identyfikacji i rozpoznania błędów przepełnienia, dzielenia przez zero, wyjścia poza zakres indeksów tablicy i innych błędów w oprogramowaniu. Ta technika sprawdza wszystkie warunki i automatycznie diagnozuje poprawne lub zakończone niepowodzeniem operacje.

Wykorzystanie zaawansowanych technik weryfikacji opartych na metodach formalnych

Tradycyjne metody weryfikacji i testowania oprogramowania są często niewydajne i niewystarczające dla wbudowanego oprogramowania dla urządzeń medycznych. Polyspace Bug Finder i Polyspace Code Prover używają zaawansowanych technik weryfikacji opartych na metodach formalnych, które zapewniają optymalne rozwiązania spełniające wysokie wymagania weryfikacji i zapewniają integralność procesu tworzenia oprogramowania. Używając narzędzi do weryfikacji kodu na wczesnych etapach rozwoju oprogramowania można znaleźć i wyeliminować błędy, co jest najszybszym i najtańszym rozwiązaniem.