Validace software PRPS (Primary Reactor Protection System) jaderné elektrárny Temelín
Software byl vytvořen firmou Westinghouse v Pittsbughu
Český úřad pro jadernou bezpečnost pro udělení povolení provozu reaktoru požadoval,
aby ochranné systémy byly podrobeny nezávislému hodnocení.
Team firem pro nezávislé hodnocení/analýzu:
- Firma SAIC (Washington, USA - kontrola požadavků
- Firma Nuclear Elektric (Gloucester) - kontrola bezpečnosti a konfigurace dat
- Firma Rolls Royce & Associates (Derby) - dynamické testování
- Firma TA Group - statická analýza kódu
Na základě našich referencí jsme byli přizváni k participaci na statické analýze
kódu PRPS.
Kód byl napsán v PLM 86 a část v ASM 86.
PRPS je založen na cca 80 ti procesorech 80486.
Analyzováno bylo cca 170 000 řádek zdrojového kódu.
Analýzu provádělo 10 lidí po dobu jednoho roku.
Statická analýza (její průběh):
- program nebyl spuštěn
- byly aplikovány matematické metody na programový text
- sledovalo se zda jsou nadefinované počáteční proměnné
- sledovalo se zda je využito všech cest v řízení toku kódu
Pro tuto práci se používal analytický softwarový nástroj MALPAS ver. 7 ( tento nástroj
byl vyvinut v době studené války pro analýzu software radarových systémů proti Ruským
balistickým raketám.)
Byl provozován na počítači VAX pod Open VMS v. 7.1
Analyzovaný kód byl nejprve MALPASem přeložen do IL (Intermediate language) jazyka.
Poté byla prováděna sémantická a syntaktická analýza. Tato technologie umožňovala
modelování procedur propagovaných z nižších vrstev kódu a tak analyzovat kód od
nejnižší vrstvy k nejvyšší. A to po jednotlivých vrstvách. Volání procedury z nižší
vrstvy bylo vždy simulováno modelem PROCSPEKem této procedury.
ZPĚT