imported>Invisigoth67: typo

2024-04-28T09:24:56Z

typo

Neue Seite

{{Belege fehlen}}
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 [[Theoretische Informatik|Theoretischen Informatik]] auf, wie z. B. [[Logik]], [[Formale Sprache]]n, [[Automatentheorie]], [[Formale Semantik]] und [[Typsystem]]e.

== Relevanz ==
Formale Methoden erleben in den letzten Jahren einen Aufschwung. [[Statische Code-Analyse|Statische Programmanalyse]] wird zum Beispiel bei [[Airbus]]<ref>{{Literatur |Autor=Jean Souyris |Titel=Industrial Experience of Abstract Interpretation-Based Static Analyzers |Sammelwerk=Building the Information Society |Verlag=Springer US |Ort=Boston, MA |Datum=2004 |Reihe=IFIP International Federation for Information Processing |ISBN=978-1-4020-8157-6 |DOI=10.1007/978-1-4020-8157-6_31 |Seiten=393–400 |Online=https://link.springer.com/chapter/10.1007%2F978-1-4020-8157-6_31 |Abruf=2020-04-20}}</ref> und [[Microsoft]] verwendet. Microsoft selbst unterhält bei [[Microsoft Research]] einige Forschungsgruppen, die sich mit formalen Methoden beschäftigen, und z. B. [[Gerätetreiber|Treiber]] werden regelmäßig mit formalen Methoden überprüft<ref>{{Internetquelle |url=https://www.microsoft.com/en-us/research/project/slam/ |titel=SLAM |werk=Microsoft Research |abruf=2020-04-20 |sprache=en-US}}</ref>. [[Amazon]] setzt im Bereich von Web Services auch auf formale Methoden<ref>{{Literatur |Autor=Byron Cook |Titel=Formal Reasoning About the Security of Amazon Web Services |Sammelwerk=Computer Aided Verification |Verlag=Springer International Publishing |Ort=Cham |Datum=2018 |Reihe=Lecture Notes in Computer Science |ISBN=978-3-319-96145-3 |DOI=10.1007/978-3-319-96145-3_3 |Seiten=38–47 |Online=https://link.springer.com/chapter/10.1007%2F978-3-319-96145-3_3 |Abruf=2020-04-20}}</ref>. Auch [[Alphabet Inc.|Google]] zeigt daran Interesse<ref>{{Internetquelle |autor=Edward Aftandilian, Raluca Sauciuc, Siddharth Priya, Sundaresan Krishnan |url=https://research.google/pubs/pub38275/ |titel=Building Useful Program Analysis Tools Using an Extensible Java Compiler |datum=2012 |abruf=2020-04-20 |sprache=en}}</ref>. Es gibt eine Konferenz, die sich nur mit diesem Thema beschäftigt<ref>{{Internetquelle |url=https://www.floc2018.org/formal-methods-in-industry/ |titel=Formal Methods in Industry |werk=floc2018.org |abruf=2020-04-20 |sprache=en-US}}</ref>.

Auch unter den [[Turing-Award|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 (Entwurfsmuster)|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 ==
* [[Formale Semantik]]
* Formale [[Spezifikation]]
* Formale [[Verifikation]]
* [[Theorembeweisen]]
* [[Modellprüfung|Modellprüfverfahren]] (''model checking'')

== Weblinks ==
* {{Literatur
| Autor=Peter Padawitz
| Titel=Formale Methoden des Systementwurfs
| Ort=Dortmund
| Jahr=2010
| Online=https://fldit-www.cs.tu-dortmund.de/~peter/TdP96.pdf
| Kommentar=Vorlesungsskript
}}
* [[Christel Baier]], [[Joost-Pieter Katoen]]: ''Principles of model checking''. MIT press, 2008.

== Einzelnachweise ==
<references />

[[Kategorie:Theoretische Informatik]]

Formale Methode - Versionsgeschichte

imported>Invisigoth67: typo