Page 1 of 1

a RT task set from Lunar Rover

Posted: Thu Jan 28, 2016
by iceslj
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

Re: a RT task set from Lunar Rover

Posted: Wed Feb 03, 2016
by Sophie Quinton
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

Re: a RT task set from Lunar Rover

Posted: Wed Feb 03, 2016
by iceslj
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.

Re: a RT task set from Lunar Rover

Posted: Wed Feb 03, 2016
by Sophie Quinton
Thanks for the prompt reply, would it be possible for you to post the entire model here?

Thanks,
Sophie

Re: a RT task set from Lunar Rover

Posted: Mon Feb 08, 2016
by iceslj
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.