Differences
This shows you the differences between two versions of the page.
| Both sides previous revisionPrevious revisionNext revision | Previous revisionBoth sides next revision | ||
| pn2mc:introduction [2014/11/14 19:34] jbiernacki | pn2mc:introduction [2021/09/23 08:51] (current) | ||
|---|---|---|---|
| Line 3: | Line 3: | ||
| Model checking is one of the most promising techniques for automatic software analysis and Petri nets are one of the most widespread formalisms used in software engineering. Unfortunately, | Model checking is one of the most promising techniques for automatic software analysis and Petri nets are one of the most widespread formalisms used in software engineering. Unfortunately, | ||
| - | **PetriNet2ModelChecker** was designed to face the problem | + | **PetriNet2ModelChecker** was designed to face this problem. It is an intuitive tool which core features enable |
| As a result, the tool provides for the automatic model checking of nets created in the TINA and CPN Tools environments. The presented solution 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. | As a result, the tool provides for the automatic model checking of nets created in the TINA and CPN Tools environments. The presented solution 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. | ||
| - | PetriNet2ModelChecker integrates [[rtcp_start?&# | + | PetriNet2ModelChecker integrates [[:rtcp_start?&# |
| **[[: | **[[: | ||