Understanding Time, from Physics to Informatics and Music
College de France
Time is one of the greatest mysteries. Physics is able to measure time with an incredible precision, without being able to understand its real nature. On the opposite, our intuitive view of time is very flaky, as exemplified by the way we talk about it: I waited long minutes, time passes fast, etc. In classical software, time is merely absent from programming concerns, being only viewed as a quantity to optimize for efficiency. In hardware circuits, time used to be associated with regular clocks, which made it easy to understand and deal with. These happy times are over: circuit clocks vary continuously to save energy, and machine instruction timing has become largely unpredictable due to caching, pipelining, speculation, etc. But more and more applications require a much better understanding of temporal issues: real-time programs found in many embedded applications of course, but also time-aware data bases, continuous / discrete simulation of physical phenomena, worldwide clock synchronization, real-time computer music, etc.
The talk will address time in Informatics by stressing and exemplifying several points
concerning the specification, implementation, and verification of time-aware applications.
First, synchronous languages such as Esterel, Lustre, Signal, and their followers have shown that we should not restrict time to milliseconds, but instead deal equally with logical clocks generated by the repetition of any arbitrary event using a synchronous model of concurrency. We will explain why the SCADE 6 synchronous language and system of Esterel Technologies has become a standard for high-security temporal applications. Second, temporal logics and hybrid systems make it possible to perform analysis and proofs of complex temporal applications impossible to analyze by hand; we will illustrate this with the UPPAAL verification system. Third, we shall see that modelers such as Simulink and Modelica exhibit incorrect behaviors when mixing continuous and discrete time; this problem has been elegantly solved in the new Zelus language. Finally, we will discuss time in music, which is by no way simple. For instance, a score is written with a straight logical time for notes, while interpretation expressivity requires constantly varying the tempo and articulation in physical time. Using as examples the Antescofo score follower and musical synchronous language and the Omax/Improtex co-improviser, we discuss fascinating questions and solutions related with relating logical and physical time during musical performance.
Former student of the Ecole polytechnique, Member of Académie des sciences, Académie
des technologies and Academia Europaea, CNRS Gold medal 2014, Gérard Berry was a
researcher at the Ecole des mines of Paris and INRIA from 1973 to 2000. He became Chief
Scientist of the company Esterel Technologies from 2001 to 2009, then Research Director at INRIA and President of the Evaluation Committee of this Institute from 2009 to 2012. He holds the Chair Algorithms, Machines and Languages at the Collège de France since 2012, after having held two annual chairs there in 2007-2008 and 2009-2010. His scientific contribution concerns four main topics: the formal treatment of programming languages and their relations with mathematical logic, reactive and real-time programming for embedded systems, integrated circuit computer-aided design, and formal verification of programs and circuits. He is the creator of the Esterel synchronous programming language.