PAT


Process Analysis Toolkit (PAT) is developed by Semantic Engineering (SemEng). It is a self-contained framework for simulating and verifying real-time, concurrent, and probabilistic systems.

Introduction


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. So far, PAT has 4370+ registered users from 1341+ organizations in 150 countries and regions.

Screenshot:

GUI-Training

The main functionalities of PAT are listed as follows:

  • User friendly editing environment (multi-document, multi-language, I18N GUI and advanced syntax editing features) for introducing models
  • User friendly simulator for interactively and visually simulating system behaviors; by random simulation, user-guided step-by-step simulation, complete state graph generation, trace playback, counterexample visualization, etc.
  • Easy verification for deadlock-freeness analysis, reachability analysis, state/event linear temporal logic checking (with or with fairness) and refinement checking.
  • A wide range of built-in examples ranging from benchmark systems to newly developed algorithms/protocols.

We design PAT as an extensible and modularized framework, which allows user to build customized model checkers easily. We provide a library of model checking algorithms as well as the support for customizing language syntax, semantics, model checking algorithms and reduction techniques, graphic user interfaces, and domain specific abstraction techniques. Delightfully, PAT has been growing up to eleven modules today to deal with problems in different domains including Real Time Systems, Web Service Models, Probability Models, and Sensor Networks etc. In order to be state-of-the-art, we are actively developing PAT to cope with latest formal-automated system analysis techniques.

We have been using PAT to model and verify a variety of systems. Ranging from recently proposed distributed algorithms, security protocols to real-world systems like multi-lift and pacemaker systems. Previously unknown bugs have been discovered. The Post to Post Links II error: No post found with slug "experiments" results show that PAT is capable of verifying systems with large number of states and outperforms the popular model checkers in some cases. We have successfully demonstrated PAT as an analyzer for process algebras in the 30th International Conference on Software Engineering (ICSE 2008), the 21st International Conference on Computer Aided Verification (CAV 2009), International Symposium on the Foundations of Software Engineering (FSE 2010), and the 22nd annual International Symposium on Software Reliability Engineering (ISSRE 2011).

20 Year ICFEM Most Influential System Award


    3 founders Jun, Yang and Jin Song have been awarded the 20 Year ICFEM Most Influential System Award for developing the PAT verification system. The award was presented by the ICFEM founder Prof. Shaoying Liu (FIEEE) at 20th ICFEM on 14 Nov 2018.

    Sir Tony C.A.R. Hoare (Turing Award) was awarded the 20 Year ICFEM Most Influential Person Award. Prof. Michael Butler was awarded 20 Year ICFEM Outstanding Service Award.

    PAT Award

System Design


System Architecture

Starting from version 3.5, PAT is developed to be a generic framework, which can be easily extended to support new modeling languages or new assertion languages (as well as dedicated verification algorithms). The system architecture is shown in the following figure.

GUI-Training

In PAT, each language is encapsulated as one module with predefined APIs, which identify the (specialized) language syntax, well-formness rules as well as (operational) formal semantics, and loaded at run time according to the input model. This architecture allows new languages to be developed easily by providing the syntax rules and semantics. Three modules have been developed currently, namely Communicating Sequential Processes (CSP) module, Real-Time System (RTS) Module and Web Service (WS) module. An extensible library of assertions, together with their verification algorithms, have been designed to operate on the underlying shared semantic models of the modules and therefore easily applicable to all modules. For instance, the automata-based LTL model checking algorithm, with partial order reduction, is applied to allmodules.

System Components

The following are the four main components of PAT.

  • Editor: User friendly editing envinronment (with advanced syntax editing features) for introducing models.
  • Parser: Smart parsing to apply process equivalence laws to simply system models as well as associating assertions with the dedicated checker.
  • Simulator: User friendly simulator for interactively and visually simulating system behaviors; by either random simulation, user-guided step-by-step simulation, complete state graph generation, trace playback, counterexample visualization, etc.
  • Model Checkers: Click button model checker for deadlock-freeness verification, reachability analysis, state/event linear temporal logic verification (with or with fairness) and refinement checking (with or without checking data components).

GUI-Training

The above highlights the work flow of PAT. The parser takes in the system model and then builds the internal representation. Different assertions are associated with the dedicated analyzers respectively. If the assertion involves LTL, it is automatically translated into an equivalent Buchi automaton. The internal representaion of the model can be fed to the simulator for simulation or the verifiers for verification. If a counterexample is generated, the counterexample may be fed to the simulator.

Software Components

PAT is implemented using C# 4.0 and Visual Studio 2010. The following external components are used or embedded in the PAT package.

  • PAT’s parser is based on Antlr Parser Generator.
  • The LTL to Buchi Automata Converter in PAT is based on Paul Gastin’s work on fast translation from LTL to Buchi automata. We have translated the original c++ code to C#.
  • PAT’s editor (i.e., mulit-document environment) is based on dotnetfireball.
  • PAT’s unit testing component is done using NUnit.
  • PAT is formally verified by Contracts and Spec#.

Publications


    When you cite PAT, please use our CAV 09 paper: PAT: Towards Flexible Verification under Fairness. (Bib)

    2021

    1. Bride, Hadrien, Jin Song Dong, Ryan Green, Zhé Hóu, Brendan Mahony, and Martin Oxenham. “GRAVITAS: A model checking based planning and goal reasoning framework for autonomous systems.” Engineering Applications of Artificial Intelligence 97 (2021): 104091. (Pdf)

    2020

    1. Bride, Hadrien, Cheng-Hao Cai, Jin Song Dong, Rajeev Gore, Zhé Hóu, Brendan Mahony, and Jim McCarthy. “N-PAT: A Nested Model-Checker – (System Description).” In International Joint Conference on Automated Reasoning, pp. 369-377. Springer, Cham, 2020. (HTML, Pdf)

    2019

    1. Jegourel, Cyrille, Jun Sun, and Jin Song Dong. “Sequential schemes for frequentist estimation of properties in statistical model checking.” ACM Transactions on Modeling and Computer Simulation (TOMACS) 29, no. 4 (2019): 1-22. (Pdf)

    2018

    1. Shi, Ling, Yongxin Zhao, Yang Liu, Jun Sun, Jin Song Dong, and Shengchao Qin. “A UTP semantics for communicating processes with shared variables and its formal encoding in PVS.” Formal Aspects of Computing 30, no. 3-4 (2018): 351-380. (Pdf)
    2. Mahadewa, Kulani Tharaka, Kailong Wang, Guangdong Bai, Ling Shi, Jin Song Dong, and Zhenkai Liang. “Homescan: Scrutinizing implementations of smart home integrations.” In 2018 23rd International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 21-30. IEEE, 2018. (Pdf)
    3. Thin, Wai Yan Maung Maung, Naipeng Dong, Guangdong Bai, and Jin Song Dong. “Formal analysis of a proof-of-stake blockchain.” In 2018 23rd International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 197-200. IEEE, 2018. (Pdf)
    4. Fernando, Dileepa, Naipeng Dong, Cyrille Jegourel, and Jin Song Dong. “Verification of strong Nash-equilibrium for probabilistic BAR systems.” In International Conference on Formal Engineering Methods, pp. 106-123. Springer, Cham, 2018. (Pdf)
    5. Jegourel, Cyrille, Jun Sun, and Jin Song Dong. “On the sequential Massart algorithm for statistical model checking.” In International Symposium on Leveraging Applications of Formal Methods, pp. 287-304. Springer, Cham, 2018. (Pdf)

    2017

    1. Bai, Guangdong, Quanqi Ye, Yongzheng Wu, Heila Botha, Jun Sun, Yang Liu, Jin Song Dong, and Willem Visser. “Towards model checking android applications.” IEEE Transactions on Software Engineering 44, no. 6 (2017): 595-612. (Pdf)
    2. Li, Li, Jun Sun, Yang Liu, Meng Sun, and Jin-Song Dong. “A formal specification and verification framework for timed security protocols.” IEEE Transactions on Software Engineering 44, no. 8 (2017): 725-746. (Pdf)
    3. Shi, Ling, Shuang Liu, Jianye Hao, Jun Yang Koh, Zhe Hou, and Jin Song Dong. “Towards solving decision making problems using probabilistic model checking.” In 2017 22nd International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 150-153. IEEE, 2017. (Pdf)
    4. Jegourel, Cyrille, Jun Sun, and Jin Song Dong. “Sequential schemes for frequentist estimation of properties in statistical model checking.” In International Conference on Quantitative Evaluation of Systems, pp. 333-350. Springer, Cham, 2017. (Pdf)

    2016

    1. Zhu, Huiquan, Jing Sun, Jin Song Dong, and Shang-Wei Lin. “From verified model to executable program: the PAT approach.” Innovations in Systems and Software Engineering 12, no. 1 (2016): 1-26. (Pdf)
    2. Song, Songzheng, Jiexin Zhang, Yang Liu, Mikhail Auguston, Jun Sun, Jin Song Dong, and Tieming Chen. “Formalizing and verifying stochastic system architectures using Monterey Phoenix.” Software & Systems Modeling 15, no. 2 (2016): 453-471. (Pdf)
    3. Li, Li, Jun Sun, and Jin Song Dong. “Automated Verification of Timed Security Protocols with Clock Drift.” In International Symposium on Formal Methods, pp. 513-530. Springer, Cham, 2016. (Pdf)
    4. Fernando, Dileepa, Naipeng Dong, Cyrille Jegourel, and Jin Song Dong. “Verification of Nash-equilibrium for probabilistic BAR systems.” In 2016 21st International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 53-62. IEEE, 2016. (Pdf)
    5. Chen, Manman, Tian Huat Tan, Jun Sun, Jingyi Wang, Yang Liu, Jing Sun, and Jin Song Dong. “Service adaptation with probabilistic partial models.” In International Conference on Formal Engineering Methods, pp. 122-140. Springer, Cham, 2016. (Pdf)
    6. Nguyen, Truong Khanh, Tian Huat Tan, Jun Sun, Jiaying Li, Yang Liu, Manman Chen, and Jin Song Dong. “Scaling BDD-based Timed Verification with Simulation Reduction.” In International Conference on Formal Engineering Methods, pp. 363-382. Springer, Cham, 2016. (Pdf)
    7. Tan, Tian Huat, Manman Chen, Jun Sun, Yang Liu, Étienne André, Yinxing Xue, and Jin Song Dong. “Optimizing selection of competing services with probabilistic hierarchical refinement.” In 2016 IEEE/ACM 38th International Conference on Software Engineering (ICSE), pp. 85-95. IEEE, 2016. (Pdf)

    2015

    1. Wang, Ting, Jun Sun, Xinyu Wang, Yang Liu, Yuanjie Si, Jin Song Dong, Xiaohu Yang, and Xiaohong Li. “A Systematic Study on Explicit-State Non-Zenoness Checking for Timed Automata.” IEEE Transactions on Software Engineering 41, no. 01 (2015): 3-18. (Pdf)
    2. Li, Li, Jun Sun, Yang Liu, and Jin Song Dong. “Verifying parameterized timed security protocols.” In International Symposium on Formal Methods, pp. 342-359. Springer, Cham, 2015. (Pdf)
    3. Dong, Jin Song, Ling Shi, Kan Jiang, and Jing Sun. “Sports strategy analytics using probabilistic reasoning.” In 2015 20th International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 182-185. IEEE, 2015.

    2014

    1. Song, S.; Liu, Y.; Zhang, J.; and Sun, J. An extensive model checking framework for multi-agent systems. In Proceedings of Autonomous Agents & Multiagent Systems (AAMAS), pages 1645-1646, 2014. (Pdf, Bib)
    2. Hansen, H.; Lin, S.; Liu, Y.; Nguyen, T. K.; and Sun, J. Diamonds Are a Girl’s Best Friend: Partial Order Reduction for Timed Automata with Abstractions. In Proceedings of Computer Aided Verification (CAV), pages 391-406, 2014. (Pdf, Bib)
    3. Dong, J. S.; Liu, Y.; Sun, J.; and Zhang, X. Towards verification of computation orchestration. Formal Asp. Comput. (FAC), 26(4):729-759. 2014. (Pdf, Bib)
    4. Li, Y.; Dong, J. S.; Sun, J.; Liu, Y.; and Sun, J. Model checking approach to automated planning. Formal Methods in System Design (FMSD), 44(2):176-202. 2014. (Pdf, Bib)
    5. Si, Y.; Sun, J.; Liu, Y.; Dong, J. S.; Pang, J.; Zhang, S. J.; and Yang, X. Model checking with fairness assumptions using PAT. Frontiers of Computer Science (FCSC), 8(1):1-16. 2014. (Pdf, Bib)

    2013

    1. Shuang Liu, Yang Liu, Jun Sun, Manchun Zheng, Bimlesh Wadhwa and Jin Song Dong. USMMC: A Self-Contained Model Checker for UML State Machines. The 9th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE 2013) , August 21-23, 2013, Saint Petersburg, Russia. (Accepted).
    2. Jianan Hao, Yang Liu, Wentong Cai, Guangdong Bai and Jun Sun. vTRUST: A Formal Modeling and Verification Framework for Virtualization Systems. 15th International Conference on Formal Engineering Methods (ICFEM 2013) , Oct 29 – Nov 1, Queenstown, New Zealand. (Accepted).
    3. Yuanjie Si, Jun Sun, Yang Liu and Ting Wang. Improving Model Checking Stateful Timed CSP with non-Zenoness through Clock-Symmetry Reduction. 15th International Conference on Formal Engineering Methods (ICFEM 2013) , Oct 29 – Nov 1, Queenstown, New Zealand. (Accepted).
    4. Manman Chen, Tian Huat Tan, Jun Sun and Yang Liu. Verification of Functional and Non-functional Requirements of Web Service Composition. 15th International Conference on Formal Engineering Methods (ICFEM 2013) , Oct 29 – Nov 1, Queenstown, New Zealand. (Accepted).
    5. Ling Shi, Yongxin Zhao, Yang Liu, Jun Sun, Jin Song Dong and Shengchao Qin. A UTP Semantics for Communicating Processes with Shared Variables. 15th International Conference on Formal Engineering Methods (ICFEM 2013) , Oct 29 – Nov 1, Queenstown, New Zealand. (Accepted).
    6. Kun Ji, Yang Liu, Shang-Wei Lin, Jun Sun, Jin Song Dong and Truong Khanh Nguyen. CELL: A Compositional Verification Framework. The 11th International Symposium on Automated Technology for Verification and Analysis (ATVA 2013) , October 15 – 18, 2013, Hanoi, Vietnam. (Accepted).
    7. Takahiro Ando, Hirokazu Yatsu, Weiqiang Kong, Kenji Hisazumi, and Akira Fukuda. Formalization and Model Checking of SysML State Machine Diagrams by CSP#. In: The 2013 International Conference on Computational Science and Its Applications (ICCSA 2013), Ho Chi Minh City, Vietnam, June 24-27, 2013. (accepted to be published)
    8. Jin Song Dong, Yang Liu, Jun Sun, Xian Zhang. Towards verification of computation orchestration. Formal Aspects of Computing (FAOC). (Accepted)
    9. Lin Gui, Jun Sun, Yang Liu, Yuanjie Si, Jinsong Dong and Xinyu Wang. Combining Model Checking and Testing with an Application to Reliability Prediction and Distribution. The International Symposium in Software Testing and Analysis (ISSTA 2013) , Lugano, Switzerland, 15-20 July 2013. (Accepted).
    10. Shuang Liu, Yang Liu, Étienne André, Christine Choppy, Jun Sun, Bimlesh Wadhwa and Jin Song Dong. A Formal Semantics for the Complete Syntax of UML State Machines with Communications. The 10th International Conference on integrated Formal Methods (iFM 2013), June 10 – 14, Turku, Finland, 2013. (Pdf, Bib, Slides)
    11. Songzheng Song, Lin Gui, Jun Sun, Yang Liu and Jin Song Dong. Improved Reachability Analysis in DTMC via Divide and Conquer. The 10th International Conference on integrated Formal Methods (iFM 2013), Turku, Finland, June 10 – 14, 2013. (Pdf, Bib, Slides)
    12. Jun Sun, Yang Liu, Jin Song Dong, Yan Liu, Ling Shi, Étienne André. Modeling and Verifying Hierarchical Real-time Systems using Stateful Timed CSP. The ACM Transactions on Software Engineering and Methodology (TOSEM), 22(1):3:1-3:29, 2013. (Pdf, Bib)
    13. Étienne André, Yang Liu, Jun Sun, Jin Song Dong and Shang-Wei Lin. Parameter Synthesis for Hierarchical Concurrent Real-Time Systems. The 25th International Conference on Computer Aided Verification (CAV 2013), Saint Petersburg, Russia, July 13 – 19, 2013 (Accepted).
    14. Jin Song Dong, Jun Sun and Yang Liu. Build Your Own Model Checker in One Month. The 35th International Conference on Software Engineering (ICSE 2013), Tutorial, San Francisco, CA, USA, May 18th – 26th, 2013 (Pdf).
    15. Tian Huat Tan, Etienne Andre, Jun Sun, Yang Liu, Jin Song Dong and Manman Chen. Dynamic Synthesis of Local Time Requirement for Service Composition. The 35th International Conference on Software Engineering (ICSE 2013), San Francisco, CA, USA, May 18 – 26, 2013. (Bib, Slides)
    16. Guangdong Bai, Jike Lei, Guozhu Meng, Sai Sathyanarayan Venkatraman, Prateek Saxena, Jun Sun, Yang Liu, and Jin Song Dong. AUTHSCAN: Automatic Extraction of Web Authentication Protocols from Implementations. Proceedings of the Network and Distributed System Security Symposium, NDSS 2013, San Diego, California, USA, February 24-27, 2013. (Pdf, Bib, Slides)
    17. Yang Liu, Wei Chen, Yanghong A. Liu, S.J. Zhang, J. Sun and Jin Song Dong. Verifying Linearizability via Optimized Refinement Checking, IEEE Transactions on Software Engineering (TSE). (Accepted)
    18. Manchun Zheng, David Sanán, Jun Sun, Yang Liu, Jin Song Dong and Yu Gu. State Space Reduction for Sensor Networks using Two-level Partial Order Reduction. The 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI2013), pages 515-535, Rome, Italy, January 20-22, 2013. (Pdf, Bib, Slides)

    2012

    1. Suman Roy, Sidharth Bihary and Jose Alfonso Corso Laos. A Conformance Checker Tool CSPConCheck. The 9th International Colloquium on Theoretical Aspects of Computing (ICTAC 2012), pages 159-163, Bangalore, India, September 24 – 27, 2012.
    2. Oguzcan OGUZ, Jan F. BROENINK and Angelika MADER. Schedulability Analysis of Timed CSP Models Using the PAT Model Checker. The 34th Communicating Process Architectures Conference, CPA 2012, organised under the auspices of WoTUG, Dundee, Scotland, August 26 – 29, 2012.
    3. Vwen Yen Lee, Yan Liu, Xian Zhang, Clifton Phua, Kelvin Sim, Jiaqi Zhu, Jit Biswas, Jin Song Dong, Mounir Mokhtari. ACARP: Auto Correct Activity Recognition Rules Using Process Analysis Toolkit (PAT). The 10th International Conference on Smart Homes and Health Telematics, ICOST 2012, Artiminio, Italy, June 12 – 15, 2012.
    4. Jie Xin Zhang, Yang Liu, Jing Sun, Jin Song Dong and Jun Sun. Model Checking Software Architecture Design. The 14th International Symposium on High-Assurance Systems Engineering (HASE 2012), pages 193-200, Omaha, USA, October 25 -27, 2012 (Pdf, Bib).
    5. Jiexin Zhang, Yang Liu, Mikhail Auguston, Jun Sun and Jin Song Dong. Using Monterey Phoenix to Formalize and Verify System Architectures. The 19th Asia-Pacific Software Engineering Conference (APSEC 2012), Hong Kong, December 4 – 7, 2012 (Pdf).
    6. Ting Wang, Songzheng Song, Jun Sun, Yang Liu, Jin Song Dong, Xinyu Wang and Shanping Li. More Anti-Chain Based Refinement Checking. The 14th International Conference on Formal Engineering Methods (ICFEM 2012), pages 364-380, Kyoto, Japan, November 12 – 16, 2012. (Pdf, Bib)
    7. Shang-Wei Lin, Yang Liu, Pao-Ann Hsiung, Jun Sun and Jin Song Dong. Automatic Generation of Provably Correct Embedded Systems. The 14th International Conference on Formal Engineering Methods (ICFEM 2012), pages 214-229, Kyoto, Japan, November 12 – 16, 2012. (Pdf, Bib, Slides)
    8. Ling Shi, Yang Liu, Jun Sun, Jin Song Dong and Gustavo Carvalho. An Analytical and Experimental Comparison of CSP Extensions and Tools. The 14th International Conference on Formal Engineering Methods (ICFEM 2012), pages 381-397, Kyoto, Japan, November 12 – 16, 2012. (Pdf, Bib, Slides)
    9. Truong Khanh Nguyen, Jun Sun, Yang Liu and Jin Song Dong. Symbolic Model-Checking of Stateful Timed CSP using BDD and Digitization. The 14th International Conference on Formal Engineering Methods (ICFEM 2012), pages 398-413, Kyoto, Japan, November 12 – 16, 2012. (Pdf, Bib)
    10. Yi Li, Jing Sun, Jin Song Dong, Yang Liu and Jun Sun. Planning as Model Checking Tasks. The 35th Annual IEEE Software Engineering Workshop (SEW-35), Heraclion, Crete, Greece, Oct 12 – 13, 2012 (Accepted).
    11. Jianye Hao, Songzheng Song, Yang Liu, Jun Sun, Liu Gui, Jin Song Dong and Ho-Fung Leung. Probabilistic Model Checking Multi-agent Behaviors in Dispersion Games Using Counter Abstraction. The 15th International Conference on Principles and Practice of Multi-Agent Systems (PRIMA 2012), pages 16-30, Kuching, Sarawak, Malaysia, September 3 – 7, 2012. (Pdf, Bib)
    12. Chunqing Chen, Jun Sun, Yang Liu, Jin Song Dong and Manchun Zheng. Formal Modeling and Validation of Stateflow Diagrams. The International Journal on Software Tools for Technology Transfer (STTT), 14:653-671, 2012. (Pdf, Bib)
    13. Shang-Wei Lin, Yang Liu, Jun Sun, Jin Song Dong and Étienne André. Automatic Compositional Verification of Timed Systems. The 18th International Symposium on Formal Methods (FM 2012), pages 272-276, Paris, France, Auguest 27 – 31, 2012. (Pdf, Bib, Slides)
    14. Truong Khanh Nguyen, Jun Sun, Yang Liu, Jin Song Dong and Yan Liu. Improved BDD-based Discrete Analysis of Timed Systems. The 18th International Symposium on Formal Methods (FM 2012), pages 326-340, Paris, France, Auguest 27 – 31, 2012. (Pdf, Bib, Slides)
    15. Yan Liu, Xian Zhang, Yang Liu, Jun Sun, Jin Song Dong, Jit Biswas and Mounir Mokhtari. Formal Analysis of Pervasive Computing Systems. The 17th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2012), pages 169-178, Paris, France, July 18 – 20, 2012. (Pdf, Bib, Slides)
    16. Yi Li, Jing Sun, Jin Song Dong and Yang Liu. Translating PDDL into CSP# – the PAT Approach. The 17th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2012), pages 240-249, Paris, France, July 18 – 20, 2012. (Pdf, Bib)
    17. Étienne André, Yang Liu, Jun Sun and Jin Song Dong. Parameter Synthesis for Hierarchical Concurrent Real-Time Systems. The 17th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2012), pages 253-262, Paris, France, July 18 – 20, 2012. (Pdf, Bib, Slides)
    18. Songzheng Song, Jun Sun, Yang Liu, and Jin Song Dong. A Model Checker for Hierarchical Probabilistic Real-time Systems. The 24th International Conference on Computer Aided Verification (CAV 2012), pages 705-711, Berkeley, California, USA, July 7-13, 2012. (Pdf, Bib, Slides)
    19. GuanJun Liu, Jun Sun, Yang Liu, and Jin Song Dong. Complexity of the Soundness Problem of Bounded Workflow Nets. The 33rd International Conference on Application and Theory of Petri Nets and Concurrency (PN 2012), pages 92-107, Hamburg, Germany, June 25-29, 2012. (Pdf, Bib, Slides)
    20. Songzheng Song, Jianye Hao, Yang Liu, Jun Sun, Ho-Fung Leung, and Jin Song Dong. Analyzing Multi-agent Systems with Probabilistic Model Checking Approach. The 34th International Conference on Software Engineering (ICSE 2012), New Ideas and Emerging Results (NIER), pages 1337-1340, Zurich, Switzerland, June 2 – 9, 2012. (Pdf, Bib, Slides)
    21. Luu Anh Tuan, Jun Sun, Yang Liu, Jin Song Dong, Xiaohong Li, and Quan Thanh Tho. SEVE: Automatic Tool for Verification of Security Protocols. Frontiers of Computer Science, Special Issue on Formal Engineering Method, 6(1):57-75, 2012. (Bib)
    22. Nguyen Chi Dat. Multi-Core Model Checking. FYP Report, 2012. (Pdf)
    23. Xian Zhang. Verification of Timed Process Algebra and Beyond. Phd Thesis, 2012. (Pdf)

    2011

    1. Yi Li. Model Checking as Planning and Service. FYP Report, 2011. (Pdf)
    2. Truong Khanh Nguyen, Jun Sun, Yang Liu and Jin Song Dong. A Symbolic Model Checking Framework for Hierarchical Systems. The 26th IEEE/ACM International Conference On Automated Software Engineering (ASE 2011), pages 633-636, Lawrence, Kan., USA, Nov 6 – 11, 2011. (Pdf, Bib, Slides)
    3. Manchun Zheng, Jun Sun, David Sanán, Yang Liu, Jin Song Dong, Yu Gu. Demo: Towards Bug-free Implementations for Wireless Sensor Networks. The 9th ACM Conference on Embedded Networked Sensor Systems (Sensys 2011), pages 407-408, Seattle, WA, USA, Nov 1 – 4, 2011. (Pdf, Bib).
    4. Yang Liu, Jun Sun and Jin Song Dong. PAT 3: An Extensible Architecture for Building Multi-domain Model Checkers. The 22nd annual International Symposium on Software Reliability Engineering (ISSRE 2011), pages 190-199, Hiroshima, Japan, Nov 29 – Dec 2, 2011. (Pdf, Bib, Slides)
    5. Shang-Wei Lin, Étienne André, Jin Song Dong, Jun Sun, and Yang Liu. Efficient Algorithm for Learning Event-Recording Automata. The 9th International Symposium on Automated Technology for Verification and Analysis (ATVA 2011), pages 463-472, Taipei, Taiwan, October 11 – 14, 2011. (Pdf, Bib, Slides)
    6. Zhenchang Xing, Jun Sun, Yang Liu and Jin Song Dong. Differencing Labeled Transition Systems. The 13th International Conference on Formal Engineering Methods (ICFEM 2011), pages 537-552, Durham, United Kingdom, October 25-28, 2011. (Pdf, Bid, Slides)
    7. Jun Sun, Yang Liu, Songzheng Song and Jin Song Dong. PRTS: An Approach for Model Checking Probabilistic Real-time Hierarchical Systems. The 13th International Conference on Formal Engineering Methods (ICFEM 2011), pages 147-162, Durham, United Kingdom, October 25-28, 2011. (Pdf, Bid, Slides)
    8. Manchun Zheng, Jun Sun, Yang Liu, Jin Song Dong and Yu Gu. Towards a Model Checker for NesC and Wireless Sensor Networks. The 13th International Conference on Formal Engineering Methods (ICFEM 2011), pages 372-387, Durham, United Kingdom, October 25-28, 2011. (Pdf, Bid, Slides)
    9. Tian Huat Tan, Yang Liu, Jun Sun and Jin Song Dong. Verification of Computation Orchestration System with Compositional Partial Order Reduction. The 13th International Conference on Formal Engineering Methods (ICFEM 2011), pages 98-114, Durham, United Kingdom, October 25-28, 2011. (Pdf, Bid, Slides)
    10. Shaojie Zhang, Jun Sun, Jun Pang, Yang Liu and Jin Song Dong. On Combining State Space Reductions with Global Fairness Assumptions. The 17th International Symposium on Formal Methods (FM 2011), pages 432 – 447, Lero, Limerick, Ireland, June 20 – 24, 2011. (Pdf, Bib, Slides)
    11. Jin Song Dong, Jun Sun and Yang Liu. Tutorial: Developing Your Own Model Checker in One Month. The 17th International Symposium on Formal Methods (FM 2011), Lero, Limerick, Ireland, June 20 – 24, 2011. (Slides)

    2010

    1. Ka Lok Man and Tomas Krilavicius. Research on Process Algebraic Analysis Tools for Electronic System Design. Intelligent Automation and Computer Engineering, Volume 52, 415 – 427, 2010.
    2. Jun Sun, Yang Liu, Jin Song Dong, Geguang Pu and Tian Huat Tan. Model-based Methods for Linking Web Service Choreography and Orchestration. The 17th Asia Pacific Software Engineering Conference (APSEC 2010), pages 166-175, Sydney, Australia, 30 November – 3 December 2010. (Pdf, Bib, Slides)
    3. Yang Liu, Jun Sun and Jin Song Dong. Analyzing Hierarchical Complex Real-time Systems. The ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE 2010), pages 365-366, Santa Fe, New Mexico, USA, 7-11 November 2010. (Pdf, Bib, Slides)
    4. Jun Sun, Yang Liu and Bin Cheng. Model Checking a Model Checker: A Code Contract Combined Approach. The 12th International Conference on Formal Engineering Methods (ICFEM 2010), pages 518-533, Shang Hai, China, 16-19 November 2010. (Pdf, Bib, Slides)
    5. Yang Liu, Jun Sun, Jin Song Dong. Developing Model Checkers Using PAT. 8th International Symposium on Automated Technology for Verification and Analysis (ATVA 2010), pages 371-377, Singapore, 2010. (Pdf, Bib)
    6. Jun Sun, Songzheng Song and Yang Liu. Model Checking Hierarchical Probabilistic Systems. The 12th International Conference on Formal Engineering Methods (ICFEM 2010), pages 388-403, Shang Hai, China, 16-19 November 2010. (Pdf, Bib, Slides)
    7. Zhenchang Xing, Jun Sun, Yang Liu and Jin Song Dong. SpecDiff: Debugging Formal Specifications. The 25th IEEE/ACM International Conference on Automated Software Engineering (ASE 2010), pages 353-354, Antwerp, Belgium, 20-24 September 2010. (Pdf, Bib, Slides)
    8. Luu Anh Tuan. Modeling and Verifying Security Protocols Using PAT Approach. The 1st International Workshop on Model Checking Secure and Reliable Systems (MoCSeRS 2010). pages 157-164, Singapore, June, 2010. (Pdf, Bib, Slides)
    9. Ling Shi and Yan Liu. Modeling and Verification of Transmission Protocols: A Case Study on CSMA/CD Protocol. The 1st International Workshop on Model Checking Secure and Reliable Systems (MoCSeRS 2010). pages 143-149, Singapore, June, 2010. (Pdf, Bib, Slides)
    10. Nguyen Truong Khanh, Quan Thanh Tho. Using Multi Decision Diagram in Model Checking. The 1st International Workshop on Model Checking Secure and Reliable Systems (MoCSeRS 2010). pages 126-129, Singapore, June, 2010. (Pdf, Bib, Slides)
    11. Man Chun Zheng. An Automatic Approach to Verify Sensor Network Systems.. The 4th IEEE International Conference on Secure Software Integration and Reliability Improvement (SSIRI 2010). pages 7-12, Singapore, June, 2010. (Pdf, Bib, Slides)
    12. Shao Jie Zhang, Yang Liu. An Automatic Approach to Model Checking UML State Machines. The 4th IEEE International Conference on Secure Software Integration and Reliability Improvement (SSIRI 2010). pages 1-6, Singapore, June, 2010. (Pdf, Bib, Slides)
    13. Songzheng Song.An Efficient Method of Probabilistic Model Checking. The 4th IEEE International Conference on Secure Software Integration and Reliability Improvement (SSIRI 2010). pages 24-25, Singapore, June, 2010. (Pdf, Bib, Slides)
    14. Tian Huat Tan. Towards Verification of a Service Orchestration Language . The 4th IEEE International Conference on Secure Software Integration and Reliability Improvement (SSIRI 2010). pages 36-37, Singapore, June, 2010. (Pdf, Bib, Slides)
    15. Huiquan Zhu. Model Checking C# Code: A Translation Approach]. The 4th IEEE International Conference on Secure Software Integration and Reliability Improvement (SSIRI 2010). pages 30-31, Singapore, June, 2010. (Pdf, Bib, Slides)
    16. Luu Anh Tuan, Man Chun Zheng, Quan Thanh Tho. Modeling and Verification of Safety Critical Systems: A Case Study on Pacemaker. The 4th IEEE International Conference on Secure Software Integration and Reliability Improvement (SSIRI 2010). pages 23-32, Singapore, June, 2010. (Pdf, Bib)
    17. Shaojie Zhang and Yang Liu. Model Checking a Lazy Concurrent List-Based Set Algorithm. The 4th IEEE International Conference on Secure Software Integration and Reliability Improvement (SSIRI 2010). pages 43-52, Singapore, June, 2010. Best Paper Awards (Pdf, Bib, Slides)
    18. Yang Liu. Model Checking Concurrent and Real-time Systems: the PAT Approach. PhD thesis, May, 2010.

    2009

    1. Man, K.L., Krilavicius, T., Leung, H.L.. Case studies with Process Analysis Toolkit (PAT). International SoC Design Conference (ISOCC), 2009.
    2. Yang Liu, Jun Sun and Jin Song Dong. Scalable Multi-Core Model Checking Fairness Enhanced Systems. 11th International Conference on Formal Engineering Methods (ICFEM 2009). pages 426-445, Rio de Janeiro, Brazil, December, 2009. (Pdf, Bib, Slides)
    3. Jun Sun, Yang Liu, Jin Song Dong and Xian Zhang. Verifying Stateful Timed CSP using Implicit Clocks and Zone Abstraction. 11th International Conference on Formal Engineering Methods (ICFEM 2009). pages 581-600, Rio de Janeiro, Brazil, December, 2009. (Pdf, Bib, Slides)
    4. Jun Sun, Yang Liu, Abhik Roychoudhury, Shanshan Liu and Jin Song Dong. Fair Model Checking with Process Counter Abstraction. The 16th International Symposium on Formal Methods (FM 2009). pages 123 – 139, Eindhoven, the Netherlands, November, 2009. (Pdf, Bib, Slides)
    5. Yang Liu, Wei Chen, Yanhong A. Liu and Jun Sun. Model Checking Lineariability via Refinement. The 16th International Symposium on Formal Methods (FM 2009). pages 321-337, Eindhoven, the Netherlands, November, 2009. (Pdf, Bib, Slides)
    6. Jun Sun, Yang Liu, Jin Song Dong and Jun Pang. PAT: Towards Flexible Verification under Fairness. The 21th International Conference on Computer Aided Verification (CAV 2009), pages 709-714, Grenoble, France, June, 2009. (Pdf, Bib, Slides).
    7. Jin Song Dong and Jun Sun. Towards Expressive Specification and Efficient Model Checking (invited tutorial). The 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2009), page 9, Tian Jing, China, July, 2009. (Pdf, Bib, Slides).
    8. Yang Liu, Jun Pang, Jun Sun and Jianhua Zhao. Verification of Population Ring Protocols in PAT. The 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2009), pages 81 – 89, Tian Jing, China, July, 2009. (Pdf, Bib, Slides) This paper presents the results of applying PAT for verifying population ring protocols. A previously unknown bug in a protocols which works under strong global fairness has been revealed.
    9. Jun Sun, Yang Liu, Jin Song Dong and Chun Qing Chen. Integrating Specification and Programs for System Modeling and Verification. The 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2009), pages 127 – 135, Tian Jing, China, July, 2009. (Pdf, Bib, Slides). This is a white paper on PAT’s specification language (named CSP#). It contains the design philosophy of CSP# and a multi-lifts case study.
    10. Shao Jie Zhang, Yang Liu, Jun Sun, Jin Song Dong, Wei Chen and Yanhong A. Liu. Formal Verification of Scalable NonZero Indicators. The 21st International Conference on Software Engineering and Knowledge Engineering (SEKE 2009), pages 406-411, Boston, Massachusetts, USA, July 1-3, 2009. (Pdf, Bib, Slides). This paper presents the results of applying PAT for verifying the newly proposed Scalable NonZero Indicators algorithm.

    2008

    1. Jun Sun, Yang Liu, Jin Song Dong and Hai H. Wang. Specifying and Verifying Event-based Fairness Enhanced Systems. The 10th International Conference on Formal Engineering Methods (ICFEM 2008), pages 318-337, Japan, October, 2008. (Pdf, Bib, Slides). This is a refereed paper on how to annotate individual events in event-based compositional processes with fairness and then perform system analysis under fairness.
    2. Jun Sun, Yang Liu and Jin Song Dong. Model Checking CSP Revisited: Introducing a Process Analysis Toolkit. The Third International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2008), pages 307-322, Porto Sani, Greece, October 13-15, 2008. (Pdf, Bib). This is a refereed paper on applying partial order reduction to CSP based system verification through refinement checking.
    3. Jun Sun, Yang Liu, Jin Song Dong and Jing Sun. Bounded Model Checking of Compositional Processes. The 2nd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2008), pages 23-30, Nanjing, China, June 17-19, 2008. (Pdf, Bib). This is a refereed paper on the bounded model checker implemented in PAT. Notice that due to various reasons (mainly lack of human power), this component has been suspected indefinitely. Note that the experimental results presented in this paper on FDR can be improved significantly with a slightly different modeling.
    4. Yang Liu, Jun Sun and Jin Song Dong. An Analyzer for Extended Compositional Processes. ICSE Companion, pages 919-920, Leipzig, Germany, 2008. (Pdf, Bib). This is an informal tool paper presented at 30th International Conference on Software Engineering 2008 (ICSE 2008) to demonstrate a very primitive version of PAT.

N-PAT: A Nested Model Checker


N-PAT implements a novel concept of nested model checking where a model may contain placeholders to be instantiated by the verification results of sub-models.

Download and documentation.

Conference Paper. Preprint. BibTex.

Contact us

contact@depintel.com