Protocol engineering

[2] While initially mainly finite-state machine were used as (simplified) models of a protocol entity,[3] in the 1980s three formal specification languages were standardized, two by ISO [4] and one by ITU.

Reachability analysis was proposed to understand all possible behaviors of a distributed system, which is essential for protocol verification.

However, finite-state descriptions are not powerful enough to describe constraints between message parameters and the local variables in the entities.

Such constraints can be described by the standardized formal specification languages mentioned above, for which powerful tools have been developed.

These methods and tools have later been used for software engineering as well as hardware design, especially for distributed and real-time systems.