Abstract
The first lecture on April 2, 2013 was twofold. The first hour deepened the general notions presented in the opening lecture, with more technical examples. The second hour dealt with the study of Combinatorics circuits, emphasizing their temporal aspects, which illustrate well the different visions of time.
Formalizing time
Building a computer system means predicting what can happen over time, restricting it to the desired behaviors, specifying these behaviors precisely and, if possible, formally, programming so that everything happens as specified, and checking that all these actions are consistent. The technical objectives are of two kinds, equally difficult: on the one hand, to specify, program and verify a priori the realization of a temporal and event-driven system, and, on the other, to analyze its execution to understand its dynamic behaviors and be able to find its bugs.
To show that things don't always work as planned, I've presented a collection of time-related bugs in consumer and professional embedded systems. They range from silly problems, such as the failure to check a seemingly non-critical time function but rendering the object unusable (MP3 players and video games, for example, due to leap years), to more subtle ones (cumulative rounding errors in time measurement causing a Patriot anti-missile to fail to intercept a Scud missile during the Kuwait war, resulting in many deaths).
I then analyzed in greater depth the questions posed in the opening lecture, with a leitmotiv : talk about time, but in a formal way. Using examples, I explained why conventional methods are inadequate.
