Predicate Logic Framework for Verification of Timed Distributed Systems
A.Slissenko University Paris 12
The talk is a survey of a recent work, done mainly with D.Beauquier, on developing a verification framework for distributed systems with timed constraints that may involve non-trivial arithmetic (e. g. clock synchronization). The time we treat is continuous (the framework works also for discrete time but with much less efficiency). The main theoretical results concern the semantics of timed algorithms and decidable classes of verification. The decidable algorithms give a description of counter-models of a bounded complexity. Thus, they are of interest independently of our decidables classes, for example as a tool of search for attacks on security of bounded complexity. What is surprising is that a rather straighforward implementation of one of the algorithms shows that it really works for known benchmark problems and simple protocols.