Duration Calculus: A Real-Time Semantic for B

Among the possible approaches for expressing real-time problems with the B method, two are dominant : the use of the usual B mechanisms to define temporal constraints on the one hand, and extending B through another formalism more adapted to the real-time context on the other hand. We define here a possible temporal semantic for B, by using a temporal logic (the duration calculus), and we te how this extension affects the proof mechanism used to show the soundness of abstract machines.

• Type: Conference
• Year: 2004
• Where: ICTAC
• Authors: Samuel Colin, Georges Mariano, Vincent Poirriez
• Keywords: ICTAC 2004, Possible Approaches, Real-time Problems, Temporal Constraints