Search found 6 matches

by iceslj
Mon Jul 11, 2016
Forum: Simulation and trace generation
Topic: A common input format
Replies: 7
Views: 4053

Re: A common input format

Yes, we are defining formal semantics for the terminology of real-time systems. We have built a formal library in Timed Automata, which consists of a set of automata templates, including Task Activation, Job, Scheduler, etc. For example, Task Activation represents the attributes on tasks' activation...
by iceslj
Thu Feb 18, 2016
Forum: Verification challenge
Topic: The FMTV'16 Challenge
Replies: 33
Views: 14300

Re: The FMTV'16 Challenge

I also spent quite a few minutes to understand this drag and drop: one has to drop the file exactly to the "project folder" in the "Project Explorer" pane, instead of just dropping in to the editor pane. I guess some people could also be stuck here.
by iceslj
Mon Feb 08, 2016
Forum: Task sets / Task set generators
Topic: a RT task set from Lunar Rover
Replies: 4
Views: 2227

Re: a RT task set from Lunar Rover

Here is the UPPAAL model of the Lunar Rover control software, its RTOS and its physical environment. We built the model for analyzing a functional-timing problem proposed by the software developers. The model covers a set of tasks which are related to the specific problem. The task set include two t...
by iceslj
Wed Feb 03, 2016
Forum: Task sets / Task set generators
Topic: a RT task set from Lunar Rover
Replies: 4
Views: 2227

Re: a RT task set from Lunar Rover

The paper does not contain the complete UPPAAL model due to the lack of space. But the main parts are in it. The major piece missed in the paper the sporadic task template, which is similar to the periodic task template.
by iceslj
Thu Jan 28, 2016
Forum: Task sets / Task set generators
Topic: a RT task set from Lunar Rover
Replies: 4
Views: 2227

a RT task set from Lunar Rover

We did a formal verification of Chinese Lunar Rover control software, an embedded real-time multitasking software system running over a home-made real-time operating system (RTOS). The main purpose of the verification is to validate if the system satisfies a time-related functional property. We mode...
by iceslj
Fri Jun 26, 2015
Forum: Verification challenge
Topic: Timing verification of an aerial video tracking system using UPPAAL
Replies: 0
Views: 3001

Timing verification of an aerial video tracking system using UPPAAL

Title: Timing Verification of an Aerial Video Tracking System Using UPPAAL Authors: Lijun Shan (College of Computer Science, Northwestern Polytechnical University, Xi'an, China) Susanne Graf (Verimag/CNRS,Gières, France) Abstract: This paper presents two different approaches for verifying the timin...