<?xml version="1.0" encoding="UTF-8"?><xml><records><record><source-app name="Biblio" version="6.x">Drupal-Biblio</source-app><ref-type>47</ref-type><contributors><authors><author><style face="normal" font="default" size="100%">Simão Melo de Sousa</style></author><author><style face="normal" font="default" size="100%">Jorge Sousa Pinto</style></author><author><style face="normal" font="default" size="100%">Joel Carvalho</style></author><author><style face="normal" font="default" size="100%">André Carvalho</style></author></authors></contributors><titles><title><style face="normal" font="default" size="100%">Model- checking temporal properties of real-time HTL programs</style></title><secondary-title><style face="normal" font="default" size="100%">4th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation - ISOLA</style></secondary-title></titles><dates><year><style  face="normal" font="default" size="100%">2010</style></year><pub-dates><date><style  face="normal" font="default" size="100%">October</style></date></pub-dates></dates><urls><related-urls><url><style face="normal" font="default" size="100%">https://haslab.uminho.pt/sites/default/files/jsp/files/2010_isola_10_a.pdf</style></url></related-urls></urls><pub-location><style face="normal" font="default" size="100%">Amirandes, Heraclion, Crete</style></pub-location><abstract><style face="normal" font="default" size="100%">&lt;p&gt;This paper describes a tool-supported method for the formal verication 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.&lt;/p&gt;
</style></abstract></record></records></xml>