Formal Methods
Formal methods are mathematical approaches to solving software (and hardware) problems at the requirements, specification, and design levels. Formal methods are most likely to be applied to safety-critical or security-critical software and systems, such as avionics software. Software safety assurance standards, such as DO-178B, DO-178C, and Common Criteria demand formal methods at the highest levels of categorization.
For sequential software, examples of formal methods include the B-Method, the specification languages used in automated theorem proving, RAISE, VDM, and the Z notation.
Formalization of software development is creeping in, in other places, with the application of Object Constraint Language (and specializations such as Java Modeling Language) and especially with model-driven architecture allowing execution of designs, if not specifications.
For concurrent software and systems, Petri nets, process algebra, and finite state machines (which are based on automata theory - see also virtual finite state machine or event driven finite state machine) allow executable software specification and can be used to build up and validate application behavior.
Another emerging trend in software development is to write a specification in some form of logic (usually a variation of first-order logic (FOL), and then to directly execute the logic as though it were a program. The OWL language, based on Description Logic (DL), is an example. There is also work on mapping some version of English (or another natural language) automatically to and from logic, and executing the logic directly. Examples are Attempto Controlled English, and Internet Business Logic, which do not seek to control the vocabulary or syntax. A feature of systems that support bidirectional English-logic mapping and direct execution of the logic is that they can be made to explain their results, in English, at the business or scientific level.
Read more about this topic: Software Development Process
Famous quotes containing the words formal and/or methods:
“True variety is in that plenitude of real and unexpected elements, in the branch charged with blue flowers thrusting itself, against all expectations, from the springtime hedge which seems already too full, while the purely formal imitation of variety ... is but void and uniformity, that is, that which is most opposed to variety....”
—Marcel Proust (1871–1922)
“We are lonesome animals. We spend all our life trying to be less lonesome. One of our ancient methods is to tell a story begging the listener to say—and to feel—”Yes, that’s the way it is, or at least that’s the way I feel it. You’re not as alone as you thought.””
—John Steinbeck (1902–1968)