În ziua de azi, devenim din ce în ce mai dependenți de echipamente controlate de software. Se pare că în viitorul apropiat, aceste echipamente vor deveni indispensabile pentru rutina noastră zilnică. Aceste echipamente domină atât de multe zone importante ale vieții noastre, încât cu greu ne putem descurca fără ele în activitatea zilnică. Prin urmare, este crucial ca acest echipament să fie fiabil în special în medii precum spitalele, aeronautica, automotive sau transportul feroviar.
Programele software care controlează un astfel de echipament sunt larg folosite și joacă un rol foarte important. Prin urmare, software-ul de calitate slabă pur și simplu nu este acceptabil. Pentru a produce software de calitate care să corespundă standardelor înalte, s-a depus un efort considerabil pentru verificare și validare, similar altor discipline din inginerie. În ciuda acestui efort, cea mai utilizată metodă de a crește calitatea programelor industriale este testarea. Totuși, aceasta nu este o metodă adecvată de a exclude erorile dintr-un program ("Testarea unui program poate fi o metodă foarte eficientă de a identifica bug-uri, dar este total inadecvată pentru a le demonstra absența" [37]). Nu trebuie să ne mire că pot eșua lucruri care au fost testate extensiv, uneori ducând la pierderi financiare sau, în cel mai rău caz, pierderi umane [129, 7].
Pentru a rezolva această problemă, noi propunem un raționament de sesiune. Introducem această abordare utilizând un protocol simplu de business între un Cumpărător (Buyer) și un Vânzător (Seller). De la bun început, Cumpărătorul trimite un identificator de produs către Vânzător. Vânzătorul oferă Cumpărătorului un preț pentru produsul solicitat. Cumpărătorul poate decide, conform regulilor interne, dacă acceptă produsul sau nu. Dacă Cumpărătorul acceptă produsul atunci Vânzătorul stabilește o conexiune cu Curierul (Shipper) pentru a aranja transportul produsului. Vânzătorul oferă informația necesară despre produs și deleagă conexiunea cu Cumpărătorul către Curier. Finalmente, Curierul și Cumpărătorul stabilesc detaliile finale legate de transport. Ca parte din acest proces Cumpărătorul oferă Vânzătorului adresa, iar Vânzătorul prezintă o dată de livrare către Cumpărător. Înainte de a începe dezvoltarea unui astfel de sistem, este recomandat să se specifice clar cum colaborează entitățile prin intermediul unei diagrame secvențiale precum în imaginea de mai jos. Această diagramă poate fi considerată o specificație grafică a raționamentului de sesiune. Transformarea se poate realiza automat.
Proiecția problemei acestui protocol se poate consulta mai jos:
unde sprice este definit astfel:
Prima specificație a protocolului buy_sp descrie comunicarea din punctul de vedere al Cumpărătorului. Protocolul nu ia în considerare că poate fi delegat/direcționat către Curier Shipper. Din punctul de vedere al Cumpărătorului delegarea este transparentă, dar pentru Vânzător, delegarea este explicită și deci inclusă în specificația protocolului ship_sp. Această specificație formulează protocolul din perspectiva Curierului și scoate în evidență procesul de delegare. Delegarea se întâmplă după ce se primesc decizia Cumpărătorului și detaliile produsului.
Alegerea Cumpărătorului este transmisă către Curier pentru a-l ajuta să consume/interpreteze protocolul. Acest proces este necesar datorită sincronizării timpurii a proceselor. Dacă s-ar permite sincronizarea târzie a proceselor, permițându-se părților să stabilească conexiuni la cerere, atunci libertatea deadlock a procesului de comunicare ar putea fi foarte greu probată. Din perspectiva delegării, specificația este precisă și scoate în evidență starea canalului de transmisie, stare ce trebuie asigurată de emițător și preluată de destinatar.
Având în vedere stilul de verificare anticipativă a abordării noastre, executarea simbolică a metodei seller începe prin asumare precondiției sale, adică:
, unde ~buy_sp și ~ship_sp sunt calculate utilizând reguli duale. Apoi, după executarea simbolică a liniei 1, starea simbolică a programului reflectă primirea unei valori int prin canalul cb înlăturând ?int din specificația lui cb. Formal, dacă precondiția lui receive rămâne validă, următoarea stare simbolică include cadrul rezultat după oferirea precondiției alături de postcondiția metodei. Același raționament se aplică liniilor 2-3 și 5-7, cu observația că linia 3 reprezintă o alegere/opțiune în specificația lui cb: ((?1; :::) V ?0), în timp ce linia 22 denotă o delegare. Este important de remarcat că abordarea noastră este compozițională, e.g. verificarea metodei send respectă aceeași regulă indiferent dacă este folosită pentru delegare sau doar pentru trimiterea unei valori int pe un canal specific.
Contribuția noastră ține de îmbunătățirea siguranței globale, evaluând corectitudinea specificației protocolului din cadrul unui limbaj imperativ cu scop general.
R. Hu, N. Yoshida, and K. Honda. Session-Based Distributed Programming in Java. In ECOOP 2008 Object-Oriented Programming, Lecture Notes in Computer Science, pages 516-541. Springer, 2010b.
W.-N. Chin, C. David, H. H. Nguyen, and S. Qin. Automated Verification of Shape, Size and Bag Properties Via User-Declined Predicates in Separation Logic. Sci. of Comp.Prog., 77:1006-1036, 2012.