A rewriting logic semantics for NCL

The Nested Context Language (NCL) is a multimedia authoring language that is part of the standard for digital television in Brazil and in Latin America and the ITU standard for IPTV services. To properly support authors in the development of NCL applications, it is important to provide tools with validation capabilities. The validation of multimedia documents indicates to the author possible inconsistent points in a given document. Thus the author has the possibility of correcting those inconsistencies before making the multimedia document available for the final user. The validation approach presented in this work considers a set of desirable document properties based on related work published in the literature. Since NCL applications may be understood as finite transition systems, standard model-based validation techniques directly apply. This paper discusses a formalization of NCL semantics with rewriting theory. Two theories are given to represent (i) NCL's static semantics and (ii) NCL's dynamic semantics. In the former, NCL structural properties are validated through equational reduction, while in the latter, NCL expected behaviors are validated through searching.