Differences
This shows you the differences between two versions of the page.
Next revision | Previous revisionBoth sides next revision | ||
pn2mc:introduction [2014/11/14 18:31] jbiernacki created | 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. \\ | ||
+ | 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** | + | **PetriNet2ModelChecker** |
+ | 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 [[: | ||
**[[: | **[[: |