ABONAMENTE VIDEO REDACȚIA
RO
EN
NOU
Numărul 144
Numărul 143 Numărul 142 Numărul 141 Numărul 140 Numărul 139 Numărul 138 Numărul 137 Numărul 136 Numărul 135 Numărul 134 Numărul 133 Numărul 132 Numărul 131 Numărul 130 Numărul 129 Numărul 128 Numărul 127 Numărul 126 Numărul 125 Numărul 124 Numărul 123 Numărul 122 Numărul 121 Numărul 120 Numărul 119 Numărul 118 Numărul 117 Numărul 116 Numărul 115 Numărul 114 Numărul 113 Numărul 112 Numărul 111 Numărul 110 Numărul 109 Numărul 108 Numărul 107 Numărul 106 Numărul 105 Numărul 104 Numărul 103 Numărul 102 Numărul 101 Numărul 100 Numărul 99 Numărul 98 Numărul 97 Numărul 96 Numărul 95 Numărul 94 Numărul 93 Numărul 92 Numărul 91 Numărul 90 Numărul 89 Numărul 88 Numărul 87 Numărul 86 Numărul 85 Numărul 84 Numărul 83 Numărul 82 Numărul 81 Numărul 80 Numărul 79 Numărul 78 Numărul 77 Numărul 76 Numărul 75 Numărul 74 Numărul 73 Numărul 72 Numărul 71 Numărul 70 Numărul 69 Numărul 68 Numărul 67 Numărul 66 Numărul 65 Numărul 64 Numărul 63 Numărul 62 Numărul 61 Numărul 60 Numărul 59 Numărul 58 Numărul 57 Numărul 56 Numărul 55 Numărul 54 Numărul 53 Numărul 52 Numărul 51 Numărul 50 Numărul 49 Numărul 48 Numărul 47 Numărul 46 Numărul 45 Numărul 44 Numărul 43 Numărul 42 Numărul 41 Numărul 40 Numărul 39 Numărul 38 Numărul 37 Numărul 36 Numărul 35 Numărul 34 Numărul 33 Numărul 32 Numărul 31 Numărul 30 Numărul 29 Numărul 28 Numărul 27 Numărul 26 Numărul 25 Numărul 24 Numărul 23 Numărul 22 Numărul 21 Numărul 20 Numărul 19 Numărul 18 Numărul 17 Numărul 16 Numărul 15 Numărul 14 Numărul 13 Numărul 12 Numărul 11 Numărul 10 Numărul 9 Numărul 8 Numărul 7 Numărul 6 Numărul 5 Numărul 4 Numărul 3 Numărul 2 Numărul 1
×
▼ LISTĂ EDIȚII ▼
Numărul 71
Abonament PDF

Raționament de sesiune

Kiss Tibor
Software engineer @ Accenture



PROGRAMARE

Î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.

Referințe

  1. 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.

  2. 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.

  3. M. Dezani-Ciancaglini, D. Mostrous, N. Yoshida, and S. Drossopoulou. Session types for object-oriented languages. In ECOOP 2006 - Object-Oriented Programming, pages328-352. Springer, 2006a.

NUMĂRUL 143 - Software Craftsmanship

Sponsori

  • Accenture
  • BT Code Crafters
  • Accesa
  • Bosch
  • Betfair
  • MHP
  • BoatyardX
  • .msg systems
  • P3 group
  • Ing Hubs
  • Cognizant Softvision
  • Colors in projects

Kiss Tibor a mai scris