Logo image
Back
Faster analysis of formal specifications
Book chapter   Peer reviewed

Faster analysis of formal specifications

Fabrice Bouquet, Bruno Legeard, Mark Utting and Nicolas Vacelet
Formal Methods and Software Engineering, pp.239-258
International Conference on Formal Engineering Methods (FEM), 6th (Seattle, United States, 08-Nov-2004–12-Nov-2004)
Lecture Notes in Computer Science (LNCS), 3308, Springer New York LLC
2004
DOI: https://doi.org/10.1007/978-3-540-30482-1_24
url
https://doi.org/10.1007/978-3-540-30482-1_24View
Published Version

Abstract

formal specifications analysis speed
When animating a formal model for validation or test generation purposes, scalability is a key issue. This paper describes a graph-based representation for the operations of state-based formal models. This representation makes it possible to handle large models efficiently and perform a variety of transformations, such as splitting an operation into separate behaviours, implementing various test coverage criteria for complex conditionals, removing inconsistent paths, factoring out common calculations, and executing the final operation using a customized constraint logic programming solver. The result is a fully automatic execution engine for state-based formal models such as B [Abr96], Z [Spi92] and UML with OCL preconditions and postconditions. It can be used for animation, test generation and other verification or validation purposes. Our experimental results on large industrial applications show that the transformations result in significant speedups. © Springer-Verlag Berlin Heidelberg 2004.

Details

Metrics

2 File views/ downloads
971 Record Views
Logo image