Tools and Benchmarks for Real-Time Systems

Re: a RT task set from Lunar Rover

2016-02-08T11:10:23+01:00

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 types of tasks: periodic and sporadic. Each type of tasks is modeled with a timed-automaton template.

LunarRover.xml

Statistics: Posted by iceslj — Mon Feb 08, 2016

Re: a RT task set from Lunar Rover

2016-02-03T15:20:19+01:00

Thanks for the prompt reply, would it be possible for you to post the entire model here?

Thanks,
Sophie

Statistics: Posted by Sophie Quinton — Wed Feb 03, 2016

Re: a RT task set from Lunar Rover

2016-02-03T14:22:30+01:00

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.

Statistics: Posted by iceslj — Wed Feb 03, 2016

Re: a RT task set from Lunar Rover

2016-02-03T14:06:11+01:00

Hi Lijun,

Thanks for the info! Is the complete UPPAAL model available in the paper or are there some parts missing due to lack of space?

Best,
Sophie

Statistics: Posted by Sophie Quinton — Wed Feb 03, 2016

a RT task set from Lunar Rover

2016-01-28T17:09:25+01:00

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 modeled the RTOS, application tasks and physical environment as timed automata and analyzed the system using statistical model checking (SMC) of UPPAAL. Verification result showed that our model was able to track down undesired behavior in the multitasking system. Moreover, as the modeling framework we designed is general and extensible, it can be a reference method for verifying other real-time multitasking systems.

Link to the paper:
http://link.springer.com/chapter/10.100 ... 06410-9_48

Statistics: Posted by iceslj — Thu Jan 28, 2016