A design-oriented method to build correct hypermedia documents

Over the years, different approaches to identify temporal and spatial conflicts in hypermedia applications has been proposed. Most of them are based on formal verification techniques and impose to the designers to follow a formal model or language to ensure application’s functional correctness. Furthermore, the error diagnose is hard to be interpreted by a non-specialist in this domain. In this paper, we present an approach which supports formal verification for documents written in markup languages. We proposed a method and built a verification toolchain that helps designers to verify time and spatial constraints in hypermedia applications. The input language is the designer language. Its translation towards the input of toolchain is automatic and transparent for the application designer. The errors scenarios provided by the verification tool are presented in a timeline way, easily understandable by the designer. The method and toolchain support different markup languages translated in the same intermediary language in order to facilitate the use of different verification tools in the same environment.