a RT task set from Lunar Rover

[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

[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

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

[Sophie Quinton]

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

Thanks,
Sophie

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