An approach for the verification of the temporal consistency of NCL applications

  • S. Yovine UBA
  • A. Olivero UNSAM
  • L. Córdoba UNSAM
  • D. Monteverde UBA
  • G. Reiter UNSAM

Resumo


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.
Publicado
05/10/2010
Como Citar

Selecione um Formato
YOVINE, S.; OLIVERO, A.; CÓRDOBA, L.; MONTEVERDE, D.; REITER, G.. An approach for the verification of the temporal consistency of NCL applications. In: WORKSHOP DE TV DIGITAL INTERATIVA - SIMPÓSIO BRASILEIRO DE SISTEMAS MULTIMÍDIA E WEB (WEBMEDIA) , 2010, Belo Horizonte. Anais [...]. Porto Alegre: Sociedade Brasileira de Computação, 2010 . p. 179-184. ISSN 2596-1683.