G. Fraser, F. Wotawa and P. E. Ammann, “Testing with Model Checkers: A Survey,” Journal Software Testing, Verification & Reliability, Vol. 19, No. 3, 2009, pp. 215-261.

has been cited by the following article:

• TITLE: Automatic Generation of Test Cases in Regression Testing for Lustre/SCADE Programs

  AUTHORS: Trinh Cong Duy, Nguyen Thanh Binh, Ioannis Parissis

  KEYWORDS: Regession Testing; Test Case; Lustre; SCADE; Model Checking

  JOURNAL NAME: Journal of Software Engineering and Applications, Vol.6 No.10A, October 4, 2013

  ABSTRACT: Lustre is a formal synchronous declarative language widely used for modeling and specifying safety critical applications in the fields of avionics, transportation, and energy production. In such applications, the testing activity to ensure correctness of the system plays a crucial role. During the development process, Lustre programs (or SCADE) are often upgraded, so regression test should be performed to detect bugs. However, regression test is generally costly, because the number of test cases is usually very large. In this paper, we present the solution to automatically generating test cases in regression testing of Lustre/SCADE programs. We apply this solution to regression testing for case study Uturn System.