PAT is a self-contained framework for to support composing, simulating and reasoning of concurrent, real-time systems and other possible domains. It comes with user friendly interfaces, featured model editor and animated simulator. Most importantly, PAT implements various model checking techniques catering for different properties such as deadlock-freeness, divergence-freeness, reachability, LTL properties with fairness assumptions, refinement checking and probabilistic model checking. To achieve good performance, advanced optimization techniques are implemented in PAT, e.g. partial order reduction, symmetry reduction, process counter abstraction, parallel model checking.

References in zbMATH (referenced in 25 articles )

Showing results 1 to 20 of 25.
Sorted by year (citations)

1 2 next

  1. Esparza, Javier: Advances in parameterized verification of population protocols (2017)
  2. Esparza, Javier; Ganty, Pierre; Leroux, Jér^ome; Majumdar, Rupak: Verification of population protocols (2017)
  3. André, Étienne; Benmoussa, Mohamed Mahdi; Choppy, Christine: Formalising concurrent UML state machines using coloured Petri nets (2016)
  4. Carvalho, Gustavo; Cavalcanti, Ana; Sampaio, Augusto: Modelling timed reactive systems from natural-language requirements (2016)
  5. Al-Humaimeedy, Abeer S.; Fernández, Maribel: Enabling synchronous and asynchronous communications in CSP for SOC (2015)
  6. Mota, A.; Farias, A.; Woodcock, J.; Larsen, P.G.: Model checking CML: tool development and industrial applications (2015) ioport
  7. André, Étienne; Liu, Yang; Sun, Jun; Dong, Jin-Song: Parameter synthesis for hierarchical concurrent real-time systems (2014)
  8. Dong, Jin Song; Liu, Yang; Sun, Jun; Zhang, Xian: Towards verification of computation orchestration (2014)
  9. Li, Yi; Dong, Jin Song; Sun, Jing; Liu, Yang; Sun, Jun: Model checking approach to automated planning (2014)
  10. Yamagata, Yoriyuki; Kong, Weiqiang; Fukuda, Akira; Tang, Nguyen Van; Ohsaki, Hitoshi; Taguchi, Kenji: A formal semantics of extended hierarchical state transition matrices using CSP# (2014)
  11. Yuan, Ting; Tang, Yiting; Wu, Xi; Zhang, Yue; Zhu, Huibiao; Guo, Jian; Qin, Weijun: Formalization and verification of REST on HTTP using CSP (2014) ioport
  12. Zhao, Yongxin; Dong, Jinsong; Liu, Yang; Sun, Jun: Towards a combination of CafeOBJ and PAT (2014)
  13. Ben Maissa, Yann; Kordon, Fabrice; Mouline, Salma; Thierry-Mieg, Yann: Modeling and analyzing wireless sensor networks with verisensor: an integrated workflow (2013)
  14. Cranen, Sjoerd; Groote, Jan Friso; Keiren, Jeroen J.A.; Stappers, Frank P.M.; de Vink, Erik P.; Wesselink, Wieger; Willemse, Tim A.C.: An overview of the mCRL2 toolset and its recent advances (2013)
  15. Bae, Kyungmin; Meseguer, José: Model checking LTLR formulas under localized fairness (2012)
  16. Carvalho, Gustavo; Falcão, Diogo; Mota, Alexandre; Sampaio, Augusto: A process algebra based strategy for generating test vectors from SCR specifications (2012)
  17. Lin, Shang-Wei; Liu, Yang; Sun, Jun; Dong, Jin Song; André, Étienne: Automatic compositional verification of timed systems (2012)
  18. Long, Teng; Zhang, Wenhui: Proving liveness property under strengthened compassion requirements (2012)
  19. Luu, Anh Tuan; Sun, Jun; Liu, Yang; Dong, Jin Song: SeVe: automatic tool for verification of security protocols (2012)
  20. Nguyen, Truong Khanh; Sun, Jun; Liu, Yang; Dong, Jin Song; Liu, Yan: Improved BDD-based discrete analysis of timed systems (2012)

1 2 next

Further publications can be found at: