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.

Coloane

Coloane is a generic graph editor and a front-end of FrameKit. 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 ;-).

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.

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.

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.

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.

BCC (Behavioral Consistency Checker)

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

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.
It is now a part of the gentoo-linux package, available here.