= 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''' || [http://www.mdd4soa.eu/ UML Transformer to BPEL/WSDL] || Transformer for converting UML4SOA activity diagrams into BPEL/WSDL || EMF XMI of UML model || BPEL/WSDL|| LMU: Philip Mayer || [http://www.mdd4soa.eu/ UML Transformer to Java] || Transformer for converting UML4SOA activity diagrams into Java || EMF XMI of UML model || Java || LMU: Philip Mayer || [http://www.mdd4soa.eu/ UML Transformer to Jolie] || Transformer for converting UML4SOA activity diagrams into Jolie || EMF XMI of UML model || Jolie|| LMU: Philip Mayer || [http://www.mdd4soa.eu/ 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 || [http://www.mdd4soa.eu/ 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 name'''||'''Description of Functionality '''||'''Input kind '''||'''Output Translations / Visualization'''||'''Contacts''' || [http://www.doc.ic.ac.uk/ltsa/eclipse/wsengineer 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 || [http://www.doc.ic.ac.uk/ltsa/eclipse/wsengineer 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 || [http://www.doc.ic.ac.uk/ltsa/sensoria/tutorials/bpelmsctrace.html 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 || [http://www.doc.ic.ac.uk/ltsa/sensoria/ 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 || [http://www.doc.ic.ac.uk/ltsa/sensoria/ 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''' || [http://homepages.inf.ed.ac.uk/mtribast/ 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 || [http://homepages.inf.ed.ac.uk/mtribast/ 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''' || [http://viatra.inf.mit.bme.hu/update/R2 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 || [http://viatra.inf.mit.bme.hu/update/Sensoria 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 || [http://viatra.inf.mit.bme.hu/update/Sensoria 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''' || [http://fmt.isti.cnr.it/cmc 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 || [http://fmt.isti.cnr.it/umc/ 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''' || [http://www.imm.dtu.dk/English/Research/Language-Based_Technology/Software/LySaTool.aspx 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 || [http://www.imm.dtu.dk/English/Research/Language-Based_Technology/Software/LySaTool.aspx 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 || [http://www.imm.dtu.dk/English/Research/Language-Based_Technology/Software/LySaTool.aspx 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''' ||[http://www.pst.ifi.lmu.de/projekte/hugo 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 ||[http://www.spinroot.com 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 ||[http://www.uppaal.com 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.