|
List of Some Formal Techniques cum Methods
- ACL2:
Applicative Common Lisp, a Computational Logic
- Action
Systems:
A
refinement calculus for parallel and reactive systems
- ASM:
Abstract-State Machines
-
B, event-B:
B
France, or
B:
UK - for
Bourbaki
- CafeOBJ:
A rewrite logic and hidden algebra OBJ-like specification and
programming language
- CASL:
Common Algebraic Specification Language
- Coq:
A proof
assistant. Coq, as a project, has been dissolved, 2000. Now see
LOGICAL
- CSP:
Communicating Sequential Processes
- Duration
Calculi:
A continuous time interval
temporal logic
- Esterel:
Synchronous teactive programming
- HOL:
Higher Order Logic
- HyTech:
Hybrid Technology -- an automatic tool for the analysis of embedded systems
- Isabelle:
A generic theorem proving environment
- Interval Temporal
Logic
- Linear Temporal
Logic
- LSCs:
, and
Live Sequence
Charts
- LOGICAL:
Logic and computing
- Maude:
Algebraic semantics based equational and rewriting logic
specification and programming language
- MSCs:
,
and Message Sequence
Charts, or
even
this !
- Model-checking @ CMU
- Nqthm:
The Boyer-Moore prover
- nuprl:
A proof & program refinment logic.
- Petri Nets
- Pi-Calculus:
Calculi for Mobile Processes
- PVS:
Prototype
Verification System
- Refinement
Calculus
- RAISE:
Rigorous Approach to Industrial Software Engineering
- REACT:
The
specification, verification and
synthesis
of
concurrent, reactive, real-time and hybrid systems.
See also
STeP:
Stanford Temporal Prover.
- SpecWare
- SPIN:
On-the-fly Linear Temporal Logic Model Checking
- Statecharts
- TLA /
TLA+
Temporal Logic of Actions
- UNITY:
A programming notation and a logic to reason about parallel and
distributed programs.
- UppAal:
An integrated tool environment for modeling, validation and
verification of real-time systems
- VDM:
Vienna Development Method
- Z
- for Zermelo
|
|
