S. Pippig, S. Andexinger, K. Daniel, M. Puzicha, M. Caron, R. Lefkowitz, and M. Lohse. J Biol Chem, 268 (5):
3201-8(February 1993)Pippig, S Andexinger, S Daniel, K Puzicha, M Caron, M G Lefkowitz,
R J Lohse, M J Research Support, Non-U.S. Gov't United states The
Journal of biological chemistry J Biol Chem. 1993 Feb 15;268(5):3201-8..
E. Uzuncaova, D. Garcia, S. Khurshid, and 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, page 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..