Abstract interpretation-based Verification of Non-functional Requirements
Abstract:
The paper investigates a formal approach to the verification of
non functional software requirements, e.g. 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.
Back to the Homepage