wiki:IntegratedTools

Update sites for Integrated Tools

Completed Tools (integrated tools)

1. MDD4SOA Transformations & Analysis

 http://www.mdd4soa.eu/update  http://www.sensoria-ist.eu/cirquent/eclipse_plugin_update/

More information on  http://www.mdd4soa.eu/

License: Eclipse Public License EPL ( http://www.eclipse.org/legal/epl-v10.html)

This update site contains:

Tool nameDescription of Functionality Input kind Output Translations / VisualizationContacts
 UML Transformer to BPEL/WSDL Transformer for converting UML4SOA activity diagrams into BPEL/WSDL EMF XMI of UML model BPEL/WSDL LMU: Philip Mayer
 UML Transformer to Java Transformer for converting UML4SOA activity diagrams into Java EMF XMI of UML model Java LMU: Philip Mayer
 UML Transformer to Jolie Transformer for converting UML4SOA activity diagrams into Jolie EMF XMI of UML model Jolie LMU: Philip Mayer
 Active-BPEL/WSDL Transformers Transformer for converting BPEL/WSDL to executable BPEL/WSDL and deployment BPEL/WSDL (result of UML transformer) BPEL/WSDL Cirquent: Rong Xie
 UML Analysis Analysis for verifying that an orchestration conforms to its protocol EMF XMI of UML model Violation Trace LMU: Andreas Schroeder

2. LTSA / WS-Engineer / Dino Service Broker

Update Site:  http://www.doc.ic.ac.uk/ltsa/eclipse

Further info:  http://www.doc.ic.ac.uk/ltsa/sensoria

 http://www.cs.ucl.ac.uk/research/dino/

License: BSD ( http://www.opensource.org/licenses/bsd-license.php)

This update site contains:

Tool nameDescription of Functionality Input kind Output Translations / VisualizationContacts
 Dino Runtime Console SDE Plug-in Runtime console and SDE APIOWL-S/QoS SpecificationsMatchmaking and Adaptive CompositionLSS-ICL:Howard Foster,LSS-UCL:Arun Mukhija
 Modes Parser and Browser / SDE Plug-ins WS-Engineer plug-ins to parse and extract broker requirements from UML2 Modes Models.UML2+Modes ProfileOWL-S/QoS SpecificationsLSS-ICL:Howard Foster
 WS-Engineer Tutorial (extensions for Demonstrator) Enhanced WS-Engineer below to include mechanism to demonstrate BPEL-FSP-MSC traces (scriptable).BPEL4WS 1.x, WS-CDL 1.xFSP/Traces/MSCsLSS-ICL:Howard Foster
 WS-Engineer The LTSA WS-Engineer plug-in is an extension to the LTSA Eclipse Plug-in which allows service models to be described by translation of the service process descriptions, and can be used to perform model-based verification of web service compositions.BPEL4WS 1.x,WS-CDL 1.xFSP/Traces/MSCsLSS-ICL:Howard Foster
 LTSA LTSA is a verification tool for concurrent systems. It mechanically checks that the specification of a concurrent system satisfies the properties required of its behaviour. In addition, LTSA supports specification animation to facilitate interactive exploration of system behaviour.FSPState Machine/LTS/TracesLSS-ICL:Howard Foster

3. SRMC - Sensoria Reference Markovian Calculus

Update site:  http://homepages.inf.ed.ac.uk/mtribast/update/site.xml

Installation help (Batik etc):  http://groups.inf.ed.ac.uk/srmc/download.html

License: BSD ( http://www.opensource.org/licenses/bsd-license.php)

This update site contains:

Tool nameDescription of Functionality Input kind Output Translations / VisualizationContacts
 SRMC Core SRMC Core provides support for SRMC, an extension to PEPA. It covers steady-state analysis of the underlying Markov chain of SRMC descriptions. SRMC file Markov Chain/Performance? Results (throughput, utilisation) UEDIN: Mirco Tribastone
 SRMC/UML Bridge SRMC/UML offers facilities for meta-model transformation. It translates a subset of UML2 models (Interactions and State Machines) into an SRMC description for performance evaulation. Results are reflected back into the UML model. UML2 model (Eclipse EMF-based implementation) SRMC Model / back-annotated UML model UEDIN: Mirco Tribastone

4. VIATRA2 - VIATRA2 and deplyoment transformations

 http://viatra.inf.mit.bme.hu/update/R2

 http://viatra.inf.mit.bme.hu/update/Sensoria

License: Eclipse Public License EPL ( http://www.eclipse.org/legal/epl-v10.html)

This update site contains:

Tool nameDescription of Functionality Input kind Output Translations / VisualizationContacts
 VIATRA2 VIsual Automated model TRAnsformations) framework. A typical application scenario is to transform high-level abstract models (e.g. UML) to models of some analysis domain (e.g. SPIN, Petri nets, etc.). It can help to build bridges between Sensoria} tools. In addition, the included vUtil component provides useful functions for Sensoria scripts (such as workspace-based file handling, XML formatting). Textual representation of a model (typically in XML/XMI); importers include the Rational UML family, BPEL, etc. Arbitrary textual representation of a target model (e.g. PNML, Promela, Java, other textual descriptions) BUTE: Daniel Varro, Istvan Rath
 SOA2WSDL transformation The SOA2WSDL transformation takes high level UML2forSOA models and produces WSDL (Web Services Description language) output. UML2forSOA models (Eclipse EMF-based implementation) WSDL files BUTE: Laszlo Gonczy
 UML2Axis deployment transformations The UML2Axis transformations take high level UML4OA models and produce WSDL (Web Services Description language), Ws-ReliableMessaging?, Ws-Security and Apache Axis-specific configuration files as output. UML4SOA models (in EMF, extended with non-functional paramaters) Configuration files BUTE: Laszlo Gonczy

5. CMC - UMC UCTL/Socl model checkers, and analysers

Eclipse plugin, Eclipse SENSORIA SDE plugin:  http://fmt.isti.cnr.it/umc/UMCDISTR/Eclipsetools/it.cnr.isti.eclipsetools.update

Direct online access:  http://fmt.isti.cnr.it/umc/  http://fmt.isti.cnr.it/cmc/

Standalone executables for Windows,Linux,MacOS,SunOS:  http://fmt.isti.cnr.it/umc/UMCDISTR/Binaries/  http://fmt.isti.cnr.it/cmc/CMCDISTR/Binaries/

License: GNU General Public License (GPL) ( http://www.gnu.org/licenses/gpl-3.0.txt)

This update site contains:

Tool nameDescription of Functionality Input kind Output Translations / VisualizationContacts
 CMC Model checker and analyser for systems defined by interacting UML statecharts. Allows to model-check on the fly abstract behavioral properties in the Socl braching-time state-action based, parametric temporal logic (all versions). Allows to explore the model evolution (all versions but SENSORIA SDE plugin). Allows to generate abstract full-trace minimized graphs of the system (only the online versions) Textual representation of a model (COWS process algebra) Dot / JPEG graphical format of minimized model ISTI: Franco Mazzanti
 UMC Model checker and analyser for systems defined by interacting UML statecharts. Allows to model-check on the fly abstract behavioral properties in the Socl braching-time state-action based, parametric temporal logic (all versions). Allows to explore the model evolution (all versions but SENSORIA SDE plugin). Allows to generate abstract full-trace minimized graphs of the system (only the online versions) Textual UML statacharts descriptions (umc format) Dot / JPEG graphical format of minimized model ISTI: Franco Mazzanti

6. LYSA Tool - static protocol analyzer

 http://www.imm.dtu.dk/English/Research/Language-Based_Technology/Software/LySaTool.aspx

As of yet, supported only on Windows!

Eclipse plugin, Eclipse SENSORIA SDE plugin:  http://lbt.imm.dtu.dk/Sensoria/update

Required standalone executable for Windows:  http://lbt.imm.dtu.dk/Sensoria/update/lysatool.exe

License: Copyright University of Denmark.

This update site contains:

Tool nameDescription of Functionality Input kind Output Translations / VisualizationContacts
 LYSA Tool Static analyzer for security protocols defined in the LYSA process calculus. Provides a prototype LYSA editor to assist users in the modeling of protocols. Given a LYSA model the analyzer will verify properties related to secrecy and authentication. Textual representation of a model (Protocols modelled in the process calculus LySa?) HTML representation of the analysis result. DTU: Henrik Pilegaard
 ConfiLySaTool Static analyzer for security protocols defined in the LYSA process calculus. Provides a prototype LYSA editor to assist users in the modeling of protocols. Given a LYSA model the analyzer will verify properties related to secrecy and authentication. Textual representation of a model (Protocols modelled in the process calculus LySa?) HTML representation of the analysis result. DTU: Henrik Pilegaard
 TypeLySaTool Static analyzer for security protocols defined in the LYSA process calculus. Provides a prototype LYSA editor to assist users in the modeling of protocols. Given a LYSA model the analyzer will verify properties related to secrecy and authentication. Textual representation of a model (Protocols modelled in the process calculus LySa?) HTML representation of the analysis result. DTU: Henrik Pilegaard

7. Hugo/RT Update Site

 http://svn.pst.ifi.lmu.de/update/tools

License: (not yet determined)

This update site contains:

Tool nameDescription of Functionality Input kind Output Translations / VisualizationContacts
 Hugo/RTTemporal logics verification (Timed CTL, LTL); UML 2.0 interaction verificationUML state machines, collaborations, interactions - XMI 1.0, 1.1, 1.2; plain text in UTE formatUPPAAL, Spin, KIV, Java, SystemC, dot graphsLMU: Alexander Knapp
 SPINSpin is a popular open-source software tool, used by thousands of people worldwide, that can be used for the formal verification of distributed software systemsPromela LTL model and QueryTraceLMU:Philip Mayer
 UPPAAALUppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.).Timed AutomataTraceLMU:Philip Mayer

Note: For SPIN and UPPAAL to work, you need to deploy two Web services. See SpinAndUppaalWebServices.