esec99 Gargantini, Angelo Heitmeyer, Constance

Using Model Checking to Generate Tests from Requirements Specifications

in Software Engineering - ESEC/FSE'99, 7th European Software Engineering Conference, Held Jointly with the 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering, Toulouse, France, September 1999 (Eds. Nierstrasz, Oscar and Lemoine, Michel) Springer Berlin Heidelberg, Lecture Notes in Computer Science, vol. 1687 (1999): 146-162 ISBN 978-3-540-66538-0

Abstract
Recently many formal methods, such as the SCR (Software Cost Reduction) requirements method, have been proposed for improving the quality of software specifications. Although improved specifications are valuable, the ultimate objective of software development is to produce software that satisfies its requirements. To evaluate the correctness of a software implementation, one can apply black-box testing to determine whether the implementation, given a sequence of system inputs, produces the correct system outputs. This paper describes a specification-based method for constructing a suite of "test sequences",


[read the copyright and download the pdf file] [DOI] [url]

My sw links