Issue No. 01 - January/February (2012 vol. 38)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2010.98
Diego Garbervetsky , FCEyN, Universidad de Buenos Aires, Buenos Aires
Guido de Caso , FCEyN, Universidad de Buenos Aires, Buenos Aires
Sebastián Uchitel , FCEyN, Universidad de Buenos Aires, Buenos Aires and Imperial College, London
Víctor Braberman , FCEyN, Universidad de Buenos Aires, Buenos Aires
Pre/postcondition-based specifications are commonplace in a variety of software engineering activities that range from requirements through to design and implementation. The fragmented nature of these specifications can hinder validation as it is difficult to understand if the specifications for the various operations fit together well. In this paper, we propose a novel technique for automatically constructing abstractions in the form of behavior models from pre/postcondition-based specifications. Abstraction techniques have been used successfully for addressing the complexity of formal artifacts in software engineering; however, the focus has been, up to now, on abstractions for verification. Our aim is abstraction for validation and hence, different and novel trade-offs between precision and tractability are required. More specifically, in this paper, we define and study enabledness-preserving abstractions, that is, models in which concrete states are grouped according to the set of operations that they enable. The abstraction results in a finite model that is intuitive to validate and which facilitates tracing back to the specification for debugging. The paper also reports on the application of the approach to two industrial strength protocol specifications in which concerns were identified.
Requirements/specifications, validation, automated abstraction.
Diego Garbervetsky, Guido de Caso, Sebastián Uchitel, Víctor Braberman, "Automated Abstractions for Contract Validation", IEEE Transactions on Software Engineering, vol. 38, no. , pp. 141-162, January/February 2012, doi:10.1109/TSE.2010.98