The usage of formal methods in the all-day engineering work moves into the focus. Especially in safety critical domains, where a failure can cause critical situations for humans or the environment, modern systems reached a complexity level, humans are not able to process anymore. However, formal methods can help to understand, analyse and secure this complex systems. Unfortunately they are not widely used in practice due to several reasons.
Today, there already exist several verification tools (like Model Checkers etc.) and languages, which help verifying and understanding a systems behavior. However, most tools are developed for a very strict purpose, i.e., proving the absence of failure or calculating the probability of a specific behavior occurrence. To solve a wider range of problems, one conceivably needs to use more than one tool to verify different aspects of a given system model. This also includes different languages with different syntax and semantics.
Therefor the system has to be build within the different modeling paradigms in parallel. The question which rises immediately is how it can be guaranteed that the model in all different languages provide the same semantical meaning? The formal verification language SAML (System Analysis Modeling Language) is one attempt to tackle this problem. It combines language elements of several modeling aspects (e.g. qualitative and quantitative elements) within one language. This means, by using only one modeling language, one can check several model aspects using different verification engines. The Verification Environment for Critical Systems (VECS) is an Eclipse based IDE supporting the development and Verification of SAML models. Therefor, it provides a full language support for SAML as well as the connection to several well-known model checking and verification tools (e.g. NuSMV and PRISM). Further, it supports several analysis features like online execution, model simulation and debugging. Additionally, VECS provides failure analysis techniques like Fault Tree Analysis to support a wider range of safety analysis requirements.
All in all, VECS is an attempt to make formal model-based development usable in all-day engineering processes. This page introduces the key features of VECS as well as several successful case studies, proving its applicability in real world scenarios.
If you wish to gather „hands-on“ experience, we invite you to visit the download page. There you will find further instructions on how to install the Eclipse plugin as well as an option to download your own free copy.