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.
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.
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).
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.
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#.