J. Rubin, M. Chechik, и S. Easterbrook. MiSE '08: Proceedings of the 2008 international workshop on Models in software engineering, стр. 7--14. New York, NY, USA, ACM, (2008)
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..
F. Mostefaoui, и J. Vachon. AOM '07: Proceedings of the 10th international workshop on Aspect-oriented modeling, стр. 41--48. New York, NY, USA, ACM Press, (2007)