Comment rendre LOTOS apte à spécifier des systèmes temps réel ?

Nous expliquons et justifions par des exemples notre proposition d'extension temporelle de LOTOS. Les exemples couvrent des fonctions de protocole et des facilités de service que l'on rencontre fréquemment en pratique ou qui en sont inspirés, tels que les temporisations, les chiens de garde, les délais, l'isochronisme, le multimédia, le contrôle de débit, ... La sémantique du langage est présentée ensuite et ses propriétés discutées de manière plus formelle. Nous pensons que l'application systématique des techniques formelles temporelles à ce type d'exemples est le passage obligé pour convaincre du bienfondé des choix de conception. L'efficacité pratique d'un formalisme est tout aussi importante que ses propriétés mathématiques associées.