news
|
 |
|
|
|
 |
Test, Verifica, Validazione »
Geensys »
SCB
|
Ridurre i tempi di test e migliorare la qualità dei modelli Simulink®/Stateflow®
TNI-Valisosys offre, attraverso SCB (Safety Checker Blockset), un metodo semplice ed efficace per la verifica formale di modelli Simulink®/Stateflow®.
La verifica formale e’ complementare alla simulazione tradizionale
Il metodo piu’ tradizionale per il test di modelli e’ la simulazione. Questa tecnica e’ essenziale per la verifica funzionale del sistema, ma la simulazione non puo’ mai provare l’assenza assoluta di errori, visto il numero limitato (anche se grande) di test case che possono essere eseguiti.
Quando viene usata solo la simulazione, ci possono essere condizioni, molti difficili da raggiungere, a cui corrisponde un funzionamento errato del modello.
In altre parola, la sola simulazione puo’ dimostare la presenza di errori, ma non puo’ escluderne la mancanza assoluta.
In generale, preparare ed eseguire un elevato numero di test case su un modello puo’ comportare costi e tempi significativi di verifica senza poter arrivare ad una confidenza completa in quanto sviluppato.
La verifica formale, a complemento delle normali tecniche di simulazione, consente di avere la certezza che determinate combinazioni di condizioni e stati del modello, non generino comportamenti diversi da quelli attesi. In questo caso SCB puo’ fornire automaticamnete il controesempio, cioe’ l’insieme di condizioni da impostare per osservarne l’errato comportamento.
Facilita’ di verifica
Il Safety-Checker Blockset di TNI-Valiosys consente agli sviluppatori di modelli Simulink, la verifica formale delle proprieta’ con un semplice drag & drop.
Una proprieta’ e’ una combinazione di variabili appartenenti al modello connesse ad un operatore di verifica. Esempio: l’operatore “NeverTogether” puo’ verificare che due segnali booleani non siano mai nello stesso stato.
Una proprieta’ tipicamente identifica una condizione non voluta. SCB verifica in altre parole se questa condizione e’ raggiungibile oppure no dal modello. Se e’ raggiungibile, SCB genera un controesempio che puo’ essere immediatamente eseguito da Stateflow per controllare fove il modello fallisce.
Se non viene trovato un controesempio allora la proprieta’ e’ provata come vera ed e’ formalmente dimostrato che non sara’ mai raggiunta durante l’esecuzione del modello.
Non e’ mai stato cosi’ facile verificare la correttezza di un modello Simulink/Stateflow !
Set di operatori di verifica per Simulink
Qui sotto il set di operatori di verifica disponibili per Simulink: poiche’ appaiono nel browser Simulink e’ sufficente fare darg & drop di uno di questi blockset nel proprio modello per verificare formalmente la presenza o meno delle proprieta’ specificate.
Esempi di proprieta’
| “La ECU 2 deve sempre essere in uno dei modi 1, 3, 4, 6 quando ECU 1 e’ in modo 0” |
| “Quando il sistema e’ acceso deve andare nello stato Ready entro 350ms” |
| “Ad eccezione del power-up ECU1 e ECU2 non devono mai essere in Reset mode allo stesso tempo” |
| “ACC non deve mai essere attivo mentre il guidatore sta frenando” |
Un controesempio trovato dal Safety-Checker Blockset puo’ essere rieseguito in StateFlow per controllare dove il modello fallisce:
Facilita’ di uso
L’interfaccia utente di Reqtify, disponibile su Windows, UNIX e Linux, e’ estremamente intuitiva e potente. La disponibilta’ di filtri e viste consente di visulazzare solo la parte dei docuementi di interesse oppure di avere una panoramica delle relazioni che coprono l’intero progetto.
Benefici nell’uso di SCB
| Riduzione significativa dei tempi di test tramite l’approccio formale
|
| Miglioramento della qualita’ del modello tramite l’aumento di copertura dei test
|
| Completa intergazione con Simulink/Stateflow
|
| Complementare alla simulazione tradizionale
|
| Report generator per test e controesempi in formato Word
|
|
|
|
