Formal methods

Formal methods are a particular kind of mathematically-based techniques for the specification, development and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

Overview[edit | edit source]

Formal methods are best described as the application of a fairly broad variety of theoretical computer science fundamentals, in particular logic calculi, formal languages, automata theory, and program semantics, but also type systems and algebraic data types to problems in software and hardware specification and verification.

Specification[edit | edit source]

Formal methods can be used at a number of levels:

Level 0: Formal syntax and semantics for a programming language, but with conventional mathematical semantics. This may include a step called formal specification where an unambiguous and consistent definition of the functions to be provided are developed.

Level 1: Formal specification with a clear semantics for a problem to be solved (or a more abstract design), and a proof that the program satisfies this specification.

Level 2: Full formal development (correctness-preserving transformation), and a proof that the problem specification transforms to the program written in the programming language.

Verification[edit | edit source]

Formal verification techniques can be used to prove the correctness of systems relative to a certain formal specification or property. The type of property to be verified determines the type of formalism to be used. For safety properties (something bad will not happen), model checking, a method of testing the different states of a system, is the most common. For properties of a more global nature, theorem proving is used.

Applications[edit | edit source]

Formal methods can be applied to a wide range of fields including computer science, engineering, and mathematics. They are also used in the development of high-integrity systems such as avionics software, medical software, nuclear control systems, and railway signaling.

Search WikiMD

Ad.Tired of being Overweight? Try W8MD's physician weight loss program.
Semaglutide (Ozempic / Wegovy and Tirzepatide (Mounjaro) available.
Advertise on WikiMD

WikiMD is not a substitute for professional medical advice. See full disclaimer.

Credits:Most images are courtesy of Wikimedia commons, and templates Wikipedia, licensed under CC BY SA or similar.

v t e Computer science
Note: This template roughly follows the 2012 ACM Computing Classification System.
Hardware	Printed circuit board Peripheral Integrated circuit Very Large Scale Integration Systems on Chip (SoCs) Energy consumption (Green computing) Electronic design automation Hardware acceleration
Computer systems organization	Computer architecture Embedded system Real-time computing Dependability
Networks	Network architecture Network protocol Network components Network scheduler Network performance evaluation Network service
Software organization	Interpreter Middleware Virtual machine Operating system Software quality
Software notations and tools	Programming paradigm Programming language Compiler Domain-specific language Modeling language Software framework Integrated development environment Software configuration management Software library Software repository
Software development	Software development process Requirements analysis Software design Software construction Software deployment Software maintenance Programming team Open-source model
Theory of computation	Model of computation Formal language Automata theory Computability theory Computational complexity theory Logic Semantics
Algorithms	Algorithm design Analysis of algorithms Algorithmic efficiency Randomized algorithm Computational geometry
Mathematics of computing	Discrete mathematics Probability Statistics Mathematical software Information theory Mathematical analysis Numerical analysis
Information systems	Database management system Information storage systems Enterprise information system Social information systems Geographic information system Decision support system Process control system Multimedia information system Data mining Digital library Computing platform Digital marketing World Wide Web Information retrieval
Security	Cryptography Formal methods Security services Intrusion detection system Hardware security Network security Information security Application security
Human–computer interaction	Interaction design Social computing Ubiquitous computing Visualization Accessibility
Concurrency	Concurrent computing Parallel computing Distributed computing Multithreading Multiprocessing
Artificial intelligence	Natural language processing Knowledge representation and reasoning Computer vision Automated planning and scheduling Search methodology Control method Philosophy of artificial intelligence Distributed artificial intelligence
Machine learning	Supervised learning Unsupervised learning Reinforcement learning Multi-task learning Cross-validation
Graphics	Animation Rendering Image manipulation Graphics processing unit Mixed reality Virtual reality Image compression Solid modeling
Applied computing	E-commerce Enterprise software Computational mathematics Computational physics Computational chemistry Computational biology Computational social science Computational engineering Computational healthcare Digital art Electronic publishing Cyberwarfare Electronic voting Video games Word processing Operations research Educational technology Document management
Book Category Outline WikiProject Commons