Experiments and Evaluation of Sensoria
- The EU Project Sensoria developed the Sensoria Development environment (SDE), which is now renamed to Service Development Environmment. It is based on Eclipse and available at http://svn.pst.ifi.lmu.de/trac/sde
- Installation: The actual installation requires Eclipse Modelling Tools Version (Eclipse version >= 3.4, I used indigo 3.7), then the installation via the update site works. Then I followed the instructions given in the tutorial. However, I could not install the tools below (e.g. SRML Editor), so went back to the installation from the update site, and first installed from the Eclipse update site all packages that have GEF and GMF in their name (as required in the tutorial). Then I also added the openArchitectureWare (site, installing the "SDK feature" item, not classic SDK). For this step you will need to have the "UML2 Tools SDK" installed. Then I could install the SRML Editor.
- General information abotu SDE and its goals are in the trac at http://svn.pst.ifi.lmu.de/trac/sde
There are a number of tools that can be used in SDE available at http://svn.pst.ifi.lmu.de/trac/sde/wiki/RelatedTools. Interesting for us could be:
- LTSA/DINO: The Eclipse Update site indicated on the webpages below is wrong; the correct URL is http://www.doc.ic.ac.uk/ltsa/eclipse/install.
- DINO: Runtime console and SDE API
- 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.
- CMC/UMC UCTL Model Checkers and Analyzers
- 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 branching-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)
- 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 branching-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)
- Hugo/RT: Temporal logics verification (Timed CTL, LTL); UML 2.0 interaction verification
- 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
- UPAAAL: 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.).
- SRML-Editor and Use Case Wizard: "The SRML Modelling Environment a) allows textual modeling of SRML modules, b) provides editing functionalities (e.g., code completion), c) allows import/re-editing of existing SRML modules, d) allows to validate SRML modules with respect to the SRML meta-model and to store SRML models, e) allows to create graphical representation of SRML modules structure and to edit it. "; "The Use Case Wizard transforms an extension of Use Case diagrams with specialized actors to SRML textual specification and module diagram. "
- ChorSLMC: "ChorSLMC is a verification tool for service-based systems that allows to verify choreography conformance, taking as input systems specified in Conversation Calculus, a core calculus for SOC developed within the SENSORIA project, and WS-CDL like choreographic descriptions. The tool is implemented as an extension to SLMC, a framework for model checking distributed systems against properties expressible in dynamic spatial logic, and may also be used on service-based systems to check other interesting properties of typical distributed systems, using the core dynamic-spatial logic available in SLMC. "
- Venus: "VENUS is a Verification ENvironment for UML models of Services. This tool permits the verification of service properties by relying on (transparent) mathematically founded techniques. VENUS has been explicitly developed for being accessible by users not familiar with formal methods. Its theoretical bases are the calculus COWS, the temporal logic SocL and the model checker CMC. VENUS automatically translates UML4SOA models of services and natural language statements of service properties into, respectively, COWS terms and Socl formulae, and then checks them using CMC, possibly providing counterexamples. "
- BliteC: "BliteC is a software tool for supporting a rapid and easy development of WS-BPEL applications. BliteC translates service orchestrations written in Blite, a formal language inspired to but simpler than WS-BPEL, into executable WS-BPEL programs. The tool simplifies the task of developing WS-BPEL applications because Blite provides a textual programming notation and is equipped with an unambiguous semantics, while BliteC properly packages the produced files to be readily deployed and executed in a WS-BPEL engine. "