Agostino Cortesi and Francesco Logozzo
This chapter investigates a formal approach to the verification of non functional sotware requirements that are crucial in Service-oriented Systems, like portability, time and space efficiency, 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.
The author(s) hereby warrants that the above‐named manuscript that has been submitted to IGI Global for publication in the encyclopedia named or any other IGI Global publication, IS ORIGINAL AND HAS NOT BEEN SUBMITTED FOR PUBLICATION OR PUBLISHED ELSEWHERE and that all trademark use within the manuscript has been credited to its owner or written permission to use the name has been granted. In addition, the author(s) acknowledges that all images such as tables, screenshots, graphics, etc., do not have a copyright that is held by a third party. IGI Global will not accept a manuscript for which the copyright is held by a third party.