PetriDotNet

A PetriDotNet program egy Petri-hálók szerkesztésére, szimulációjára és analízisére szolgáló keretrendszer. A programot a BME Méréstechnika és Információs Rendszerek tanszékén fejlesztjük azzal a céllal, hogy az oktatásban is használható, könnyen kezelhető és bővíthető program legyen.

Célunk a legújabb verifikációs és modellellenőrző algoritmusok megismerése, implementációja és továbbfejlesztése.

A PetriDotNet keretrendszerhez eddig az alábbi analízisek készültek el:

• szaturáción alapuló szimbolikus állapottérgenerálás, -reprezentáció, és ezen fixpont számításon alapuló CTL-modellellenőrzés,
• szaturációalapú LTL és PLTL-modellellenőrzés,
• a modellellenőrzési problémát lineáris programozási feladattá visszavezetve végtelen állapotterű Petri-hálók vizsgálata (CEGAR),
• Markovi modellek sztochasztikus analízise.

A bonyolultabb adatstruktúrák kezelése és analízise fejlesztés alatt van, lelkes, az algoritmusok iránt érdeklődő hallgatókat szívesen látunk a csapatban!

Letöltés

Az eszköz fejlesztés alatt áll, jelenleg korlátozottan érhető el. Az alábbi verziók érhetők el publikusan:

• PetriDotNet -- Formális módszerek tárgy szorgalmi feladatához (1.3.5546) | Felhasználói dokumentáció
• PetriDotNet -- teljes változat, analízis eszközökkel (1.5 beta2) | Felhasználói dokumentáció
• Példamodellek: examples.zip
• PetriDotNet -- PLTL modellellenőrző (2013. évi TDK)

A program futtatásához .NET 4.0 keretrendszer szükséges.

A modellellenőrző modulok fejlesztés alatt állnak, addig is e-mailben szívesen elküldjük!

Az eszközhöz kapcsolódó egyéb fejlesztések:

• Elosztott feladatkezelő keretrendszer mérések futtatásához (1.0) | Kapcsolódó szakdolgozat (felhasználói útmutató a 7. fejezetben)

Publikációk

Referenciák teljes listája (letölthető formában)

TDK-dolgozatok

•  Élő Dániel, Soltész Adrián: Symbolic model checking and trace generation by guided search
  • 1. helyezés, Szoftver szekció, 2015.
• Klenik Attila, Marussy Kristóf: Configurable stochastic analysis framework for asynchronous systems
  • 1. helyezés, Modellezés és szimuláció szekció, 2015.
  • Rektori különdíj
• Molnár Vince, Segesdi Dániel: Múlt és jövő: Új algoritmusok lineáris temporális tulajdonságok szaturáció-alapú modellellenőrzésére
  • 1. helyezés, Intelligens és információs rendszerek Szekció, 2013.
  • OTDK: 2. helyezés, Alkalmazott informatika II. szekció, 2014.
• Molnár Vince: Szaturáció alapú modellellenőrzés lineáris idejű tulajdonságokhoz, TDK-dolgozat.
  • 2. helyezés, Szoftver szekció, 2012.
• Hajdu Ákos, Mártonka Zoltán: Diszkrét dinamikus rendszerek viselkedésének felderítése ellenpélda-alapú absztrakció finomítás (CEGAR) segítségével, TDK-dolgozat.
  • 1. helyezés, Modellezés és szimuláció szekció, 2012.
  • OTDK: 1. helyezés, Rendszertervezés alszekció, Formális módszerek tagozat, 2013.
• Darvas Dániel, Jámbor Attila: Komplex rendszerek modellezése és verifikációja, TDK-dolgozat.
  • 1. helyezés, Szoftver szekció, 2011.
  • OTDK: 2. helyezés és Cisco különdíj, Rendszertervezés alszekció, Kritikus rendszerek tagozat, 2013.
• Darvas Dániel: Szaturáció alapú automatikus modellellenőrző fejlesztése aszinkron rendszerekhez, TDK-dolgozat.
  • 1. helyezés, Szoftver szekció, 2010.
  • OTDK
• Jámbor Attila, Szabó Tamás: Aszinkron rendszerek modellellenőrzése párhuzamos technikákkal, TDK-dolgozat.
  • 2. helyezés, Információs rendszerek szekció, 2010.

​Szakdolgozatok és diplomatervek

• Dániel Darvas: Incremental extension of the saturation algorithm-based bounded model checking of Petri nets, MSc Thesis, 2014.
• Hajdu Ákos: Petri-hálók CEGAR alapú vizsgálatának kiterjesztése, szakdolgozat, 2013.
• Klenik Attila: Szerkesztő keretrendszer Petri-háló alapú modellekhez, szakdolgozat, 2013.
• Jámbor Attila: Időzített modellek ellenőrzése szaturációs algoritmussal, diplomaterv, 2013.
• Molnár Vince: Szaturáció alapú modellellenőrzés lineáris idejű tulajdonságokhoz, szakdolgozat, 2013.
• Darvas Dániel: Petri-háló alapú formális modellek analízise hatékony korlátos modellellenőrzési technikák segítségével, szakdolgozat, 2011.
• Jámbor Attila: Aszinkron rendszerek modellellenőrzése párhuzamos technikákkal, szakdolgozat, 2010.
• Szabó Tamás: Aszinkron rendszerek heurisztikával támogatott modellellenőrzése, szakdolgozat, 2010.
• Szilvási Bertalan: Oktatási segédeszköz fejlesztése Formális módszerek tantárgyhoz, diplomaterv, 2008.

Fontosabb tudományos publikációk

• Ákos Hajdu, András Vörös, and Tamás Bartha. New search strategies for the Petri net CEGAR approach.
  In Raymond Devillers and Antti Valmari, editors, Application and Theory of Petri Nets and Concurrency, volume 9115 of Lecture Notes in Computer Science, pp. 309-328. Springer, 2015. Presented at the 36th International Conference on Application and Theory of Petri Nets and Concurrency.
• Vince Molnár, Dániel Darvas, András Vörös, and Tamás Bartha. Saturation-based incremental LTL model checking with inductive proofs. In C. Baier and C. Tinelli, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 9035 of Lecture Notes in Computer Science, pp. 643-657. Springer, 2015.
• Ákos Hajdu, András Vörös, Tamás Bartha, Zoltán Mártonka: Extensions to the CEGAR Approach on Petri Nets.
  Acta Cybernetica, 21(3):401-417, 2014. DOI: 
• András Vörös, Dániel Darvas, Attila Jámbor, Tamás Bartha: Advanced Saturation-based Model Checking of Well-formed Coloured Petri Nets. Periodica Polytechnica, Electrical Engineering and Computer Science, 58(1):3-13, 2014.
• András Vörös, Dániel Darvas, Tamás Bartha: Bounded saturation-based CTL model checking. Proceedings of the Estonian Academy of Sciences, 62(1):59-70, 2013.
• Tamás Bartha, András Vörös, Attila Jámbor, Dániel Darvas: Verification of an Industrial Safety Function Using Coloured Petri Nets and Model Checking. In: 14th International Conference on Modern Information Technology in the Innovation Processes of the Industrial Enterprises (MITIP 2012), pp. 472-485, 2012.
• András Vörös, Tamás Bartha, Dániel Darvas, Tamás Szabó, Attila Jámbor, Ákos Horváth: Parallel Saturation Based Model Checking. In: The 10th International Symposium on Parallel and Distributed Computing (ISPDC 2011), IEEE Computer Society, 2011.
• A publikációk teljes listája itt található (letölthető formában)

Fejlesztők