Prepare Multitasking Code - R2014b
显示 更早的评论
Hello,
In the help of Polyspace R2014b I found for "Prepare Multitasking Code" the below piece of code:
void upper_approx_C_sequencer(void)
{
volatile int random;
while(1){
if (random) tsk_10ms();
if (random) tsk_30ms();
if (random) tsk_50ms();
...
}
}
I have 2 questions:
1) Shouldn't actually be something like below?
...
if (random > 0) tsk_10ms();
...
In your example the probability to call the function tsk_10ms() is
p_call = ("Nr. of values in int range" - 1) / "Nr. of values in int range" = 1 (approximately)
While the probability to not call the function tsk_10ms() is
p_NoCall = 1 / "Nr. of values in int range" = 0 (approximately)
If the intention is to have the same probability for calling and for not calling the function than we should use a solution similar to what I proposed.
If this is not the case, could you please explain why?
2) I read that Polyspace for volatile variables it can give them any value from the range of the variable. I want to know how this is performed, especially for the code used in multitasking, like the one above. Is Polyspace instrumenting the code? For example between the below lines it introduces others which give to the "random" variable a random value?
if (random) tsk_10ms();
if (random) tsk_30ms();
采纳的回答
Alexandre De Barros
2014-12-3
0 个投票
Hi Daniel!
The word "execution" should not be interpreted as a real (and dynamic) execution. The wikipedia page about abstract interpretation talks about "partial execution". Maybe "abstract execution" would describe this process better. This sentence of the documentation just means that the end of the main should be reached in this abstract execution. If there is a red error, the main is indeed not completly verified since Polyspace can not continue the verification after a red check. And when the main is not completly verified, the tasks are not "launched". The power of abstract interpretation is that it is similar to an execution, this is why use the same words (execution, launched,...) but we are still in a formal domain. And for your first question, again since there is no random values for the 'if', we can't talk about probability. Ranges are used instead of discrete values, and Polyspace propagates these ranges in this abstract execution.
Regards
-- Alex
更多回答（1 个）
Alexandre De Barros
2014-11-26
0 个投票
Hello Daniel,
1) Talking about probability doesn't make sense in the case of formal tools like Polyspace, since there is no execution of the code. Follow this link for more information on how Polyspace works and the power of abstract interpretation: http://www.mathworks.com/discovery/abstract-interpretation.html
2) a volatile variable will be considered "always full-range" by Polyspace (by the way this is the nature of a volatile variable!). The code is not instrumented (again, there is no execution) and Polyspace will simply consider that for the 'if (random)' statements, the if can be true or not. And because random is volatile, Polyspace will also consider that the two values of random can be different for each statement.
Hope that helps!
Last but not least, these topics are covered in the Polyspace trainings.
Best regards,
Alex
类别
在 帮助中心 和 File Exchange 中查找有关 Run Settings 的更多信息
Community Treasure Hunt
Find the treasures in MATLAB Central and discover how the community can help you!
Start Hunting!
Translated by 
