Model-checking is a powerful automated technique for verifying finite state real-time safety critical systems, but suffers from a combinatorial explosion of states as system complexity increases. In this paper, we introduce a method for compositional reasoning in real-time temporal logic that is suitable for model-checking finite state real-time reactive modules with data variables. This allows for the formal development of systems by top-down hierarchical program derivation. A system can be decomposed into modules, and the modules checked separately instead of checking the complete system all at once. This procedure often results in a significant decrease in the size of the reachability graphs that must be checked, particularly if the modules are loosely coupled. The modular model-checking method developed in this paper is illustrated using a real time resource allocation problem and the StateTime toolset. StateTime is a prototype toolset that uses visual specifications and temporal logic for the design and verification of real-time systems. The StateTime toolset has been used on small but non-trivial industrial examples. The incorporation of the modular methods discussed in this paper will allow StateTime to evolve from a prototype into an industrial strength tool. This paper presents an application of optic flow estimation to image metamorphosis. It uses a state of the art optical flow algorithm to do image metamorphosis, which is used in video production. The method presented automates the labor intensive process of image animation. It an advanced optic flow algorithm but the rest of it is simple: most of the code fits in the limited space of this summary.

Download paper in PDF format.

The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.