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.
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
[Bearbeiten | Quelltext bearbeiten]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.
Siehe auch
[Bearbeiten | Quelltext bearbeiten]- Formale Semantik
- Formale Spezifikation
- Formale Verifikation
- Theorembeweisen
- Modellprüfverfahren (model checking)
Weblinks
[Bearbeiten | Quelltext bearbeiten]- Peter Padawitz: Formale Methoden des Systementwurfs. Dortmund 2010 (tu-dortmund.de [PDF] Vorlesungsskript).
- Christel Baier, Joost-Pieter Katoen: Principles of model checking. MIT press, 2008.
Einzelnachweise
[Bearbeiten | Quelltext bearbeiten]- ↑ Jean Souyris: Industrial Experience of Abstract Interpretation-Based Static Analyzers. In: Building the Information Society (= IFIP International Federation for Information Processing). Springer US, Boston, MA 2004, ISBN 978-1-4020-8157-6, S. 393–400, doi:10.1007/978-1-4020-8157-6_31 (springer.com [abgerufen am 20. April 2020]).
- ↑ SLAM. In: Microsoft Research. Abgerufen am 20. April 2020 (amerikanisches Englisch).
- ↑ Byron Cook: Formal Reasoning About the Security of Amazon Web Services. In: Computer Aided Verification (= Lecture Notes in Computer Science). Springer International Publishing, Cham 2018, ISBN 978-3-319-96145-3, S. 38–47, doi:10.1007/978-3-319-96145-3_3 (springer.com [abgerufen am 20. April 2020]).
- ↑ Edward Aftandilian, Raluca Sauciuc, Siddharth Priya, Sundaresan Krishnan: Building Useful Program Analysis Tools Using an Extensible Java Compiler. 2012, abgerufen am 20. April 2020 (englisch).
- ↑ Formal Methods in Industry. In: floc2018.org. Abgerufen am 20. April 2020 (amerikanisches Englisch).