VERification of models for distributed communicating COmponants, with safety and Security
We are building a tool platform for the analysis and verification of safety and security properties of distributed applications. The central component of the platform is a method for generating finite models for distributed applications, for a set of (model driven) graphical editors.
We base the generation procedure on the strong semantic features provided by the GCM component model, and we generate compositional models using synchronised labelled transition systems. Various tools for static analysis, model checking, and equivalence checking can then operate on these models. One long term goal of this work is to integrate the various techniques and tools involved in this software platform, so that the platform can be integrated in a development environment, and used by non-specialists.
Download and installation instructions here: VerCors-V4 download page.