A dynamic assertion-based verification platform for validation of UML designs

Banerjee, A. ; Ray, S. ; Dasgupta, P. ; Chakrabarti, P. P. ; Ramesh, S. ; Vignesh, P. ; Ganesan, V. (2012) A dynamic assertion-based verification platform for validation of UML designs ACM SIGSOFT Software Engineering Notes, 37 (1). pp. 1-14. ISSN 0163-5948

Full text not available from this repository.

Related URL: http://dx.doi.org/10.1145/2088883.2088891


Capacity limitations continue to impede widespread adoption of formal property verification in the design validation ow of software and hardware systems. The more popular choice (at least in the hardware domain) has been dynamic property verification (DPV), which is a semi-formal approach where the formal properties are checked over simulation runs. DPV is highly scalable and can support a rich specification language. The main contribution of this paper is to build an integrated DPV platform for validation of UML-based designs. Specifically, we present (a) a language, named Action-LTL (a simple extension of Linear Temporal Logic) for writing assertions over data attributes and events of UML models, and (b) an integrated dynamic assertion-verification platform for verification of UML designs. In view of the capacity limitations of existing formal property verification tools, we believe that the methods presented in this paper are of immediate practical value to the UML design community.

Item Type:Article
Source:Copyright of this article belongs to Association for Computing Machinery.
ID Code:101025
Deposited On:09 Mar 2018 10:20
Last Modified:09 Mar 2018 10:20

Repository Staff Only: item control page