Name	Research Group or Company	Brief Description	Services
Verinec (Verified Network Configuration)	TNS group at the university of Fribourg (Switzerland) Dominik Jungo, David Buchmann, Ulrich Ultes-Nitsche	The Verinec project aims to simplify network configuration. It is based upon an abstract definition of a network and the devices in that network. Network simulation is used to test correctness of the configuration with respect to the requirements for the network.	Modelling? Yes Simulation? Yes Verification? Yes Testing? No Other? apply configuration to devices.
FBT (FIL to Büchi automaton Translator)	Research group GEDES (Grupo de Especificación, Desarrollo y Evolución del Software) - Dept. of Lenguajes y Sistemas Informáticos (University of Granada, Spain)	This tool converts a FIL (Future Interval Logic) formula to a generalised Büchi automaton, which may be used, for instance, in model checking, where it represents the property to be verified.	Modelling? Yes Simulation? No Verification? Yes Testing? No Other? --
CADP (Construction and Analysis of Distributed Processes)	INRIA Rhone-Alpes / VASY project team (Grenoble, France)	CADP is a toolbox for the design of communication protocols and distributed systems. It offers a complete range of functionalities assisting the user throughout the design process: compilation and rapid prototyping, interactive and guided simulation, random execution, model checking, equivalence checking, and test case generation.	Modelling? Yes Simulation? Yes Verification? Yes Testing? Yes Other? Performance evaluation.
VeriProc	Vrije Universiteit Amsterdam (the Netherlands)	The tool is dedicated for automated verification of the correctness of a process-oriented specification with respect to a set of constraints. A constraint is a formula expressed over a process-oriented language based on order-sorted predicate logic. The language allows expressing all commonly used workflow templates, numerical temporal relations, and different resource-related aspects.	Modelling? No Simulation? No Verification? Yes Testing? No Other? No
mCRL 2 toolset	LaQuSo (Laboratory for Quality Software - U. of Eindhoven and Radboud U. Nijmegen - The Netherlands)	mCRL 2 is a toolset based on a process algebraic language.	Modelling? Yes Simulation? Yes Verification? Yes Testing? No Other? Validation.
Yasper + Woflan	LaQuSo (Laboratory for Quality Software - U. of Eindhoven and Radboud U. Nijmegen - The Netherlands)	Yasper is a Petri net editor and Woflan a tool for their verification.	Modelling? Yes Simulation? Yes Verification? Yes Testing? No Other? Performance analysis and validation.