BUT4Reuse (in cooperation with the University of Luxembourg)

BUT4Reuse is a framework that provides technologies for leveraging commonality and variability of software artefacts. Use it for analysing commonality and variability, feature identification, feature location, structural and semantic constraints discovery or for reusable assets construction.

CosyVerif

CosyVerif is a Verification environment jointly developed by LIP6 (UPMC), LIPN (Univ. Paris 13) and LSV (ENS de cachan). It is composed of an integration platform gathering verification tools based on Petri Nets and various kind of automatas.

libDDD

libDDD is a package for manipulation of Data Decision Diagrams and Hierarchical Set Decision Diagrams. It supports flexible data types and "saturation" algorithms to offer cutting edge performances using decision diagrams. It is a C++ package distributed under Gnu LGPL.

PNML Framework

PNML Framework is a prototype implementation of ISO/IEC-15909 part 2, International Standard on Petri Net Markup Language. The primary purpose of PNML is to enable interoperability among Petri net tools. PNML framework has thus been designed to back the Standard. It will enable Petri nets tools developers to seamlessly integrate PNML support into their tools. It provides an extensive and comprehensible API to create, save, load and browse PNML models.

Puck

Puck is an architecture refatoring tool for Java software, which allows developpers to detect and remove unwanted dependencies from code.They can plan their refactorings on dependency graphs and then apply their plans to code automatically. Puck is still at a prototyping stage.

Spot (in cooperation with LRDE)

Spot is an object-oriented model checking library written in C++. It offers a set of bricks to experiment with and develop your own model checker. The library uses a special kind of automata called Transition-based Generalized Büchi Automata (TGBA). These are OmegaAutomata with labels on transitions, and multiple acceptance sets of transitions. Compared to more traditional Büchi Automata with acceptance sets of states, TGBA allow LtlFormulae to be represented more concisely. SPOT was orginally created at LIP6 and is now co-developped between LIP6 and LDRE.

ITS tools

ITS tools are a suite of command-line model-checking tools supporting safety, CTL and LTL model-checking for a wide range of formalisms conforming to the Instantiable Transition System framework. LTL model-checking is built using an interaction with SPOT. The ITS tools are supported by native encodings of states and operations using libDDD, thus supporting very large transition systems. The Guarded Action Language (GAL) is provided as a universal way to express semantics of concurrent systems for ITS tools independently from any given high-level formalism. These C++ tools are distributed is distributed under Gnu GPL.

ITS modeler

ITS modeler is a set of Eclipse plugins providing a user friendly front-end to the ITS tools and a rich graphical and textual modeling environment. Using model transformations with GAL as a target, ITS modeler currently offers support for models expressed in DVE the language of DiViNe, Spin's Promela formalism, Uppaal's XTA timed automata format, time Petri nets (with graphical editor and import/export to Tina and Romeo tools), and high level Petri nets expressed in PNML standard format. Of course ITS modeler also offers support to model directly using GAL and ITS, the native formalisms of ITS tools. These plugins are distributed through a standard Eclipse update site under EPL license, and embed a distribution of ITS-tools.

VerChor

VerChor is a framework for the development of correct distributed systems following the choreography-based approach. VerChor architecture is centered around a pivot model (CIF) together with front-ends to transform standard languages into the pivot model and back-ends to transform the pivot model into formal languages, thus enabling formal support. VerChor enables for example one to check for the realizability of a choreography specification, to generate behavioral peer skeletons from a choreography specification, and to generate behavioral controllers for a set of peers to be reused. In its current version VerChor integrates with the Eclipse BPMN 2.0 modeler to let the designer use this ISO standard notation for specifying choreographies and then perform formal analyses directly from the Eclipse IDE (through the use of a BPMN-to-CIF front-end and a CIF-to-LNT back end).

Past software (still available but maintained elsewhere)

PolyORB (in cooperation with TELECOM ParisTech)

PolyORB (see here or here) is a middleware that aims at providing a uniform solution to build distributed applications; relying either on industrial-strength middleware standards such as CORBA, the Distributed System Annex of Ada 95, distribution programming paradigms such as Web Services, Message Oriented Middleware (MOM), or to implement application-specific middleware. It is based on an original architecture design called "Schizophrenic" because it allows to host in the same machine several middlewares API (personnalities) sharing the same middleware kernel. For several years, maintenance has been taken over by Ada-Core. The product version is available here.

Past software (still available but not maintained any more)

BCC (Behavioral Consistency Checker)

BCC is a model checking based tool to check consistency of UML diagrams. It is developed within the ModelPlex project.

Coloane

Coloane is a generic graph editor and a front-end of CosyVerif. It is an Eclipse plug-in and thus, works on the major execution environments supported by Eclipse. So, it can be considered as an alternative solution to the Macao user interface for non Macintosh users ;-).

CPN-AMI

CPN-AMI is a Petri Net based CASE environment. It offers a set of services to perform specification, validation, formal verification, model checking, compute structural properties (invariants, traps, syphons etc.) simulate and generate code. These services have been implemented either by members of our team or university partners (Technical university of Helsinki, University of Torino, Technical university of Munchen, Bell laboratories).

Since march 1997, CPN-AMI is built on top of FrameKit.

FrameKit

FrameKit is a software platform dedicated to the prototyping and fast implementation of CASE environments. FrameKit is valuable to quickly implement a CASE environment, either for evaluation purposes or as a final product, especially if graphical representations are involved. It is a small generic CASE environment that can be customized with specific information to produce dedicated CASE environements for various purpose. CPN-AMI is an example.

Macao

Macao is a generic graph drawing software that lets you create and manipulate graphs quickly and easily. When using CPN-AMI or the Framekit environment, Macao provides you with a user interface for accessing tools developed on Linux and MacOS X. Macao itself runs only on MacOS X.

MetaScribe

MetaScribe is a generator of transformation engine that facilitates the construction of automatic program generators. The transformation is handled from the source formalism, a semantic pattern that specifies the transformations to do on an input model to produce another one that belongs to the target formalism, and a syntactic pattern that defines the syntactic sugar to apply on the result of the semantic pattern. An experimental version of MetaScribe is available on demand.