Concurrency Workbench NC

Automatic verification of concurrent software systems

Brought to you by: cschulze1984

Downloads: 3 This Week

Last Update: 2016-07-23

Get an email when there's a new version of Concurrency Workbench NC

The Concurrency Workbench of the New Century (CWB-NC) provides support for the automated verification of concurrent software systems. The tool allows the user to write a description of the system at hand in one of several design languages (CCS, CSP, LOTOS, PCCS, SCCS, TCCS). Furthermore it supports a variety of automated verification and analysis techniques to check whether the system adheres to its specifications.

Among the verification and analysis techniques are:
- Behavioral-Relation-Based Verification
- Temporal-Logic-Based Verification
- Interactive Simulation
- Reachability analysis

Project Activity

See All Activity >

Follow Concurrency Workbench NC

Concurrency Workbench NC Web Site

Other Useful Business Software

MongoDB Atlas runs apps anywhere Icon

MongoDB Atlas runs apps anywhere

Deploy in 115+ regions with the modern database for every enterprise.

MongoDB Atlas gives you the freedom to build and run modern applications anywhere—across AWS, Azure, and Google Cloud. With global availability in over 115 regions, Atlas lets you deploy close to your users, meet compliance needs, and scale with confidence across any geography.

Start Free

Rate This Project

Login To Rate This Project

User Reviews

Be the first to post a review of Concurrency Workbench NC!

Additional Project Details

Registered

2013-03-10

Report inappropriate content

Recommended Projects

The PEP tool
PEP is a modelling and verification framework for parallel systems, providing a large number of different modelling languages and verification techniques (e.g. SDL, Petri nets and model checking)
Syspect
Syspect is a tool to specify a system using UML2 diagramms and translate them into a CSP-OZ-DC specification for formal verification.
Temporal Inference Engine
A real time inference engine for temporal logical specifications, which is able to acquire, process and generate any binary or real signal through POSIX IPC, files or UNIX sockets. Specifications of signals and dynamic systems are represented as special graphs and executed in real time, with a...
JBernstein
JBernstein is a tool implemented in Java that enables to check whether a polynomial constraint holds for all variables within their domain. It is mainly used in the verification or synthesis of cyber-physical systems where the system model is nonlinear. The tool also supports specifications in...
LazySets.jl
LazySets.jl is a Julia package for calculus with convex sets. The aim is to provide a scalable library for solving complex set-based problems, such as those encountered in differential inclusions or reachability analysis techniques in the domain of formal verification. Typically, one is...