Formal Methods and Notations
There are a variety of formal methods and notations available.
- Specification languages
- Abstract State Machines (ASMs)
- ANSI/ISO C Specification Language (ACSL)
- Alloy
- B-Method
- CADP
- Common Algebraic Specification Language (CASL)
- Process calculi
- CSP
- LOTOS
- π-calculus
- Actor model
- Esterel
- Lustre
- mCRL2
- Perfect Developer
- Petri nets
- RAISE
- SPARK Ada
- Specification and Description Language
- Temporal logic of actions (TLA)
- USL
- VDM
- VDM-SL
- VDM++
- Z notation
- Rebeca Modeling Language
- Model checkers
- SPIN
- PAT is a powerful free model checker, simulator and refinement checker for concurrent systems and CSP extensions (e.g. shared variables, arrays, fairness).
- MALPAS Software Static Analysis Toolset is an industrial strength model checker used for Formal Proof of safety critical systems
Read more about this topic: Formal Methods
Famous quotes containing the words formal and/or methods:
“The conviction that the best way to prepare children for a harsh, rapidly changing world is to introduce formal instruction at an early age is wrong. There is simply no evidence to support it, and considerable evidence against it. Starting children early academically has not worked in the past and is not working now.”
—David Elkind (20th century)
“The philosopher is in advance of his age even in the outward form of his life. He is not fed, sheltered, clothed, warmed, like his contemporaries. How can a man be a philosopher and not maintain his vital heat by better methods than other men?”
—Henry David Thoreau (1817–1862)