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/22 20:32] abiernacka [nuXmv] | pn2mc:pt_cp_model_checking [2021/09/23 08:51] (current) | ||
---|---|---|---|
Line 135: | Line 135: | ||
- '' | - '' | ||
- '' | - '' | ||
- | - '' | + | - '' |
+ | - '' | ||
+ | - '' | ||
+ | - '' | ||
+ | These formulae can be added to the nuXmv code file: | ||
+ | < | ||
+ | LTLSPEC G F p5 | ||
+ | LTLSPEC G F p6 | ||
+ | LTLSPEC G F p7 | ||
+ | LTLSPEC G F p8 | ||
+ | LTLSPEC G F p9 | ||
+ | |||
+ | CTLSPEC EF p5 | ||
+ | CTLSPEC EF p6 | ||
+ | CTLSPEC EF p7 | ||
+ | CTLSPEC EF p8 | ||
+ | CTLSPEC EF p9 | ||
+ | |||
+ | LTLSPEC G ((!p0 & !p1 & !p2 & !p3 & !p4) -> (p5 | p6 | p7 | p8 | p9)) | ||
+ | |||
+ | LTLSPEC G (p5 -> (!p0 & !p1)) | ||
+ | LTLSPEC G (p6 -> (!p1 & !p2)) | ||
+ | LTLSPEC G (p7 -> (!p2 & !p3)) | ||
+ | LTLSPEC G (p8 -> (!p3 & !p4)) | ||
+ | LTLSPEC G (p9 -> (!p4 & !p0)) | ||
+ | |||
+ | CTLSPEC AG (p5 -> EF !p5) | ||
+ | CTLSPEC AG (p6 -> EF !p6) | ||
+ | CTLSPEC AG (p7 -> EF !p7) | ||
+ | CTLSPEC AG (p8 -> EF !p8) | ||
+ | CTLSPEC AG (p9 -> EF !p9) | ||
+ | |||
+ | CTLSPEC AG (!p5 -> EF p5) | ||
+ | CTLSPEC AG (!p6 -> EF p6) | ||
+ | CTLSPEC AG (!p7 -> EF p7) | ||
+ | CTLSPEC AG (!p8 -> EF p8) | ||
+ | CTLSPEC AG (!p9 -> EF p9) | ||
+ | </ | ||
+ | |||
+ | LTL and CTL formulae can be then verified in nuXmv tool. | ||
+ | Below are the results of verification for this illustrative example. | ||
+ | |||
+ | < | ||
+ | nuXmv > check_ltlspec | ||
+ | -- specification G ( F p5) is false | ||
+ | -- as demonstrated by the following execution sequence | ||
+ | Trace Description: | ||
+ | Trace Type: Counterexample | ||
+ | -- Loop starts here | ||
+ | -> State: 1.1 <- | ||
+ | s = s0 | ||
+ | p0 = TRUE | ||
+ | p1 = TRUE | ||
+ | p2 = TRUE | ||
+ | p3 = TRUE | ||
+ | p4 = TRUE | ||
+ | p5 = FALSE | ||
+ | p6 = FALSE | ||
+ | p7 = FALSE | ||
+ | p8 = FALSE | ||
+ | p9 = FALSE | ||
+ | -> State: 1.2 <- | ||
+ | s = s3 | ||
+ | p2 = FALSE | ||
+ | p3 = FALSE | ||
+ | p7 = TRUE | ||
+ | -> State: 1.3 <- | ||
+ | s = s0 | ||
+ | p2 = TRUE | ||
+ | p3 = TRUE | ||
+ | p7 = FALSE | ||
+ | </ | ||
+ | Analogical counterexamples are generated for formulae '' | ||
+ | |||
+ | < | ||
+ | -- specification G (p5 -> (!p0 & !p1)) is true | ||
+ | -- specification G (p6 -> (!p1 & !p2)) is true | ||
+ | -- specification G (p7 -> (!p2 & !p3)) is true | ||
+ | -- specification G (p8 -> (!p3 & !p4)) is true | ||
+ | -- specification G (p9 -> (!p4 & !p0)) is true | ||
+ | -- specification G (((((!p0 & !p1) & !p2) & !p3) & !p4) -> ((((p5 | p6) | | ||
+ | p7) | p8) | p9)) is true | ||
+ | nuXmv > check_ctlspec | ||
+ | -- specification EF p5 is true | ||
+ | -- specification EF p6 is true | ||
+ | -- specification EF p7 is true | ||
+ | -- specification EF p8 is true | ||
+ | -- specification EF p9 is true | ||
+ | -- specification AG (p5 -> EF !p5) is true | ||
+ | -- specification AG (p6 -> EF !p6) is true | ||
+ | -- specification AG (p7 -> EF !p7) is true | ||
+ | -- specification AG (p8 -> EF !p8) is true | ||
+ | -- specification AG (p9 -> EF !p9) is true | ||
+ | -- specification AG (!p5 -> EF p5) is true | ||
+ | -- specification AG (!p6 -> EF p6) is true | ||
+ | -- specification AG (!p7 -> EF p7) is true | ||
+ | -- specification AG (!p8 -> EF p8) is true | ||
+ | -- specification AG (!p9 -> EF p9) is true | ||
+ | </ | ||
---- | ---- | ||
==== CADP ==== | ==== CADP ==== | ||
Line 146: | Line 244: | ||
===== CP-net model checking - Producer–consumer example ===== | ===== CP-net model checking - Producer–consumer example ===== | ||
+ | Producer–consumer problem will serve as an explanatory example showing capabilities of the presented approach for coloured Petri nets. | ||
==== Problem ==== | ==== Problem ==== | ||
- | ---- | + | This is a classic problem related to the synchronization of concurrent processes. In the system there are two types of processes: producers who produce some data and consumers who receive these data from producers. Between producers and consumers there is a buffer of a certain capacity. The problem is how to synchronise the two types of processes in such a way that: |
- | ==== nuXmv ==== | + | - Consumers do not try to receive data from empty buffer, |
+ | - Producers 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 | ||
+ | A coloured Petri net model was prepared for this problem. To make this example as easy as possible. there is only one producer and one consumer. Number of consumers and producers can be easily changed for this model. | ||
+ | |||
+ | {{: | ||
+ | |||
+ | 3 enumeration colour sets were defined: | ||
+ | * '' | ||
+ | * '' | ||
+ | * '' | ||
+ | |||
+ | Places '' | ||
+ | |||
+ | 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. | ||
+ | |||
+ | {{: | ||
---- | ---- | ||
+ | ==== nuXmv ==== | ||
+ | Using PetriNet2ModelChecker to translate reachability graph into description of the system in nuXmv code, the following file was generated: | ||
+ | |||
+ | < | ||
+ | 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; | ||
+ | </ | ||
+ | |||
+ | |||
+ | 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 ==== | ||