One main intention of the System analysis and modelling language is to serve as an intermediate language between the engineering and the formal verification world. The goal of VECS is to bring them together and decrease the complexity of using formal methods during the engineering processes. Therefore, VECS provides several interfaces between enginnering and modeling, as well as, verifcation tools.
The big advantage of using Saml as intermediate language lies in the fact that it provides the possibility to decouple the engineering and the verification layer. In fact, this means that you only need one importer into and one epxorter from the syntactically and semantically well defined and researched language Saml, which of course reduces the possiblity of transformation mistakes and serves as plattform for other analysation features like debugging, static anlyasis and others.
The engineering interface provides connections to several design and modeling tools and languages. Thereby, you can verify your design and modeling documents against several specifcaitons as well as check them for formal correctnes. Due to the well specified interface we are able to connect almost every tool with vecs, if there exists any semantically transformation into Saml. If you wonder, whether your favorit tool can be connected to VECS, just send us an email and we can evaluate that. At the moment, we are working on the following connections:
- Requirement Tools: We provide a link to the requirement engineering tool Rational Doors. By using this, you get the opportunity to trace the given requirements to the Saml-Model, i.e., it is possible to state out from which requirement a specific model element results.
- UML-Tools: Currently, we provide a link to the widely used modeling tool Enterprise Architect (EA). Although we only support EA at the moment, it is possible to import other UML-Models via the XMI-Importer. This means, each file in the standard XMI-format can be imported into VECS as Saml code.
- Modelica: In our ongoing research, we are also working on hybrid modeling support for Saml. At the moment, we provide a prototypical implementation of a Modelica importer (not included in the standard setup).
For handeling a wide range of verification tasks, VECS provides interfaces to several verifcation tools, whereas each has its own advantages. Currently, these are: