language syntax classes

The language syntax classes in CSP module naturally form a COMPOSITE pattern by following the language grammar. Each language construct (e.g., parallel composition, sequential compositions, choice process and so on) is implemented as a single class, which implements the Process interface with two key methods: MoveOneStep and EncodeProcess. These two methods implement the semantics of the language syntax for the two different model checking approaches. MoveOneStep method follows the operational semantic rules to realize the state transitions from current state to a list of target states. EncodeProcess performs the encoding of the syntax to Boolean formulae that can be used by the symbolic model checker or SAT solvers.

CSPState class

The most important class to be implemented is the CSPState class, which realizes the concrete transitions of the LTS. For CSP#, each system state contains the current valuation of variables, buffered elements in the channels and current active process. This composition is exactly implemented in the Class Diagram. The MoveOneStep method (or EncodeState method) in CSPState class will invoke the MoveOneStep (or EncodeProcess) method of the current active process by providing current variable valuation and channel buffer data. This guarantees that LTS is generated by following the operational semantics. At this point, modeling layer is completed.

Abstraction and Reduction Techniques

Most of the abstraction and reduction techniques are highly language dependent. For example, different timed related operators in real-time systems shall update the zones in different ways. Partial order reduction strategies require information about processes, global variables, dependencies of transitions, control-flow of processes, etc. This restriction makes the abstraction layer hardly fully independent from modeling layer. Most of the abstraction and reduction techniques are embedded inside method MoveOneStep or EncodeState to produce a reduced state space. In PAT, we demonstrate these techniques by code samples and libraries so that our experiences can be reused.