<?xml version="1.0" encoding="UTF-8"?>
<feed xmlns="http://www.w3.org/2005/Atom" xml:lang="en-gb">
	<link rel="self" type="application/atom+xml" href="http://localhost/app.php/feed/topic/34" />

	<title>Tools and Benchmarks for Real-Time Systems</title>
	<subtitle>ECRTS Community Forum</subtitle>
	<link href="http://localhost/index.php" />
	<updated>2015-06-26T13:42:54+01:00</updated>

	<author><name><![CDATA[Tools and Benchmarks for Real-Time Systems]]></name></author>
	<id>http://localhost/app.php/feed/topic/34</id>

		<entry>
		<author><name><![CDATA[iceslj]]></name></author>
		<updated>2015-06-26T13:42:54+01:00</updated>

		<published>2015-06-26T13:42:54+01:00</published>
		<id>http://localhost/viewtopic.php?t=34&amp;p=32#p32</id>
		<link href="http://localhost/viewtopic.php?t=34&amp;p=32#p32"/>
		<title type="html"><![CDATA[Timing verification of an aerial video tracking system using UPPAAL]]></title>

		
		<content type="html" xml:base="http://localhost/viewtopic.php?t=34&amp;p=32#p32"><![CDATA[
<strong class="text-strong">Title:</strong> Timing Verification of an Aerial Video Tracking System Using UPPAAL<br><br><strong class="text-strong">Authors:</strong><br>Lijun Shan (College of Computer Science, Northwestern Polytechnical University, Xi'an, China)<br>Susanne Graf (Verimag/CNRS,Gières, France)<br><br><strong class="text-strong">Abstract:</strong> This paper presents two different approaches for verifying the timing properties of the industrial use cases proposed as two challenges by WATERS’2015. The system under study is an aerial video system which contains two parts, a multiprocessor system and a uni-processor multitasking system. A timed automata model is constructed for each subsystem with the model checker UPPAAL. The symbolic model checking and statistical model checking functions of UPPAAL are applied to verify the models. Each of the models is modular, reusable and extensible, and can act as a general modeling framework for analyzing a type of systems.<br><br><strong class="text-strong">Keywords:</strong> Real-time systems; verification; model checking<br><br><strong class="text-strong">Attached paper:</strong> <div class="inline-attachment"><dl class="file"><dt><span class="imageset icon_topic_attach"></span> <a class="postlink" href="http://localhost/download/file.php?id=22&amp;sid=d74079af129d5480a5ac4fd1778eecc1">FMTV15_Solution_UPPAAL.pdf</a></dt></dl></div><p>Statistics: Posted by <a href="http://localhost/memberlist.php?mode=viewprofile&amp;u=70">iceslj</a> — Fri Jun 26, 2015</p><hr />
]]></content>
	</entry>
	</feed>
