| | 1 | = Update sites for Sensoria Tools = |
| | 2 | |
| | 3 | == Completed Tools (integrated tools) == |
| | 4 | |
| | 5 | == 1. MDD4SOA Transformations & Analysis == |
| | 6 | |
| | 7 | http://www.mdd4soa.eu/update |
| | 8 | http://www.sensoria-ist.eu/cirquent/eclipse_plugin_update/ |
| | 9 | |
| | 10 | More information on http://www.mdd4soa.eu/ |
| | 11 | |
| | 12 | '''License:''' Eclipse Public License EPL (http://www.eclipse.org/legal/epl-v10.html) |
| | 13 | |
| | 14 | This update site contains: |
| | 15 | |
| | 16 | ||'''Tool name'''||'''Description of Functionality '''||'''Input kind '''||'''Output Translations / Visualization'''||'''Contacts''' |
| | 17 | || [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 |
| | 18 | || [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 |
| | 19 | || [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 |
| | 20 | || [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 |
| | 21 | || [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 |
| | 22 | |
| | 23 | == 2. LTSA / WS-Engineer / Dino Service Broker == |
| | 24 | |
| | 25 | Update Site: http://www.doc.ic.ac.uk/ltsa/eclipse |
| | 26 | |
| | 27 | Further info: http://www.doc.ic.ac.uk/ltsa/sensoria |
| | 28 | http://www.cs.ucl.ac.uk/research/dino/ |
| | 29 | |
| | 30 | '''License:''' BSD (http://www.opensource.org/licenses/bsd-license.php) |
| | 31 | |
| | 32 | This update site contains: |
| | 33 | |
| | 34 | ||'''Tool name'''||'''Description of Functionality '''||'''Input kind '''||'''Output Translations / Visualization'''||'''Contacts''' |
| | 35 | || [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 |
| | 36 | || [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 |
| | 37 | || [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 |
| | 38 | || [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 |
| | 39 | || [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 |
| | 40 | |
| | 41 | == 3. SRMC - Sensoria Reference Markovian Calculus == |
| | 42 | |
| | 43 | Update site: http://homepages.inf.ed.ac.uk/mtribast/update/site.xml |
| | 44 | |
| | 45 | Installation help (Batik etc): http://groups.inf.ed.ac.uk/srmc/download.html |
| | 46 | |
| | 47 | '''License:''' BSD (http://www.opensource.org/licenses/bsd-license.php) |
| | 48 | |
| | 49 | This update site contains: |
| | 50 | |
| | 51 | ||'''Tool name'''||'''Description of Functionality '''||'''Input kind '''||'''Output Translations / Visualization'''||'''Contacts''' |
| | 52 | || [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 |
| | 53 | || [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 |
| | 54 | |
| | 55 | |
| | 56 | == 4. VIATRA2 - VIATRA2 and deplyoment transformations == |
| | 57 | |
| | 58 | http://viatra.inf.mit.bme.hu/update/R2 |
| | 59 | |
| | 60 | http://viatra.inf.mit.bme.hu/update/Sensoria |
| | 61 | |
| | 62 | '''License:''' Eclipse Public License EPL (http://www.eclipse.org/legal/epl-v10.html) |
| | 63 | |
| | 64 | This update site contains: |
| | 65 | |
| | 66 | ||'''Tool name'''||'''Description of Functionality '''||'''Input kind '''||'''Output Translations / Visualization'''||'''Contacts''' |
| | 67 | || [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 |
| | 68 | || [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 |
| | 69 | || [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 |
| | 70 | |
| | 71 | == 5. CMC - UMC UCTL/Socl model checkers, and analysers == |
| | 72 | |
| | 73 | Eclipse plugin, Eclipse SENSORIA SDE plugin: http://fmt.isti.cnr.it/umc/UMCDISTR/Eclipsetools/it.cnr.isti.eclipsetools.update |
| | 74 | |
| | 75 | Direct online access: http://fmt.isti.cnr.it/umc/ http://fmt.isti.cnr.it/cmc/ |
| | 76 | |
| | 77 | Standalone executables for Windows,Linux,MacOS,SunOS: http://fmt.isti.cnr.it/umc/UMCDISTR/Binaries/ http://fmt.isti.cnr.it/cmc/CMCDISTR/Binaries/ |
| | 78 | |
| | 79 | '''License:''' GNU General Public License (GPL) (http://www.gnu.org/licenses/gpl-3.0.txt) |
| | 80 | |
| | 81 | This update site contains: |
| | 82 | |
| | 83 | ||'''Tool name'''||'''Description of Functionality '''||'''Input kind '''||'''Output Translations / Visualization'''||'''Contacts''' |
| | 84 | || [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 |
| | 85 | || [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 |
| | 86 | |
| | 87 | == 6. LYSA Tool - static protocol analyzer == |
| | 88 | |
| | 89 | http://www.imm.dtu.dk/English/Research/Language-Based_Technology/Software/LySaTool.aspx |
| | 90 | |
| | 91 | As of yet, supported only on Windows! |
| | 92 | |
| | 93 | Eclipse plugin, Eclipse SENSORIA SDE plugin: http://lbt.imm.dtu.dk/Sensoria/update |
| | 94 | |
| | 95 | Required standalone executable for Windows: http://lbt.imm.dtu.dk/Sensoria/update/lysatool.exe |
| | 96 | |
| | 97 | '''License:''' Copyright University of Denmark. |
| | 98 | |
| | 99 | This update site contains: |
| | 100 | |
| | 101 | ||'''Tool name'''||'''Description of Functionality '''||'''Input kind '''||'''Output Translations / Visualization'''||'''Contacts''' |
| | 102 | || [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 |
| | 103 | || [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 |
| | 104 | || [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 |
| | 105 | |
| | 106 | == 7. Hugo/RT Update Site == |
| | 107 | |
| | 108 | http://svn.pst.ifi.lmu.de/update/tools |
| | 109 | |
| | 110 | '''License:''' (not yet determined) |
| | 111 | |
| | 112 | This update site contains: |
| | 113 | |
| | 114 | ||'''Tool name'''||'''Description of Functionality '''||'''Input kind '''||'''Output Translations / Visualization'''||'''Contacts''' |
| | 115 | ||[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 |
| | 116 | ||[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 |
| | 117 | ||[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 |
| | 118 | |
| | 119 | '''Note:''' For SPIN and UPPAAL to work, you need to deploy two Web services. See SpinAndUppaalWebServices. |
