Description des protocoles par automates d'états étendus (automates à prédicats )
Les protocoles de communication sont décrits par des automates d'états finis à prédicats ( automates étendus ). Les services sont souvent modélisés de la même manière. La description formelle de ces automates d'états finis à prédicats peut prendre trois formes de précision croissante qui présentent chacune leur intérêt. La conception voire la compréhension d'un tel automate nécessite d'utiliser ces trois formes. Pour chaque forme il existe plusieurs notations parfois éloignées l'une de l'autre.
