Computing, IT & AI

Timed automata

1990-1994 CERajeev Alur and David DillA theory of timed automata (Theoretical Computer Science, 1994)Diaspora (work abroad)

1990

A mathematical model for verifying systems whose correctness depends on timing.

Dated: 1990–1994
As scholars put it: 1990-1994 CE
Originator: Rajeev Alur and David Dill
Source text: A theory of timed automata (Theoretical Computer Science, 1994)
Region: Diaspora (work abroad)
Discipline: Computing, IT & AI
Evidence: Documented
Confidence: High
Verification: Verified-web

Background

Rajeev Alur, born in Pune and an IIT Kanpur graduate, introduced timed automata with David Dill: finite automata extended with real-valued clocks whose values can be tested and reset. Checking properties of such models remains decidable.

Significance

The standard formalism for verifying real-time systems, the basis of tools such as UPPAAL. It won the 2016 Church Award.

Path to modern innovation

Used to verify communication protocols, automotive and avionics controllers, and medical devices.

Global impact

Formal verification of safety-critical real-time software.

References

3A theory of timed automata R. Alur and D. L. Dill, 1994