Formale Methode

Der Begriff Formale Methode bezeichnet in der Informatik eine Vielzahl von natur- und ingenieurswissenschaftlichen Techniken zur Modellierung und mathematisch rigorosen Überprüfung von Computersystemen. Die Anwendung von Formalen Methoden zur Analyse von Software und Hardware ist motiviert von der Erwartung, dass wie in anderen ingenieurswissenschaftlichen Disziplinen eine angemesse mathematische Analyse zur Zuverlässigkeit und zur Stabilität eines Systems beitragen kann.

Formale Methoden bauen auf einer sehr breiten Basis von Konzepten aus der Theoretischen Informatik auf, wie z. B. Logik, Formale Sprachen, Automatentheorie, Formale Semantik und Typsysteme.

Relevanz

Formale Methoden erleben in den letzten Jahren einen Aufschwung. Statische Programmanalyse wird zum Beispiel bei Airbus^[1] und Microsoft verwendet. Microsoft selbst unterhält bei Microsoft Research einige Forschungsgruppen, die sich mit formalen Methoden beschäftigen, und z. B. Treiber werden regelmäßig mit formalen Methoden überprüft^[2]. Amazon setzt im Bereich von Web Services auch auf formale Methoden^[3]. Auch Google zeigt daran Interesse^[4]. Es gibt eine Konferenz, die sich nur mit diesem Thema beschäftigt^[5].

Auch unter den Turing-Award-Gewinnern finden sich einige Forscher aus dem Bereich der formalen Methoden, z. B. Tony Hoare für seinen Beitrag zur formalen Spezifikation von Programmiersprachen, Robin Milner für seine allgemeine Theorie der Nebenläufigkeit, Amir Pnueli für seinen Beitrag zur temporalen Logik und Edmund M. Clarke, E. Allen Emerson und Joseph Sifakis für ihren Beitrag zum Model Checking.

Remove ads

Relevanz

Siehe auch

Weblinks

Einzelnachweise

Wikiwand - on