Tools and Benchmarks for Real-Time Systems

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

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.

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

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.

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

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