Synthesising Certificates in Networks of Timed Automata
Bernd Finkbeiner, Hans-Jörg Peter, and Sven Schewe
The authors present an automatic method for the synthesis of certificates for components in embedded real-time systems. A certificate is a small homomorphic abstraction that can transparently replace the component during model checking: if the verification with the certificate succeeds, then the component is guaranteed to be correct; if the verification with the certificate fails, then the component itself must be erroneous. The authors give a direct construction, based on a forward and backward reachability analysis of the timed system, and an iterative refinement process, which produces a series of successively smaller certificates. In their experiments, model checking the certificate is several orders of magnitude faster than model checking the original system.
IET-Software, June 2010, Volume 4, Issue 3, Automated compositional verification (IET SEN 2010).