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:32] jbiernacki | pn2mc:introduction [2021/09/23 08:51] (current) | ||
---|---|---|---|
Line 1: | Line 1: | ||
====== Introduction ====== | ====== Introduction ====== | ||
The most widely used software verification techniques are peer reviewing and testing. In case of concurrent systems, these techniques can cover only a limited portion of possible behaviours. Formal methods can be used to establish a concurrent system correctness with mathematical rigour. \\ | The most widely used software verification techniques are peer reviewing and testing. In case of concurrent systems, these techniques can cover only a limited portion of possible behaviours. Formal methods can be used to establish a concurrent system correctness with mathematical rigour. \\ | ||
- | 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 this problem. It is an intuitive tool which core features enable translation of pupular classes of Petri Nets (P/T-, CP- and RTCP-nets) reachability graphs | ||
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?&# |
**[[: | **[[: |