Model-checking temporal properties of real-time HTL programs

This paper describes a tool-supported method for the formal verification of timed properties of HTL programs, supported by the automated translation tool HTL2XTA, which extracts from a HTL program (i) an Uppaal model and (ii) a set of properties that state the compliance of the model with certain au...

ver descrição completa

Detalhes bibliográficos
Autor principal: Carvalho, André Ribeiro de (author)
Outros Autores: Carvalho, Joel (author), Pinto, Jorge Sousa (author), Sousa, Simão Melo de (author)
Formato: conferencePaper
Idioma:eng
Publicado em: 2010
Assuntos:
Model checking
Hierarchical timing language
Timed automata
Formal verification
Science & Technology
Texto completo:http://hdl.handle.net/1822/13099
País:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/13099
Descrição
Resumo:This paper describes a tool-supported method for the formal verification of timed properties of HTL programs, supported by the automated translation tool HTL2XTA, which extracts from a HTL program (i) an Uppaal model and (ii) a set of properties that state the compliance of the model with certain automatically inferred temporal constraints. These can be manually extended with other temporal properties provided by the user. The paper introduces the details of the proposed mechanisms as well as the results of our experimental validation.

Registros relacionados