In addition to the case studies presented here, we are currently working on two larger case studies. There intention is to evaluate, whether Saml and VECS can be applied for real world size system models that are currently on topic in systems engineering. This is on the one hand a model of the PZB (Punktförmige Zugbeeinflussung literally "punctiform train influencing"), which is the most used train protection system in Germany, and on the other hand the new ETCS (European train Control System), which is planned to be the new train controle system across many european countries.
The Verification Environment for Critical Systems (VECS) was designed to allow engineers to use model-based analyzing techniques without the need to gain deep knowledge in the field of formal model checkers. We aim at creating an intuitive and user-friendly experience, hiding the technical layer of this type of analysis and displaying the results of the formal model checkers in a comprehensive way.
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.
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.
Am Donnerstag, dem 08.09.2016 veranstaltete der Lehrstuhl für Software Engineering der Otto-von-Guericke Universität Magdeburg unter Leitung von Prof. Dr. Frank Ortmeier mit großem Erfolg den dritten Expertenworkshop zum Thema „Anwendung innovativer modellbasierter Sicherheitsanalysemethoden im Zulassungsprozess sicherheitskritischer Anwendungen“.