Differences
This shows you the differences between two versions of the page.
| Both sides previous revisionPrevious revision | Both sides next revision | ||
| rtcp_start [2014/11/20 21:35] marcin [Coverability graphs] | rtcp_start [2021/09/23 08:51] (current) | ||
|---|---|---|---|
| Line 122: | Line 122: | ||
| {{ :logo.png |}} | {{ :logo.png |}} | ||
| - | **PetriNet2ModelChecker** tool deals with the problem of translation of reachability graphs for place-transition, | + | **PetriNet2ModelChecker** tool deals with the problem of translation of reachability graphs for place-transition, |
| PetriNet2ModelChecker works with reachability graphs generated respectively by the TINA, CPN Tools and RTCPNC software. Thus, it provides the possibility of formal verification of Petri nets designed with these environments using model checking techniques and mainstream model checkers - nuXmv for LTL and CTL temporal logics, CADP Evaluator for regular alternation-free mu-calculus. Thus, a Petri model can be verified using model checking techniques without necessity of learning any additional language for the specification of requirements. | PetriNet2ModelChecker works with reachability graphs generated respectively by the TINA, CPN Tools and RTCPNC software. Thus, it provides the possibility of formal verification of Petri nets designed with these environments using model checking techniques and mainstream model checkers - nuXmv for LTL and CTL temporal logics, CADP Evaluator for regular alternation-free mu-calculus. Thus, a Petri model can be verified using model checking techniques without necessity of learning any additional language for the specification of requirements. | ||
| It also integrates [[rtcp_start?&# | It also integrates [[rtcp_start?&# | ||