FUJABA vs. CHARMY: confronto della feature model checking

(Analisi e Testing di Sistemi a Componenti)Universit degli Studi dellAquilaFACOLTA DI SCIENZE MM.FF.NN.Corso di Laurea in Informatica ANNO ACCADEMICO 2005 2006

Prof. Henry Muccini Stud.ssa: Romina Spalazzese matr.162992

Road MapCos il Model Checking (MC)Caratteristiche dellapproccio FujabaCaratteristiche dellapproccio Charmy Confronto e considerazioniFuture works

1. Model CheckingTecnica automatica basata sul modello: controlla se una determinata propriet valida per un certo modello di un sistema. Risultato: true o false + controesempio

STEP 1 - Crea un finite state model (FSM) del sistemaSTEP 2 - Specifica propriet critiche di correttezza (safety, liveness)STEP 3 Valida il modello rispetto alle specificheVANTAGGI- Automatico- Esaustivo - Genera controesempio

SVANTAGGI- State explosion problem- Skills in metodi formali

2. FUJABA: cosCASE tool open-source che supporta modellazione e verifica di modelli UML

Tra tutte le feature [2] di Fujaba Real-Time Tool Suite, consideriamo laprogettazione e model checking di modelli per safety-critical systems (UML/RealTime)

Problemi nel model checking di modelli UML/RT: 1. State explosion problem 2. Difficile integrazione standard model checking nel processo di design incrementale ed iterativo

Soluzione proposta: applicare un approccio di verifica formale composizionale ed iterativo su un sottinsieme di nozioni UML 2.0

2. FUJABA: approccio MC [3]Basato su modelli UML 2.0Incrementale: design e model checking Iterativo: design e model checking Composizionale: model checking

CosaSTRUTTURA: Real-Time Component DiagramCOMPORTAMENTO: Real-Time State Chart (RTSC) + formule Timed Computation Tree Logic (TCTL)

ComeModella pattern e componenti sw=> sistema

2. FUJABA overview [1]Input Uppaal : - Flat Timed AutomataTimed Computation Tree Logic

2. Esempio: mechatronic rail system [3] SAFETY-CRITICAL ASPECT: coordinazione tra le unit di controllo della velocit degli shuttles =>HARD RT CONSTRAINTProblema: ridurre consumo energetico coordinando gli shuttles per formare convogli on-demand

Per ottenere economia piccole distanze tra shuttles Shuttles autonomi applicano una tecnologia di guida lineare Viaggiano sul sistema ferroviario dei treni standard

2. Coordination pattern in FUJABA [3] [4]COORDINATION PATTERN = ROLES + CONNECTORS descrivono comunicazione, interazioni tra le componenti del sistema

vincolati da constraints specificati in formule attori della comunicazione descritta dal pattern

devono soddisfare invariants e constraints

comportamento specificato tramite RTSC collegano PORTS che raffinano i roles e permettono la comunicazione

comportamento specificato tramite RTSC

2. Componenti e sistema in FUJABACOMPONENTI SW: costruite integrando e raffinando role del pattern coinvolto. Devono rispettare comportamento specificato dai roles invariants

SISITEMA: costituito istanziando un insieme di componenti e patternComportamento necessario per coordinare due shuttle successiviES. Non ci devessere collisione in caso di frenata improvvisaES. Deve frenare con potenza ridotta se in modalit convoglioComportamento specifico per il tipo di role ES. Deve frenare con piena potenza (invariant)ES. RearRole non pu essere in mode convoy se FrontRole in mode no convoy (pattern constraint)

2. Fujaba screen shots

2. Approccio composizionaleProgettazione patterns e roles

Verifica di ogni pattern individualmente

Progettazione dei tipi di componenti e del loro comportamento

Verifica di ogni tipo di componente

Costruzione del sistema istanziando componenti e connettendo porteModel checking per verificare constraintsComponente corretta se soddisfa invariants dei refined roles e se non ci sono deadlockDA NOTARE: assicura corretta composizione semantica a partire dalla corretta composizione sintattica (rigorosa)Pattern constraints in ATCTL formulas

2. Approccio incrementale [1]STEP 1) seleziona pattern o componenti composti minimali che contengono tutti gli elementi referenziati dalla propriet

STEP 2) controlla la propriet :se soddisfatta, fine

altrimenti estende aggiunge componenti interconnesse a quelle gi selezionate se non ci sono pi componenti interconnesse, seleziona i vicini uno ad ogni passo e li aggiunge

2. Consistency management [4] Consistenza tra propriet ed elementi strutturali e comportamentali

Mantenuto lo stato della propriet- TRUE propriet rispettata- FALSE propriet non rispettata- UNSAFE elementi del modello nellultimo check potenzialmente inconsistentiRegole:Comportamento di un pattern o di un role cambiato => marcate UNSAFE le sue propriet + quelle associate alle componenti coinvolte

2) Componente o il suo comportamento modificato => marcate UNSAFE le propriet correlate

Check solo sulla parte unsafe

2. Sintesi di pattern da scenari [5] [6]SceBaSy Plugin per Fujaba Real Time Tool Suite per sintetizzare real-time coordination pattern da Sequence Diagram UML 2.0

Idea: esprimere il comportamento desiderato tramite scenari parametrizzati con vincoli sul temposintetizzare automaticamente gli scenari in TCGsintetizzare automaticamente TCG in RTSCfae analisi per evidenziare errori (sintattici, conflitti tra scenari, deadlock)quando RTSC sono verificati, sintetizzare automaticamente i coordination pattern

Sequence diagramTime constraint graph TCGRTSCModel chedckingCoordination pattern

3. CHARMY: cosCharmy un framework che permette la progettazione e la verifica formale di sistemi software

Tra tutte le festure di Charmy tool [7] consideriamoprogettazione e model checking di architetture software rispetto a requisiti funzionali

Problemi nel fare model checking: 1. State explosion problem 2. Skills in formal specification

Soluzione proposta [8]: applicare un approccio di verifica iterativo su modelli basati su UML senza dover dare una specifica formale

3. CHARMY: approccio MC e overviewModelli basati su UML Check a livello architetturaleIncrementale: design e model checking Iterativo: processoComposizionale: model checking di sa basate su middlewareCosaSTRUTTURA: Component DiagramCOMPORTAMENTO: State Diagrams + Scenari PSCComeModella architettura software, comportamento delle componenti e propriet [8]

3. Property Sequence Chart (PSC) [9] [10] [14]Wizard W_PSC: domande testuali per la traduzione dei requisiti in scenari

3. Charmys screen shots

3. Approccio composizionale [11]Idea: decomporre verifica di un insieme di propriet dellarchitettura sw in verifica di propriet locali sulle singole componenti architetturali per mezzo del compositional reasoningDef: A architettura sw, Z insieme di propriet soddisfatte da A, M middleware, P insieme di propriet soddisfatte da M, S sistema risultante da A + M + I (interfacce)Scopo: dimostrare che anche S soddisfa Z (sotto alcune assunzioni) propriet locali alle componenti

propriet sulle interazioni componenti-interfacce

propriet di comportamento di M

-propriet sulle interazioni interfacce-middleware

3. Approccio iterativo ed incrementale [8]Specifica architettura e propriet iniziali

Verificare se larchitettura garantisce requisiti funzionali espressi dalle propriet. Soddisfatti ?

3a. Termina il processo

3b. Raffina i modelli e le propriet focalizzandosi su parti critiche dellarchitettura e torna a verificare la SA

3. Consistency checks [12][13] Valida modello dinamico della SA rispetto a coordination requirementsSTEP 1- Coordination policies catturate a livello requisitiSTEP 2- Coordination policies usate per guidare descrizione architetturaleSTEP 3- SA validata rispetto ai coordination requirements STEP 4- SA utilizzata per guidare coordination model

INPUT Macchina a stati delle componenti (tradotte in Promela) Scenari (tradotti in formule LTL)

Spin verifica se il comprtamento espresso degli scenari ben implementato sul modello Promela- prima validazione del modello architetturale che dopo pu essere usato per fare analisi di safety e liveness

Spin pu verificare propriet di deadlock o violazioni di constraint siulle macchine a stati

3. Consistency checks [12][13]Assunzione: gli scenari iniziali riflettono il flusso di esecuzione desiderato (non desiderato)Check tra modelli architetturali per evitare errori di specifica statici:identificatori degli stati univoci negli state diagram;

ogni state diagram deve avere un solo stato iniziale;

per ogni send (receive) in una componente, deve esistere un receive (send) in unaltra;

sequence diagrams pu contenere solo messaggi gi inseriti nello state;

sender e receiver di un msg devono essere gli stessi (componenti) nel sequence e nello state;

messaggi con lo stesso nome devono avere lo steso numero di parametri;

3. Approccio di slicing ed abstraction [15] Program Slicing: tecnica definita sui linguaggi di programmazione che cerca di decomporre un sistema, estraendo elementi basici, come variabili o statement, correlati ad una particolare computazione Slicing architetturale: sottinsieme del comportamento della SA che cerca di isolare le parti coinvolte nel criterio di slicing Architectural abstraction: tecnica per astrarre parti del sistema coinvolte nel criterio di astrazione ma che non sono direttamente legate alla sua formulazione.

4. Confronto

4. Confronto

5. Future works (Charmy)Considerare tempo: timed automata, real-time model checker ed estensione PSC e W_PSCoppure profilo per real-time in UML, real-time model checker ed estensione PSC e W_PSCInserire ulteriori model checker per confronti sullefficienzaApprofondire approccio composizionale per generalizzarloIndagare maggiormente tecniche di slicing ed abstractionEffettuare studio di fattibilit su modellazione ed analisi di Service Oriented Architecture e Dynamic Architecture Sviluppare un CVSMiglioramenti dellusabilitscaricare ed installare plugin automaticamenteuniformare notazione ad UML 2.0plugin per Eclipsemaggiore documentazionecase study di esempio nel tool

5. Future works (Fujaba)Considerare model checking architetturale: plugin per rappresentare architettura + plugin per propriet

Integrare lanalisi di sistemi real-time con quella di sistemi concorrenti

case study industriali

Miglioramenti dellusabilitmaggiore documentazione ed in lingua inglese

case study di esempio nel tool

References[1] Hirsch, M., Giese, H.: Towards the Incremental Model Checking of Complex RealTime UML Models. In: Proc. of the Fujaba Days 2003, Kassel, Germany. (2003)

[2] Fujaba Website: www.fujaba.de

[3] Sven Burmester, Holger Giese, Martin Hirsch, and Daniela Schilling, Incremental Design and Formal Verification with UML/RT in the FUJABA Real-Time Tool Suite, in Proc. of SVERTS2004, pp. 1--20, October 2004.

[4] Sven Burmester, Holger Giese, Martin Hirsch, Daniela Schilling, and Matthias Tichy, 'The Fujaba Real-Time Tool Suite: Model-Driven Development of Safety-Critical, Real-Time Systems', in Proc. of ICSE 2005, pp. 670--671, ACM Press.

[5] H. Giese and S.Tissen. The SceBaSy PlugIn for the Scenario-Based Synthesis of Real-Time Coordination Patterns for Mechatronic UML. In Proc. of the 3rd International Fujaba Days 2005, Paderborn, Germany, pp. 67--70, September 2005.

[6] Holger Giese, Stefan Henkler, Martin Hirsch, and Florian Klein, Nobody's perfect: Interactive Synthesis from Parametrized Real-Time Scenarios, in Proc. of the 5th ICSE 2006 Workshop SCESM'06, pp. 67--74, ACM Press, May 2006.

[7] Charmy Website: http://www.di.univaq.it/charmy/

References[8] P. Pelliccione, P. Inverardi, H. Muccini, Charmy: A framework for Designing and Validating Architectural Specifications. Tech. Report April 2005. Submitted for publication.

[9] M. Autili, P. Inverardi, and P. Pelliccione, A Scenario Based Notation for Specifying Temporal Properties. SCESM'06.

[10] PSC Project WebSite: http:// www.di.univaq.it/psc2ba

[11] M. Caporuscio, P. Inverardi, P. Pelliccione, "Compositional Verificationof Middleware-Based Software Architecture descriptions". In ICSE 2004.

[12] P. Inverardi, H. Muccini, P. Pelliccione, "Checking consistency betweenarchitectural models using Spin". In Proc. of STRAW2001.

[13] P. Inverardi, H. Muccini, P. Pelliccione, "Automated Check ofArchitectural Models Consistency using Spin". In ASE 2001.

[14] M. Autili, and P. Pelliccione, Towards a Graphical Tool for Refining User to System Requirements. GT-VMT06. To appear in ENTCS.

[15] Daniela Colangelo, Daniele Compare, Paola Inverardi, and Patrizio Pelliccione Reducing Software Architecture Models Complexity: a Slicing and Abstraction Approach.FORTE 2006.