Formal Methods - Formal Methods and Notations

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:

    “I will not let him stir
    Till I have used the approvèd means I have,
    With wholesome syrups, drugs, and holy prayers,
    To make of him a formal man again.”
    —William Shakespeare (1564–1616)

    “A woman might claim to retain some of the child’s faculties, although very limited and defused, simply because she has not been encouraged to learn methods of thought and develop a disciplined mind. As long as education remains largely induction ignorance will retain these advantages over learning and it is time that women impudently put them to work.”
    —Germaine Greer (b. 1939)