This chapter investigates a formal approach to the verification of non-functional software requirements that are crucial in Service oriented Systems, like portability, time and space efficiency, and dependability/robustness. The key-idea is the notion of observable, i.e., an abstraction of the concrete semantics when focusing on a behavioral property of interest. By applying an abstract interpretation-based static analysis of the source program, and by a suitable choice of abstract domains, it is possible to design formal and effective tools for non-functional requirements validation.
Verification of Non-functional Requirements by Abstract Interpretation
CORTESI, Agostino;
2012-01-01
Abstract
This chapter investigates a formal approach to the verification of non-functional software requirements that are crucial in Service oriented Systems, like portability, time and space efficiency, and dependability/robustness. The key-idea is the notion of observable, i.e., an abstraction of the concrete semantics when focusing on a behavioral property of interest. By applying an abstract interpretation-based static analysis of the source program, and by a suitable choice of abstract domains, it is possible to design formal and effective tools for non-functional requirements validation.File in questo prodotto:
File | Dimensione | Formato | |
---|---|---|---|
handbook_2012.pdf
non disponibili
Tipologia:
Documento in Post-print
Licenza:
Accesso chiuso-personale
Dimensione
1.65 MB
Formato
Adobe PDF
|
1.65 MB | Adobe PDF | Visualizza/Apri |
I documenti in ARCA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.