An approach for the verification of the temporal consistency of NCL applications - Yovine, S.; Olivero, A.; Córdoba, L.; Monteverde, D.; Reiter, G. (Anais Estendidos do Simpósio Brasileiro de Sistemas Multimídia e Web (WebMedia), 2010)
NCL is used to write interactive applications for DTV. This paper presents the first steps of our approach towards the formalization of the semantics of NCL. We use Time Petri Nets (TPN) as target formalism for giving mathematically precise meaning to NCL. We rely on Visual Timed Scenarios (VTS) to graphically specify the behavioral properties the NCL application should satisfy. We sketch the method to translate NCL programs into TPN models and to verify VTS properties on the obtained model. We illustrate the approach with “O Primeiro João” from club.ncl.org.br.