Automatyka czasowa jest rozszerzeniem automatyki - teoretycznego podejścia do modelowania systemw czasu rzeczywistego, ktre wprowadza czas do klasycznej automatyki. Od czasu, gdy zostala po raz pierwszy zaproponowana na początku lat dziewięcdziesiątych, stala się ważnym obszarem badań i byla szeroko badana zarwno w kontekście językw formalnych, jak i modelowania i weryfikacji systemw czasu rzeczywistego. Automaty czasu rzeczywistego wykorzystują gęste modelowanie czasowe, pozwalające na sprawne sprawdzanie modeli systemw wrażliwych na czas, ktrych prawidlowe funkcjonowanie zależy od wlaściwości czasowych. Jednym z tych obszarw zastosowań jest weryfikacja protokolw bezpieczeństwa. Książka ta koncentruje się na modelu automatyki czasowej i wykorzystuje go jako narzędzie weryfikacyjne dla protokolw bezpieczeństwa. Jako studium przypadku, Neuman-Stubblebine Repeated Authentication Protocol jest modelowany i weryfikowany z wykorzystaniem wrażliwych czasowo wlaściwości modelu. Wady protokolu są analizowane i komentowane na temat korzyści i wyzwań związanych z modelem.