Difference between revisions of "Extending the Static Checker (How to extend Rodin Tutorial)"
From Event-B
Jump to navigationJump to searchimported>Tommy m (→In this part) |
imported>Tommy m (→In this part) |
||
| Line 4: | Line 4: | ||
We will see how to add rules to statically check the machines after our extension. The Static Checker is one dedicated part of the Proof Obligation generation process. In fact, we have to be sure before creating Proof Obligations, that the model is correctly expressed (i.e. proof obligations are generated for a model which is sound).<br> | We will see how to add rules to statically check the machines after our extension. The Static Checker is one dedicated part of the Proof Obligation generation process. In fact, we have to be sure before creating Proof Obligations, that the model is correctly expressed (i.e. proof obligations are generated for a model which is sound).<br> | ||
| + | The question addressed here is : " '''Which are the conditions under which the model is correct for proof obligation generation?''' ".<br> | ||
=== Step1 === | === Step1 === | ||
Revision as of 08:19, 27 August 2010
In this part
We will see how to add rules to statically check the machines after our extension. The Static Checker is one dedicated part of the Proof Obligation generation process. In fact, we have to be sure before creating Proof Obligations, that the model is correctly expressed (i.e. proof obligations are generated for a model which is sound).
The question addressed here is : " Which are the conditions under which the model is correct for proof obligation generation? ".
