COSTO Plugins description

Current state


  • Graphs Generator: COSTOLIB_PLUGIN_UI_GRAPH


  • Kml2Latex : COSTOLIB_PLUGIN_KML2LATEX release 2.0 Kml2Latex – Generate a LaTeX documentaion of the specification
  • Kml2Html : todo Kml2Html – Generate a HTML documentaion of the specification

Formal Analysis

  • Kml2Mec: COSTOLIB_PLUGIN_KML2MEC release 2.1 Kml2Mec – Generate a MEC specification for a triple of service interaction
  • MecLoader: COSTOLIB_PLUGIN_MECLOADER release 1.1 MecLoader – Get a visual view of the Mec analysis
  • Kml2Lotos: todo Kml2Lotos
  • Kml2B and EventB: COSTOLIB_PLUGIN_KML2B release 1.0 Kml2B – Generate B specifications to check the data part (data and service assertions)

Execution and tests

  • Framework Java: (COSTO_JAVA_FRAMEWORK) library costo.kml2java.jar to include in the specification project libs directory KmlJavaFramework
  • Framework Java Animation: (COSTO_JAVA_MONITOR) library costo.kml2java.monitor.jar to include in the specification project libs directory KmlJavaMonitor
  • Kml2Java : COSTOLIB_PLUGIN_KML2JAVA release 1.1 Kml2Java – generate a Java application from the specification
    – requires javamappings for the Kmelia functions
  • KmlTest : COSTOLIB_PLUGIN_KML_TEST release 0.9 KmlTest – a set of actions and functions to generate a test application from the specification
  • MutantsGenerator : todo KmlTest


On our former website, additional details can be found:

  • Plugins Pages here

A Platform to Specify and Verify Component and Service Software

Quick Contact ^
We want to thank you for contacting us through our website and let you know we have received your information. A member of our team will be promptly respond back to you.