Timed automata is een uitbreiding op de automata-theoretische benadering van de modellering van real time systemen die tijd in de klassieke automata introduceert. Sinds het voor het eerst werd voorgesteld in het begin van de jaren negentig, is het een belangrijk onderzoeksgebied geworden en is het op grote schaal bestudeerd in zowel de context van formele talen als van het modelleren en verifiëren van realtime systemen. Getimede automaten maken gebruik van dichte tijdmodellering, wat een efficiënte modelcontrole mogelijk maakt van tijdgevoelige systemen waarvan de correcte werking afhankelijk is van de eigenschappen van de timing. Een van deze toepassingsgebieden is de verificatie van beveiligingsprotocollen. Dit boek richt zich op het getimede automata-model en gebruikt het als verificatie-instrument voor beveiligingsprotocollen. Als casestudy wordt het Neuman-Stubblebine Repeated Authentication Protocol gemodelleerd en geverifieerd aan de hand van de tijdgevoelige eigenschappen in het model. De gebreken van het protocol worden geanalyseerd en er wordt commentaar gegeven op de voordelen en uitdagingen van het model.
Hinweis: Dieser Artikel kann nur an eine deutsche Lieferadresse ausgeliefert werden.
Hinweis: Dieser Artikel kann nur an eine deutsche Lieferadresse ausgeliefert werden.