Sidebar

Main

Internal

Trace:
Trace: • faq

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
Both sides next revision
pn2mc:pt_cp_model_checking [2014/11/24 23:26]
jbiernacki [Problem] 		pn2mc:pt_cp_model_checking [2021/09/23 08:51] (current)
Line 179: Line 179:
  
 <code> <code>
-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 264: Line 264:
   * ''BUF'' - denoting a buffer. Number of tokens of this type refers to amount of free and occupied slots in the buffer. This colour set has also only one possible colour - ''bufSpace''.   * ''BUF'' - denoting a buffer. Number of tokens of this type refers to amount of free and occupied slots in the buffer. This colour set has also only one possible colour - ''bufSpace''.
  
-Places ''P1'' and ''P2'' refer to producers, ''P3'' and ''P6"" refer to the buffer, ''P4'' and ''P5'' refer to consumers. Tokens in places ''P1'' and ''P5'' denote activity of a producer and a consumer, respectively. Tokens in places ''P2'' and ''P4'' denote waiting for access to the buffer. Occupied slots in the buffer are represented by the tokens in place ''P3'' and free slots are represented by the tokens in place ''P6''.+Places ''P1'' and ''P2'' refer to producers, ''P3'' and ''P6'' refer to the buffer, ''P4'' and ''P5'' refer to consumers. Tokens in places ''P1'' and ''P5'' denote activity of a producer and a consumer, respectively. Tokens in places ''P2'' and ''P4'' denote waiting for access to the buffer. Occupied slots in the buffer are represented by the tokens in place ''P3'' and free slots are represented by the tokens in place ''P6''.
  
 In order to verify the properties of the created model of the system, reachability graph of the net was generated in CPN Tools. Its representation is shown below. In order to verify the properties of the created model of the system, reachability graph of the net was generated in CPN Tools. Its representation is shown below.
Line 272: Line 272:
 ==== nuXmv ==== ==== nuXmv ====
  
-----+Using PetriNet2ModelChecker to translate reachability graph into description of the system in nuXmv code, the following file was generated:
  
 +<code>
 +MODULE main
 +VAR
 + s: {s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12};
 + P5_client : 0..2;
 + P6_bufSpace : 0..2;
 + P4_client : 0..2;
 + P1_factory : 0..2;
 + P3_bufSpace : 0..2;
 + P2_factory : 0..2;
 +ASSIGN
 + init(s) := s1;
 + next(s) := case
 + s = s1 : s2;
 + s = s2 : s3;
 + s = s3 : {s5, s4};
 + s = s4 : {s7, s6};
 + s = s5 : {s1, s7};
 + s = s6 : {s8, s9};
 + s = s7 : {s2, s9};
 + s = s8 : s10;
 + s = s9 : {s3, s10};
 + s = s10 : {s4, s11};
 + s = s11 : {s6, s12};
 + s = s12 : s8;
 + esac;
 + P5_client := case
 + s = s10 : 1;
 + s = s11 : 1;
 + s = s5 : 1;
 + s = s9 : 1;
 + s = s7 : 1;
 + s = s12 : 1;
 + TRUE : 0;
 + esac;
 + P6_bufSpace := case
 + s = s10 : 1;
 + s = s1 : 2;
 + s = s4 : 1;
 + s = s2 : 2;
 + s = s5 : 2;
 + s = s9 : 1;
 + s = s7 : 2;
 + s = s3 : 1;
 + TRUE : 0;
 + esac;
 + P4_client := case
 + s = s1 : 1;
 + s = s8 : 1;
 + s = s6 : 1;
 + s = s4 : 1;
 + s = s2 : 1;
 + s = s3 : 1;
 + TRUE : 0;
 + esac;
 + P1_factory := case
 + s = s11 : 1;
 + s = s1 : 1;
 + s = s6 : 1;
 + s = s5 : 1;
 + s = s9 : 1;
 + s = s3 : 1;
 + TRUE : 0;
 + esac;
 + P3_bufSpace := case
 + s = s10 : 1;
 + s = s11 : 2;
 + s = s8 : 2;
 + s = s6 : 2;
 + s = s4 : 1;
 + s = s9 : 1;
 + s = s12 : 2;
 + s = s3 : 1;
 + TRUE : 0;
 + esac;
 + P2_factory := case
 + s = s10 : 1;
 + s = s8 : 1;
 + s = s4 : 1;
 + s = s2 : 1;
 + s = s7 : 1;
 + s = s12 : 1;
 + TRUE : 0;
 + esac;
 +</code>
 +
 +
 +To verify specified properties of the system, the following LTL formulae were created:
 +
 +  - Consumer do not try to receive data from empty buffer, \\ \\ ''(P3_bufSpace = 0 Λ P4_client = 1) ⇒ ¬X(P5_client = 1)'' \\ \\ 
 +  - Producer do not try to send data to full buffer, \\ \\ ''(P6_bufSpace = 0 Λ P2_factory = 1) ⇒ ¬X(P1_factory = 1)'' \\ \\ 
 +  - There is no possibility of starvation of a consumer, \\ \\ ''GF(P4_client = 1) ⇒ GF(P5_client = 1)'' \\ \\ 
 +  - There is no possibility of starvation of a producer, \\ \\ ''GF(P2_factory = 1) ⇒ GF(P1_factory = 1)'' \\ \\ 
 +  - There are no deadlocks \\ \\ ''GF(P2_factory = 1) Λ GF(P1_factory = 1) Λ GF(P4_client = 1) Λ GF(P5_client = 1)'' \\ \\ 
 +
 +These formulae can be added to the previously generated nuXmv code for the model:
 +
 +<code>
 +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)
 +</code>
 +
 +Verification of satisfiability of these formulae can be performed in nuXmv tool:
 +
 +<code>
 +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
 +</code>
 +----
 ==== CADP ==== ==== CADP ====
  
© Marcin Szpyrka 2008-2024