NASA i razvoj softvera

Ako niste veći dio života proveli na pustom otoku, daleko od bilo kakvog oblika komunikacije, teško da do sada niste čuli za američku svemirsku agenciju. Dobro poznatu širom svijeta pod svojim izvornim nazivom National Aeronautics and Space Administration. Ili, pod još poznatijom skraćenicom, NASA.

Od trenutka svojeg osnivanja (29.7.1958.), NASA je (samostalno ili u suradnji s drugim sličnim agencijama) zaslužna za neka od najpoznatijih i najdojmljivijih postignuća ljudskog djelovanja. Spuštanje ljudske posade na Mjesec, brojne misije bez ljudske posade na druge planete Sunčevog sustava, prvo djelo ljudskih ruku koje je izašlo van granica Sunčevog sustava (Voyager) – samo su neki od impresivnih rezultata djelovanja ove agencije. Nije zato nikakvo čudo da zbog svojih postignuća za koje danas znaju svi, NASA predstavlja dio popularne kulture te se njezin logo može pronaći i na brojnim predmetima u širokoj uporabi.

Pitanje koje se postavlja samo od sebe jest – a kakav utjecaj ima NASA na područje koje se nalazi u domeni ovog časopisa, to jest, na IT tehnologiju? Promatrajući NASA-ine uratke sa stanovišta hardvera, odgovor je nešto jednostavniji. Teško da u vlastitom domu ili tvrtki možete i želite imati NASA-ine hardverske proizvode poput dijelova satelita, raketa ili slično. Iako nije isključena upotreba ponekog korisnog hardverskog sklopa ili materijala. Sa stanovišta softvera, situacija je potpuno drugačija. Neki od proizvoda, iako prvobitno namijenjeni za posebne potrebe svemirske agencije, sasvim su upotrebljivi za korištenje i u drugim situacijama, odnosno u vlastitim softverskim projektima. Na primjer, napredne grafički orijentirane biblioteke izvorno zamišljene za vizualizaciju svemirskih podataka ili događaja, uz manje ili veće prilagodbe su sasvim upotrebljive za potpuno drugačije oblike vizualizacije.

Da ne spominjemo komunikacijski orijentirane biblioteke ili alate. Ako se nešto može uspješno koristiti u međuplanetarnoj komunikaciji, onda je vjerojatno iskoristivo i u običnoj „zemaljskoj“ komunikaciji.

https://software.nasa.gov/: Početna adresa za pretraživanje svih NASA-inih softverskih rješenja.

Da bi cijela stvar bila još zanimljivija, najčešće je riječ o javno dostupnim alatima ili bibliotekama koje se mogu neograničeno koristiti bez nekih posebnih ograničenja. Što je zapravo razumljivo samo po sebi. NASA u svojem djelovanju kao vladina agencija ovisi o sredstvima odobrenima od strane Kongresa, a to posredno znači da je zapravo financirana od strane američkih poreznih obveznika. Pa je onda sasvim logično da ti isti obveznici mogu koristiti ono za što su sami platili. A u pravilu, mogućnost korištenja najčešće nije ograničena samo na američke građane. Postoje određeni komercijalni izuzeci čija je primjena legalno dozvoljena samo drugim sličnim agencijama i ustanovama, ali NASA vrlo jasno ističe status svake softverske komponente kako pri korištenju ne bi bilo nikakve zabune.

Najveći problem u korištenju NASA-inog softvera je u tome da prvo treba znati da nešto uopće postoji, kako bi se od toga moglo krenuti u nekakvo dodatno istraživanje i korištenje. Srećom, rješenje postoji i nalazi se na web adresi https://software.nasa.gov/. Na ovoj adresi je sav dostupan softver organiziran prema kategorijama i omogućeno je pretraživanje prema različitim pojmovima, tako da je relativno jednostavno pronaći ima li NASA nešto što bi moglo biti iskoristivo.

Za svaki od izabranih alata je - osim točne adrese s koje se može preuzeti - naveden i oblik dozvole za korištenje (najčešće javno dostupno rješenje), eventualne specifičnosti u pogledu korištenja na točno određenom operativnom sustavu (ako postoje), te email adresa tima koji je radio na razvoju (u slučaju potrebe za dodatnim informacijama). Kako to sve skupa izgleda, možete vidjeti na pratećim slikama uz tekst za alat pod nazivom VERVE. Ovaj alat namijenjen je za daljinsku 3D vizualizaciju koja se može koristiti kod upravljanja različitim robotiziranim uređajima. „Sumnjivo slično“ različitim izvještajima koje NASA prezentira kao rezultate korištenja robotiziranih uređaja na Marsu, zar ne? Ako vam treba nešto slično za vaše vlastite inteligentne uređaje koje namjeravate dizajnirati i koristiti, na primjer, u modernoj poljoprivredi, zašto ne biste probali nešto slično?

Detaljnije predstavljanje dostupnih alata s tako opsežnog popisa daleko prelazi okvire pojedinačnog teksta u časopisu. Ovaj zadatak, na temelju do sada napisanog, prepuštamo vam da odradite sami prema vlastitim potrebama i sklonostima. Ono čime ćemo se malo detaljnije pozabaviti u nastavku je jedan malo „egzotičniji komad softvera“ čiji se prikazi rijetko pojavljuju u općim IT časopisima.

 VERVE https://software.nasa.gov/software/ARC-16457-1A: Sustav za daljinsku 3D vizualizaciju

VERVE - primjer korištenja: Primjer daljinske vizualizacije

NASALib i PVS

Riječ je o biblioteci na kojoj se u NASA-i kontinuirano radi već preko tri desetljeća! Ako to nije dovoljan dokaz njezine važnosti, onda također spomenimo činjenicu kako se upravo ova biblioteka nekoliko puta koristila u filmskom spektaklu „Marsovac“ (režisera Ridleyja Scotta iz 2015. godine) za pripremu sadržaja monitora u međusobnoj komunikaciji između Marsa i Zemlje. Iako treba biti pošten i priznati kako ta biblioteka sama po sebi nije baš pomogla Mattu Damonu da se kao slučajno ostavljeni istraživač na Marsu vrati na matičnu planetu, ipak pokazuje koliko je bitna za NASA-u.

NASALib (https://github.com/nasa/pvslib) predstavlja posebnu kolekciju formalnih biblioteka napisanih u posebnom jeziku PVS (Prototype Verification System). Trenutna verzija 7.1.2 (01.09.2023.) sastoji se od 63 osnovnih biblioteka, a za svoje korištenje zahtijeva PVS 7.1 (o tome malo više nešto kasnije).
Kako izgleda primjer sadržaja takve biblioteke (na primjer, na području koje se bavi opisivanjem teorema s područja teorije grafova) pokazano je u nastavku te na pratećim slikama uz tekst.

circuits[T: TYPE]: THEORY
%
% A circuit is a pre_circuit with no small loops (i.e. reduced)
%
%  pre_circuit?(G: graph[T], w: prewalk): bool = walk?(G,w) AND 
%                  w(0) = w(length(w)-1)
%

NASALib (https://github.com/nasa/pvslib): Biblioteka koja se koristi za opisivanje formalnih teorema na različitim područjima

NASALib / Graphs: Pregled teorema opisanog u biblioteci graphs

% NOTE: The extra term “w(1) /= w(length(w)-2)” in the definition of
%    cyclically_reduced? handles the special case where
%    w(0) is a small loop
%
%    removed “walk?(G,w)” from circuit? defn because it is in pre_circuit
%
BEGIN

 IMPORTING walks[T]

 G: VAR graph[T]


 reducible?(G: graph[T], w: Seq(G)): bool = 
   (EXISTS (k: posnat): k < length(w) - 1 AND w(k-1) = w(k+1))

 reduced?(G: graph[T], w: Seq(G)): bool = NOT reducible?(G,w)

%
% cyclically_reduced?(G: graph[T], w: Long_walk(G)): bool = 
%   reduced?(G,w) AND
%   (FORALL (j: below(length(w)-1)): reduced?(G,w^(j+1, length(w)-1) o w^(1,j))) 


 cyclically_reduced?(G: graph[T], w: Seq(G)): bool = length(w) > 2 AND
  reduced?(G,w) AND w(1) /= w(length(w)-2)

 circuit?(G: graph[T], w: Seq(G)): bool = %% walk?(G,w) AND
       cyclically_reduced?(G,w) AND
       pre_circuit?(G,w) 

END circuits

https://pvs.csl.sri.com/description.html: Početna web adresa za proučavanje PVS jezika

Allegro CL 11.0 Free Express Edition: Jedna od verzija LISP-a koja podržava PVS

Ako ste se ikada do sada bavili programiranjem (a ako čitate ovaj tekst, onda vjerojatno jeste), prikazani kod vam djeluje nekako poznato jer u njemu mogu uočiti strukture (na primjer BEGIN / END), varijable, petlje i slično, a opet se ne radi ni o jednom poznatom i raširenom programskom jeziku. O čemu je riječ?

PVS pripada posebnoj kategoriji jezika za definiranje specifikacija, koji se u IT svijetu koriste tijekom analize (vrlo složenih) sustava i zahtjeva, odnosno u dizajniranju budućeg sustava. To se u ovom slučaju izvodi na višoj razini nego kao što je to slučaj kod konkretnog programskog jezika. Za razvoj PVS jezika zaslužan je Computer Science Laboratory of SRI International (Menlo Park, California). Budući da se na razvoju PVS-a radi već čitav niz desetljeća, na početku razvoja je za implementaciju u konkretan softverski alat izabran programski jezik Lisp. U to vrijeme, programski jezik kojem su predviđali veliku budućnost na različitim područjima.

Detaljan opis PVS jezika, karakteristika trenutne verzije te pratećih softverskih alata dostupan je na web adresi https://pvs.csl.sri.com/description.html. U slučaju da sami radite na vrlo složenom novom sustavu čije ponašanje želite prvo formalno definirati kako biste izbjegli nepotrebne i skupe greške kod razvoja (nešto vrlo bitno za NASA-u), PVS je jedno od rješenja koje svakako možete uzeti u razmatranje.

Za stvarno korištenje PVS jezika i pratećih alata na računalima, potrebna je jedna od sljedeće dvije implementacije LISP jezika: Allegro Common Lisp (https://franz.com/downloads/clp/survey) ili Steel Bank Common Lisp – SBCL (https://www.sbcl.org/).

Dobra vijest je da su obje implementacije Lisp jezika slobodno dostupne za korištenje na različitim verzijama operativnih sustava: Linux, Windows i MacOS. Loša vijest je to što Lisp danas baš i nije previše popularan jezik među općom programerskom populacijom. Prema TIOBE indeksu, kojeg autor teksta često voli koristiti kao relevantni izbor za prikaz popularnosti nekog programskog jezika, Lisp se trenutno nalazi tek na 42. mjestu s postotkom korištenja od svega 0,28%. Dakle, skoro pa praktično beznačajno.

Lisp zapravo i ne morate učiti, ako samo namjeravate koristiti PVS bez potrebe za razumijevanjem pratećeg Lisp koda u pozadini. Međutim, ako poželite razumjeti kako je zapravo programiran PVS, odgovarajuće početnice za Lisp možete pronaći u okviru web adrese za preuzimanje Allegro verzije Lispa.

Ako se nikad niste susreli s Lispom, evo kratkog primjera kako se u Lispu priprema funkcija. Tek toliko da steknete uvid u to kako to zapravo izgleda.

(defun queue-put (queue element)
 “Store ELEMENT in the QUEUE and return T on success or NIL on failure.”
 (check-type queue queue)
 (let* ((get (queue-get-ptr queue))
   (put (queue-put-ptr queue))
   (next (queue-next queue put)))
 (unless (= get next)
  ;; store element
  (setf (svref (queue-elements queue) put) element) 
  (setf (queue-put-ptr queue) next) ; update put-ptr
 t)))

Svakako prilično drugačije u odnosu na različite C-olike jezike na kakve ste već navikli. Ako ništa drugo, najočitija razlika je da se mijenja uobičajena vrsta zagrada u kodu. U Lispu se obične zagrade koriste toliko često i intenzivno da među programerima čak kruži šala da uklanjanjem zagrada iz koda zapravo ne ostane više ništa. Srećom, u samom PVS-u je upotreba zagrada svedena na „normalne“ okvire.

Toliko o NASA-i i njezinom utjecaju na razvoj softvera. Ako u praksi uspijete iskoristiti nešto od slobodno dostupnih rješenja najpoznatije svemirske agencije, bit će nam vrlo drago ako smo vam pomogli da posegnete za nečim takvim.