セミナー

形式手法に関するセミナーを開催しています．

詳細につきましてはセミナーのページをご覧ください．

SyncStitch: A Model Checker based on the Process Algebra CSP

SyncStitch is a model checker based on the process algebra CSP (Communicating Sequential Processes). By using SyncStitch, you can check six types of properties of the system you are developping:

• Deadlocks
• Divergences (also known as livelocks)
• Refinement relation on traces semantics (safety)
• Refinement relation on stable failures semantics (safety and liveness)
• LTL (Linear-Time Logic) with fluents and enabledness
• CTL (Computation-Tree Logic) with fluents and enabledness. In addition, three types of fairness assumptions (unconditional, strong, and weak) can be specified.

The behaviour of the system and the result of checking (violation or witness) can be shown as a computation tree and analyzed interactively.

News