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...

Full description

Bibliographic Details
Main Author: Carvalho, André Ribeiro de (author)
Other Authors: Carvalho, Joel (author), Pinto, Jorge Sousa (author), Sousa, Simão Melo de (author)
Format: conferencePaper
Language:eng
Published: 2010
Subjects:
Model checking
Hierarchical timing language
Timed automata
Formal verification
Science & Technology
Online Access:http://hdl.handle.net/1822/13099
Country:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/13099

Internet

http://hdl.handle.net/1822/13099

Similar Items