My past works consist in my PhD thesis, titled (after translation): Contribution to the integration of time into the B formalism: duration calculus as semantics for B, whose summary follows:
In the field of automated systems where reliability is the first requirement, formal methods proved to be efficient for the design of safe software. The dependency towards such systems is increasing, and the constraints to be met by these systems become more and more various and precise, particularly timed constraints. Some formal methods, notably the B method, make designing difficult under these constraints, because this is not what they have been made for in the first place.
We therefore propose to extend the B method so that it can help specifying and validating systems with complex timed constraints. We use calculi of durations in order to express the semantics of the B language and deduce a conservative extension allowing its use in both its original context and in the context of time-constrained systems.
We also study the problem of using a generic proof tool for validating duration calculus formulas. The genericity of this kind of tool helps answering the growing number of formal methods, but introduces the problem of adapting the mathematical foundations of such formal methods to a generic tool. We thus propose to study the implementation of duration calculus as a shallow embedding in the Coq proof assistant. We draw from it more general conclusions about the implementation of a particular modal logic in a generic-oriented tool.
You can find all my publications and related documents in my résumé and my publication list.
You can also download the associated implementation of duration calculus in Coq (for version 8.0, if I remember correctly).