Agenda 1. Runtime Verification

2. Paradigma MOP

3. Java MOP

4. SOA Monitoring

5. Concluzii

1. Runtime Verification Notiunea de verificare implica trei tehnici de baza:

demonstrarea teoremelor – permite demonstrarea corectitudiniiunui program prin utilizarea mecanismelor matematice

model checking – metoda automata de verificare, se aplica inspecial sistemelor cu stari finite; se bazeaza pe logici temporale

testarea – denota procesul de gasire a bugg-urilor unui sistem

1. Runtime Verification vs Model Checking Idea logicilor temporale – o formula nu este adevarata sau falsa

intr-o maniera statica intr-un model (contraex. LP)

Modelele logicilor temporale contin cateva stari, iar o formulapoate fi adevarata in unele dintre aceastea si falsa in altele.

Modelul este un sistem tranzitional, iar proprietatile formuletemporale.

1. Runtime Verification vs Model Checking Verificarea unui sistem implica urmatorii pasi:

folosim un limbaj descriptiv a model checker-ului

codificam proprietatea(ile) vizate utilizand limbajul de specificatiea model checker-ului

rulam model checker-ul, avand ca input: modelul si formulele

1. Runtime Verification Verificarea la runtime este privita ca o tehnica de verificare

usoara, complementara tehnicilor de tipul: model checking sitestare.

Un esec software ("software failure") este o deviatie dintre uncomportament observat si comportamentul necesar al unui sistemsoftware.

Un "fault" este identificat de catre deviatia starii curente in raport custarea asteptata a sistemului.

O eroare este o greseala ce apartine programatorului, greseala cerezulta intr-un “fault” si posibil intr-un esec.

1. Runtime Verification - Monitoare Verificarea la runtime vizeaza doar detectarea violarii sau

respectarii proprietatilor de corectitudine.

In literatura de specialitate executia unui sistem software ("run") esteprivita ca o posibila secventa infinita de stari ale sistemului.

Starile pot fi alcatuite din asignari de variabile sau secvente de actiuniemise si efectuate de catre un sistem.

Formal, o executie este considerata ca un posibil cuvant infinit sautrace.

Executia unui sistem este un prefix finit al acelui run, trace finit.

1. Runtime Verification - Monitoare Verificarea executiei unui sistem in raport cu o proprietate de

corectitudine este responsabilitatea unui monitor.

Functionalitatea de baza a unui astfel de monitor este de a decidedaca executia curenta satisface o anumita proprietate.

Putem extrapola si afirma ca verificarea la runtime din punct devedere matematic si formal incearca dezvoltarea de tehnicicapabile sa ofere un raspuns in ceea ce priveste incluziunii unuicuvant (trace) intr-un limbaj (set de stari ale unui sistem).

1. Runtime Verification - Monitoare Monitorizare online - implica folosirea unui monitor pentru a

verifica executia curenta a unui sistem.

Monitorizare offline - implica folosirea unui monitor pentru amultime finita de executii inregistrate

In ceea ce priveste verificarea la runtime, monitoarele suntgenerate automat dintr-o specificatie de nivel inalt.

1. Runtime Verification - „Safety properties” Prin conceptul de proprietate de siguranță se încearcă

surprinderea unui proprietăți comportamentale corelată cutrace-uri de execuției

Caracteristica de bază este dată de faptul că odată încălcată(proprietatea), aceasta nu mai poate fi satisfăcută

Proprietatile de siguranta pot fi aplicate peste trace-uri finitesi/sau infinite

1. Runtime Verification – Definire formalamonitoare sintaxa formală: Ḿ=(S, s0, M: S x ∑ → S)

un monitor este un automat specializat, fară stări terminale

proprietăți ale unui monitor:

Ĺ*( Ḿ ) = { w ϵ ∑* | M (s0,w) ↓}

Ĺ (Ḿ ) = { u ϵ ∑ | M (s0,w) ↓} for all w ϵ prefixes(u)}

Ĺ*, (Ḿ ) = Ĺ*( Ḿ ) Ĺ ( Ḿ )

1. Runtime Verification – Definireamecanismului de functionare a monitoarelor ideea generală de funcționare a unui monitor este:

automatul specializat, va fi declanșat de evenimentele generate de cătresistemul observant (în mod concret sistemul este reprezentat de literele din∑)

fiecare eveniment nou primit trece monitorul din starea curentă în altăstare

trecerea este dictată de funcția de tranziție M

dacă monitorul se blochează (mai exact în cazul în care funcția de tranzițieeste nedefinită pe starea curentă și evenimentul curent), proprietateamonitorizată este declarată ca fiind încălcată în acel punct

procesul de monitorizare este descris de necesitatea verificării apartenței unuicuvânt w ϵ ∑* la prefixes(w), unde prefixes(w): ∑*→Ƥ(∑*)

1. Runtime Verification – Amendament Sisteme tranzitionale (modele software)

Forma generala: Ḿ= (S, →, L) – S –multimea starilor; → relatiebinara (relatie de tranzitie); L – functie de etichetare L: S ->Ƥ(Atoms). Pentru fiecare stare s, avem și o multime de propozițiiatomice L(s), propoziții ce dețin valoarea de adevăr pentru starea s.

Tranzițiile sunt: so → s1, so → s2, s1 → s0,

s1 → s2, s2 → s2.

Etichetele sunt: L(so)={a,b}, L(s1)={b,c}, L(s2)={c}

2. Monitoring-Oriented Programming Modelul MOP

2. Monitoring-Oriented Programming Din perspectiva paradigmei MOP, cerintele unui sistem apar sub

forma unor specificații formale, aceste specificații prezentându-se ca adnotări.

Flexibilitatea acestei abordări constă în faptul că respectiveleadnotări pot fi inserate în diferite locatii ale programului (însensul unui sistem software); locurile de insertie sunt definite decatre programator.

2. Monitoring-Oriented Programming Pe baza specificatiilor formale se va genera un asa-numit „cod de

monitorizare”, acest cod este acelasi cu limbajul de implementareal sistemului peste care vrem să adaugam monitoarele.

Evenimentele (element de sintaxă din cadrul unei specificațiiMOP –„event”) sunt cele care facilitează verificarea proprietățilorla diferite locuri în cod.

Un monitor trebuie privit sub forma unui automat specializat,fară stări terminale.

2. Monitoring-Oriented Programming Sintaxa generala a unei specificatii MOP

2. Monitoring-Oriented Programming Prima componentă (header-ul) va contine informatii despre

procesul de monitorizare, generare si integrare. Pot fi adăugate siinformatii privitoare la scopul si logica folosită la definirea unorproprietati in vederea monitorizarii.

În cea de a doua componenta (corpul) proprietatile monitorizatesunt declarate, acele formule vor fi asociate cu anumite plug-in-uri logice, în concordanta cu semnatica formala utilizata.

Ultima componentă (handler-ul) este reprezentată de coduldeclarat de programator pentru cazul in care proprietatea esterespectata sau incalcata.

3. JavaMOP Tool ce faciliteaza declararea de specificatii MOP, in urma

procesului de generare vom avea un cod de monitorizare cusintaxa specifica limbajului de programare Java.

La nivel de arhitectura JavaMOP prezinta o structura de tipclient-server:

partea de client contine un modul pentru interfata si procesorul despecificatii, special dezvoltat pentru JavaMOP

partea de server conține un dispecer de mesaje si plug-in-uri logicepentru Java, acestea suporta formalisme ca: ptLTL, ftLTL, ERE siCGF

3. JavaMOP Principalul rol al acestei tehnologii este de a translata output-ul

furnizata de egine-urile logice in aspecte (sintaxa este unaproprietara AspectJ). Etapa finala de integrare apartinecompilatorului AspectJ care are rolul de a unifica programuloriginal cu aspectele generate.

3. JavaMOP

3. JavaMOP

3. JavaMOP Exemplu nr.1 (din care reiese necesitatea folosirii JavaMOP)

Vector v=new Vector();

v.add(new Integer(10));

Iterator i =v.iterator();

v.add(new Integer(20));

System.out.println(i.next());

JVM: ConcurentModificationException

Proprietatea unui iterator: fail-fast

3. JavaMOP – exemplu nr.1 package mop;

import java.io.*;import java.util.*;

HasNext(Iterator i) {event hasnext after(Iterator i) : call(* Iterator.hasNext()) && target(i) {} event next before(Iterator i) : call(* Iterator.next()) && target(i) {}

ptltl : next implies (*) hasnext

@violation {System.out.println("next called without hasNext!");

}}

Specificatiamonitorului

3. JavaMOP – exemplu nr.2 monitorizarea unei proprietăți ptLTL de forma : (b→ • a), unde în cazul de față b

reprezintă returnarea unei liste de produse, iar a reprezintă autentificarea

rolul proprietății de mai sus este de a verifica accesul la o resursă în contextul unui SW

package mop;

import searchFarm.ServiciuWebSearchFarm

IsAuthentificated(ServiciuWebSearchFarm swsf) {

event authenticate before(ServiciuWebSearchFarm swsf) :

call(* ServiciuWebSearchFarm.authenticate()) && target(swsf) {}

event getFarmProdList after(ServiciuWebSearchFarm swsf) :

call(* ServiciuWebSearchFarm.getFarmProdList()) && target(swsf) {}

ptltl : getFarmProdList implies (*) authenticate

@violation { System.out.println("Operatia nu poate fi realizata fara a fi autentificat!"); }

}

4. SOA Monitoring Consta in folosirea paradigmei MOP pentru tehnologiile

specifice “Service Oriented Arcitecture“:

Servicii Web

Procese de afaceri

Componente software

4. SOA – Definire concepte Conceptul fundamental al SOA este acela de serviciu,

proprietățile sale putând fi enumerate (de menționat că unserviciu este privit sub forma unei componente software):

este definit de o interfata ce poate fi independenta de platforma

este accesibil folosind o retea

operatiile definite in interfata vor realiza operatiile esentiale(„business functions”), realizarea lor vizand obiectele de tipbusiness

interfata unui serviciu si implementarea acestuia pot fi „decorate”cu extensii ce isi vor face simtita prezenta la „runtime”.

4. SOA – Proprietati generale ale unuiserviciu Interfata independenta de platforma: functionalitatea unui

serviciu trebuie definita de catre o interfata externa. Principalulrol al unui serviciu este acela de a adresa si de a rezolva aspectelegate de integrare.

Accesibil prin intermediul unei retele: este un principiufundamental si consta in capacitatea de a accesa functionalitătileunui serviciu intr-o manieră remote.

4. SOA – Proprietati generale ale unuiserviciu Operatii realizate asupra „business object”-urilor: aceasta

proprietate se refera la indeplinirea/executia unor functionalitatispecifice unui domeniu al aplicatiei supuse viziunii SOA.

Decorabilitate: acest concept face referire la posibilitatea de adecora, adnota operatiile serviciului, astfel incat sa fie surprinseatat aspectele functionale, cat si cele nefunctionale (WS-RealiableMessaging, WS-SecureConversation).

4. SOA - Clasificare Distingem urmatoarea clasificare a serviciilor:

servicii entitate - un serviciu de tip entitate reprezinta una sau maimulte entitati de tip „business”.

servicii functionale - deseori acest tip de serviciu nu are oreprezentare in cadrul unui model de afaceri; poate fi reprezentattotusi in cadrul unei diagrame de tip secventa. Trebuie mentionatca un serviciu functional este serviciul orientat spre tehnologie si nuspre business (operatii de logging și notificare) .

servicii de tip proces - un serviciu de tip proces este alcatuit dintr-oserie de task-uri (activitati) relationate. Aceste activitati pot fiindeplinite in cadrul granitelor unui singur domeniu de business,peste mai multe domenii de business sau intre organizatii.

4. SOA – Principii modelare Tehnicile arhitecturale ce se impun în procesul de modelare:

Generalizarea presupune analiza serviciului pentru adetermina definirea la nivel de concept a serviciului respectiv.Putem face o analogie cu programarea orientata-obiect; oastfel de analiza in contextul OO poarta numele de relatie detip „IS-A”. O generalizare exagerata poate evita surprindereaaspectelor relevante pentru respectivul serviciu, diminuandposibilitatea refolosirii; prin acest fapt se încalca unul dintreprincipiile de baza ale SOA.

4. SOA – Principii modelare

Descompunerea presupune determinarea elementelorcandidat pentru realizarea unei compuneri. O astfel deabordare de cele mai multe ori duce la descoperirea serviciilorde tip entitate sau a serviciilor functionale, servicii cetrebuiesc separate. Ca principiu general, cu cat serviciul estemai bine izolat, in sensul lipsei unei interdependenteexcesive, cu atat mai mult respectivul serviciu va putea fifolosit/refolosit si eventual integrat intr-un scenariu de“compunere “.

4. SOA – Principii modelare

Agregarea presupune analiza serviciului in vedereadeterminarii contextului din care face parte, in sensulrelatiilor de interdependenta. Elementele ce tin de agregarepot fi clasificate ca fiind procese existente, servicii sau chiarservicii-candidat. De asemenea, putem face o paralelă cuprogramarea orientata-obiect; procesul poarta numele decautare a relatiilor de tip „HAS-A”.

4. SOA – Principii modelare Aplicarea principiilor de mai sus este necesara in vederea

descoperirii serviciilor ce pot fi compuse.

Vom prezenta si principiile aditionale:

Reutilizabilitatea

Securitate

Interoperabilitate

SLA

Granularitate

Contract

Proces

4. SOA – Principii modelare Reutilizabilitatea: scopul final al acestei tehnici este de a

furniza un contract; pe baza analizelor sistemului se urmareste inprimul rand gradul de refolosire pe care il poate avea respectivulserviciu.

Securitatea: de obicei, acest aspect este luat in considerare lanivelul aplicatiei. In cazul modelarii serviciilor componentele cevor asigura securitatea vor fi încadrate intr-un model general desecuritate asociat respectivei solutii SOA, model care va contineSAML (Security Assertion Markup Language), un „policyenforcement”, specificatii privind securitatea transportului,semnaturi digitale, Kerberos etc.

4. SOA – Principii modelare Interoperabilitate: in contextul programarii orientate-

obiect, obiectele comunica doar cu alte obiecte; in cazulserviciilor, acest principiu nu este aplicat, ideea de bazafiind aceea de comunicarea intre componente softwareimplementate pe platforme software eterogene.

SLA-uri: serviciile, asemenea sistemelor pe care le expun,trebuie sa aiba definite contracte, „agreement-uri” la nivelde servicii. Aceste tipuri de specificatii sunt extrem deimportante deoarece un anume serviciu intr-un contextSOA va fi reutilizat de mai multe ori, in contexte diferite,implicit, procese diferite.

4. SOA – Principii modelare Granularitate: un serviciu de cele mai multe ori va fi integrat

intr-un mediu in care serviciile evolueaza in ceea ce privesteinteractiunea, implicit interoperabilitatea dintre diferite sisteme.Definirea unei cat mai bune granularitati (functionalitatispecifice unui anume business, nu exista un grad mare deinterdependenta) reprezinta garantia reutilizarii respectiveicomponente software.

4. SOA – Principii modelare Contract: in cadrul unui model (in sensul unei aplicatii SOA),

definirea unui contract consta in identificarea elementelornecesare la nivel global. Unele dintre elemente vor fi atributeserviciilor, iar altele vor servi ca metadate expuse in cadrulcontextului WS-MetaDataExchange. Trebuie mentionat faptul cadeseori vor fi luate in calcul si elementele nefunctionale, deobicei declararea acestora fiind facilitata de tehnologiile ce oferasuport pentru dezvoltarea de aplicatii orientate SOA.

4. SOA – Principii modelare Proces: analiza de proces difera de abordarile traditionale (in

sensul construirii de sisteme capabile sa realizeze un set clar defunctionalitati) axate pe paradigma orientata-obiect; importantalor in contextul IT este data de posibilitatea de a translata, areprezenta un proces de afaceri sub forma unui serviciu web(ultimul standard elaborat de OASIS – WS-BPEL 2.0).Numeroase proiecte (tehnologii ce permit dezvoltarea software)ofera ca solutie pentru realizarea mecanismului de orchestrare(opusul conceptului de coreografie specific mai mult serviciilorweb clasice – „WS-Choreography”) suport pentru lucrul cuprocese de afaceri si expunerea lor ca servicii.

5. Concluzii JavaMOP si MOP sunt centrate pe flexibilitate si optimizarea

monitorizarii

Provocarea consta in elaborarea unui set de tehnici si solutiicapabile sa monitorizeze la runtime aplicatiile software ceapartin viziunii SOA.

Sfarsit Intrebari?