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 name | Description of Functionality | Input kind | Output Translations / Visualization | Contacts |
| 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
License: BSD ( http://www.opensource.org/licenses/bsd-license.php)
This update site contains:
| Tool name | Description of Functionality | Input kind | Output Translations / Visualization | Contacts |
| Dino Runtime Console SDE Plug-in | Runtime console and SDE API | OWL-S/QoS Specifications | Matchmaking and Adaptive Composition | LSS-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 Profile | OWL-S/QoS Specifications | LSS-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.x | FSP/Traces/MSCs | LSS-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.x | FSP/Traces/MSCs | LSS-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. | FSP | State Machine/LTS/Traces | LSS-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 name | Description of Functionality | Input kind | Output Translations / Visualization | Contacts |
| 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 name | Description of Functionality | Input kind | Output Translations / Visualization | Contacts |
| 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 name | Description of Functionality | Input kind | Output Translations / Visualization | Contacts |
| 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 name | Description of Functionality | Input kind | Output Translations / Visualization | Contacts |
| 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 name | Description of Functionality | Input kind | Output Translations / Visualization | Contacts |
| Hugo/RT | Temporal logics verification (Timed CTL, LTL); UML 2.0 interaction verification | UML state machines, collaborations, interactions - XMI 1.0, 1.1, 1.2; plain text in UTE format | UPPAAL, Spin, KIV, Java, SystemC, dot graphs | LMU: Alexander Knapp |
| SPIN | Spin is a popular open-source software tool, used by thousands of people worldwide, that can be used for the formal verification of distributed software systems | Promela LTL model and Query | Trace | LMU:Philip Mayer |
| UPPAAAL | Uppaal 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 Automata | Trace | LMU:Philip Mayer |
Note: For SPIN and UPPAAL to work, you need to deploy two Web services. See SpinAndUppaalWebServices.
