Temporal and Spatial Coherence Verification in SMIL Documents with Hoare Logic and Disjunctive Constraints: A Hybrid Formal Method

Abstract

The challenging problem of formal verification of SMIL (Synchronized Multimedia Integration Language Specification) documents is considered in this paper, where we propose a hybrid formal method that automatically detects and corrects the temporal and spatial conflicts. The proposed solution is based on a related work that uses Hoare logic for temporal conflict detection in SMIL documents. The use of Hoare logic is borrowed by that solution but with many improvements and extensions. New rules are added to enable modeling of more SMIL elements. We also deal with spatial conflicts and propose a spatio-temporal inconsistencies verification algorithm, called Spatio-temporal Inconsistencies Verification Algorithm (SIVA), that checks the spatial incoherence of SMIL documents. The disjunctive constraints of Marriott are used to correct the spatial inconsistencies. Furthermore, we propose a new tool that helps the author to validate the temporal and spatial constraints in SMIL documents. If any temporal or spatial conflicts are detected, the system returns a help message to report the error and help the author to correct the conflict. Finally, our contribution has been compared with two recent related works, and the results show that the proposed solution allow to check more attributes.