Differences
This shows you the differences between two versions of the page.
| Both sides previous revisionPrevious revisionNext revision | Previous revisionBoth sides next revision | ||
| pn2mc:pt_cp_model_checking [2014/11/24 23:29] jbiernacki [nuXmv] | pn2mc:pt_cp_model_checking [2021/09/23 08:51] (current) | ||
|---|---|---|---|
| Line 179: | Line 179: | ||
| < | < | ||
| - | NuSMV > check_ltlspec | + | nuXmv > check_ltlspec |
| -- specification G ( F p5) is false | -- specification G ( F p5) is false | ||
| -- as demonstrated by the following execution sequence | -- as demonstrated by the following execution sequence | ||
| Line 218: | Line 218: | ||
| -- specification G (((((!p0 & !p1) & !p2) & !p3) & !p4) -> ((((p5 | p6) | | -- specification G (((((!p0 & !p1) & !p2) & !p3) & !p4) -> ((((p5 | p6) | | ||
| p7) | p8) | p9)) is true | p7) | p8) | p9)) is true | ||
| - | NuSMV > check_ctlspec | + | nuXmv > check_ctlspec |
| -- specification EF p5 is true | -- specification EF p5 is true | ||
| -- specification EF p6 is true | -- specification EF p6 is true | ||
| Line 359: | Line 359: | ||
| esac; | esac; | ||
| </ | </ | ||
| - | ---- | ||
| + | |||
| + | To verify specified properties of the system, the following LTL formulae were created: | ||
| + | |||
| + | - Consumer do not try to receive data from empty buffer, \\ \\ '' | ||
| + | - Producer do not try to send data to full buffer, \\ \\ '' | ||
| + | - There is no possibility of starvation of a consumer, \\ \\ '' | ||
| + | - There is no possibility of starvation of a producer, \\ \\ '' | ||
| + | - There are no deadlocks \\ \\ '' | ||
| + | |||
| + | These formulae can be added to the previously generated nuXmv code for the model: | ||
| + | |||
| + | < | ||
| + | LTLSPEC (P3_bufSpace=0 & P4_client=1) -> !X(P5_client=1) | ||
| + | LTLSPEC (P6_bufSpace=0 & P2_factory=1) -> !X(P1_factory=1) | ||
| + | LTLSPEC G F (P4_client=1) -> G F (P5_client=1) | ||
| + | LTLSPEC G F (P2_factory=1) -> G F (P1_factory=1) | ||
| + | LTLSPEC G F (P2_factory=1) & G F (P1_factory=1) & G F (P4_client=1) & G F (P5_client=1) | ||
| + | </ | ||
| + | |||
| + | Verification of satisfiability of these formulae can be performed in nuXmv tool: | ||
| + | |||
| + | < | ||
| + | nuXmv > check_ltlspec | ||
| + | -- specification ( G ( F P4_client = 1) -> G ( F P5_client = 1)) is true | ||
| + | -- specification ( G ( F P2_factory = 1) -> G ( F P1_factory = 1)) is true | ||
| + | -- specification ((P3_bufSpace = 0 & P4_client = 1) -> !( X P5_client = 1)) | ||
| + | is true | ||
| + | -- specification ((P6_bufSpace = 0 & P2_factory = 1) -> !( X P1_factory = | ||
| + | 1)) is true | ||
| + | -- specification ((( G ( F P2_factory = 1) & G ( F P1_factory = 1)) & G ( F | ||
| + | P4_client = 1)) & G ( F P5_client = 1)) is true | ||
| + | </ | ||
| + | ---- | ||
| ==== CADP ==== | ==== CADP ==== | ||