This document contains some pointers to information on Formal Methods, useful for mathematically describing and reasoning about computer-based systems, available around the world on the World Wide Web (WWW). Formal methods are a fault avoidance technique that help in the reduction of errors introduced into a system, particularly at the earlier stages of design. They complement fault removal techniques like testing.
A. Bertolino, A. Fantechi, S. Gnesi, and G. Lami. Software Product Lines - Research Issues in Engineering and Management, chapter 11, Springer-Verlag, (2006)
S. Mishra. CS&P 2006 - Concurrency, Specification and Programming, (2006)MR: Es wird gezeigt, dass bei SPLs, die mit formalen Spezifikationen (hier CSP-CASL) beschrieben sind, die Testfälle, Testeingaben und erwartete Ergebnisse automatisch generiert werden können.
Die Wiederverwendung der Tests beschränkt sich im Paper auf SPLs von speziellen Art, bei denen die Varianten nur erweitert werden können und somit andere Varianten und den gemeinsamen Teil vollständig involvieren..
A. van Lamsweerde. ICSE '00: Proceedings of the Conference on The Future of Software Engineering, page 147--159. New York, NY, USA, ACM, (2000)MR: Wertvoll wegen dem Überblick über formale Spezifikations- und somit Modell-Paradigmen..
D. Peters, and D. Parnas. IEEE Transactions on Software Engineering, 24 (3):
161--173(1998)ST: Spezifikation einer SW-Einheit (im Paper Methoden) wird formal beschrieben. Tool leitet automatisch Orakel ab.
Grenzen werden bei dynamische Datenstrukturen erreicht da sie schwer beschreibbar sind.
Die formale Spezifikation erscheint in den Beispielen sehr aufwendig..