a RT task set from Lunar Rover

Benchmarks and case studies which contain task information but possibly no code
Post Reply
User avatar
iceslj
Posts: 6
Joined: Wed Jul 01, 2015
Location: Verimag @ Grenoble

a RT task set from Lunar Rover

Post by iceslj » Thu Jan 28, 2016

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
Lijun SHAN
E-mail: lijun.shan@imag.fr.
VERIMAG
2, Avenue de Vignate
Centre Equation
F - 38610 GRENOBLE - Gières, FRANCE
Phone : (33) 04.56.52.03.76

Sophie Quinton
Site Admin
Posts: 52
Joined: Tue Apr 28, 2015
Location: Inria Grenoble - Rhône-Alpes, France
Contact:

Re: a RT task set from Lunar Rover

Post by Sophie Quinton » Wed Feb 03, 2016

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
Sophie Quinton
INRIA Grenoble - Rhône-Alpes
655 Avenue de l'Europe - Montbonnot
38334 St Ismier Cedex - FRANCE
tel: +33 4 76 61 55 31
https://team.inria.fr/spades/quinton/

User avatar
iceslj
Posts: 6
Joined: Wed Jul 01, 2015
Location: Verimag @ Grenoble

Re: a RT task set from Lunar Rover

Post by iceslj » Wed Feb 03, 2016

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.
Lijun SHAN
E-mail: lijun.shan@imag.fr.
VERIMAG
2, Avenue de Vignate
Centre Equation
F - 38610 GRENOBLE - Gières, FRANCE
Phone : (33) 04.56.52.03.76

Sophie Quinton
Site Admin
Posts: 52
Joined: Tue Apr 28, 2015
Location: Inria Grenoble - Rhône-Alpes, France
Contact:

Re: a RT task set from Lunar Rover

Post by Sophie Quinton » Wed Feb 03, 2016

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

Thanks,
Sophie
Sophie Quinton
INRIA Grenoble - Rhône-Alpes
655 Avenue de l'Europe - Montbonnot
38334 St Ismier Cedex - FRANCE
tel: +33 4 76 61 55 31
https://team.inria.fr/spades/quinton/

User avatar
iceslj
Posts: 6
Joined: Wed Jul 01, 2015
Location: Verimag @ Grenoble

Re: a RT task set from Lunar Rover

Post by iceslj » Mon Feb 08, 2016

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.
Attachments
LunarRover.xml
(59.42 KiB) Downloaded 144 times
Lijun SHAN
E-mail: lijun.shan@imag.fr.
VERIMAG
2, Avenue de Vignate
Centre Equation
F - 38610 GRENOBLE - Gières, FRANCE
Phone : (33) 04.56.52.03.76

Post Reply