E. Uzuncaova, D. Garcia, S. Khurshid, и D. Batory. ESEC-FSE '07: Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, стр. 525--528. New York, NY, USA, ACM, (2007)ST: Die Spezifikation der Produktlinie liegt in einer formalen Beschreibung vor (LTL)
Es wird ein Modelchecking-Verfahren durchgefuehrt um zu beweisen, dass die Spezifikation gilt.
Fazit: Keine explizite Ableitung von Testdaten, die Spezifikation muss formal vorliegen.
MR: Anhand von formalen Alloy-Spezifikationen von Invarianten und Constraints kann der Alloy Analyzer (SAT solver) automatisch alle passenden Testdaten generieren.
Nachteile: Die erwarteten Ergebnisse werden nicht betrachtet (oder?). Die Spezifikation wird als Annotationen in den Code eingebracht (hier als moderner Ansatz angesehen ähnlich JML). An der Wiederverwendung wird erst gearbeitet..
S. Khurshid, M. Malik, и E. Uzuncaova. Leveraging Applications of Formal Methods, Verification and Validation, 2006. ISoLA 2006. Second International Symposium on, стр. 449--457. (2006)