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.

VECS - Verification Environment for Critical Systems

Many standards for safety critical applications recommend the usage of formal verifcation techniques as a quality assurance during the complete system developement cycle.

Hence, 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, analyze and secure such complex systems. Unfortunately they are not widely used in practice due to several reasons.

Today, there already exist lots of verification tools (like Model Checkers, Deductive Verification Tools 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 the usage of different languages with different syntax and semantics. Therefor the system has to be build within the different modeling paradigms in parallel. The question rising immediately is: how can it be guaranteed that the model provides the same semantical meaning in all different languages?

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.

VECS - safety analysis made easy

VECS is a verification environment build to support the development process of safety critical systems, including formal verification techniques and decumentations to build a corresponding safety case on.

Therefor, it provides full language support for SAML (Safety Analysis and Modeling Language). It combines language elements of both, qualitative and quantitative modeling languages as well as the integration of specific failure behavior. Hence, it is possible to use different verification aspects and techniques (e.g. probabilistic model checking, fault tree analysis, qualitative model checking) with one single model.

To support these techniques, VECS implements, well specified, connection to external verification tools like NuSMV, nuXmv or PRISM and implements other analysis techniques as DCCA. Further, it is planned to extend the set of tools with other verification engines as UPPAAL or iimc.

All in all, VECS attempts to make formal model-based development usable in all-day engineering processes. This is reached by combining several different formal analysis techniques and tools within one verification environment.

VECS Features

VECS includes several features making the work with formal verification techniques easier. On the one hand, it supports extended IDE features for the SAML development and on the other hand provides several model verification and analysis techniques. The main features are given in the following list:

  • Extended SAML IDE support: for the comfortable SAML modeling, VECS offers several IDE features, e.g., syntax highlighting, syntax verification with error messages and quick fixes, a package explorer, a model outline, ... Further, VECS offers special model specific analysis to check whether the SAML model is exhaustive or if there exists overlapping transition rules.
  • Connection to several model checking tools: VECS implements a connection to several model checkers like NuSMV, nuXmv and Prism. Therefore, one can easily execute a model check from and analyze the returned results (e.g. counter examples) within and with the help of VECS. (see Verification)
  • Visualization of the verification results: To gain a better understanding of verification result, VECS offers several visualization tools.(see Legend View, Plot View, Trace View)
  • Model debugging: VECS offers an interactive debugger making it possible to analyze counter examples by jumping into the hazard state and step back- and forward through the model's state space. (see Simulator)
  • Simulator: With the simulator it is possible to explore the model's state space by jumping into a specific model state and to walk through the model's state space. Further, it can be combined with external, real world systems, to execute a co-simulation and analyze the model's behavior in a real-world environment. (see Simulator)
  • Fault Tree Analyses: VECS implements DCCA (Deductive Cause-Consequence Analysis) to generate minimal cut set for fault tree analyses. (see DCCA Generator)
  • Model Viewer: The Model Viewer visualizes all model elements and its connections to get an overview over the modeled system as well as over all existing links and dependencies. (see Model Viewer)
  • Remote model checking: With VECS-Remote expensive verifications can be executed on external server systems without loosing the comfort of using VECS on your local machine, because all results and information are returned to your personal VECS instance. (see Simulator)

 

IDE-Features

description

VECS relies on the Eclipse framework. Therefor the developer will gain from a known look and feel. Additionally the framework offers the plugin-based structure which with you can get all kinds of third party connectors available for eclipse.

Besides that, VECS was extended to allow the best experience with known developer-support tools as

  • Syntax Highlighting
  • Auto-Completion
  • Auto-Formating
  • Error Recognition and Quickfixes (syntax and semantic)
  • Project Management
  • Model Outline
  • Version Control System
  • Import System

Model Overview

Description

Sometimes it can be hard to understand a defined model, especially if it's a large one. VECS offers a graphical model view to identify possible elements within a given model. Interconnections between components and formulas can be seen in a graph-like representation.

Grey boxes denote formulas. Each rectangle represents one component, which can be a state machine or a hierarchy element. Hierarchical structure is shown by grouping components within their parent component rectangle. As a component can be used as state automaton and at the same time hierarchical element, in this case a state machine symbol (black dot with gray cogwheels) refers to the automaton within this component. The arrow indicates who is reading the value of the referred element, indicating the relation between two components/formulas.

Integrated Verification

Description

One key feature of vecs is the integration of the verification process in the development environment. To verify a SAML model, the application of different model checkers is possible. The automatic selection of a tool adaptor depends on the type of specification that is used. The SAML model can be verified using CTL, LTL or PCTL specifications. Moreover, a propositional logic Hazard can be specified that is used for the fault tree generation.

Traceview

Description

The trace view allows you to analyse a certain path trough the model. This can be either a counter example provided by a model checker or a trace generated by the simulator. It allows you to understand, when the model did which state change. Thus allowing you to analyse, how a counter example was able to happen or what consequences a certain state change might have.

The trace view presents the time-steps of the model in descending order at the most-left row. State values are displayed in a timeline, only displaying value changes. If no change occurred over several step, a simple line is added to improve readability.

Plotview

Description

The plot-view allows for an alternative representation of a certain trace within the model. This trace can be either a counter example or a simulator run. Especially for long execution times, e.g. more then 30 steps, it is much easier to gather the model behavior from the plot view then the table view. This is because state changes are made visible by changes in the gradient of the graph.

Together with the counter example viewer, the plot view allows the easy and fast understanding of the model behavior.

Legendview

Description

The Legend View displays all states and formulas used within the model, when in the debug mode. It allows you to enable and disable this elements to adjust the plot view as well as the trace view. This allows you to concentrate on this states and formulas that are of current interest for you.

Model Simulation 

Description

One of the most complicated aspects of formal methods is the behavior of the model. This is in particular important, as the benefit of formal methods can be easily compensated if users specify models incorrectly. Understanding the semantics of state-based synchronous models within discrete time-steps is challenging. VECS offers tool-support for formal models, allowing the user to investigate any model step-by-step in forward and backward direction. For probabilistic or non-deterministic transition, the user can choose the next value out of a list of possible states. Therefore, it is possible to easily understand, how the formal model behaves over time.

DCCA-Generator

Description

The DCCA Generator is a method to calculate a minimal failure cut set for a given hazard. DCCA stands for Deductive Cause Consequence Analysis.

It is calculated be running a number of qualitative specifications through a model checker. Within this specification, failures are allowed and disallowed, until the minimal cut set is calculated. Therefor the DCCA generator must know about the failure modes within the model. This is done with the failure component keyword. Failures, which are not modeled using this syntax will not be taken into account during the DCCA.

Based on the result of the DCCA, VECS is able to generate a fault tree, depicting the minimal cut set in an easy to read and for safety engineers understandable manner.

Remote Verification

Description

When dealing with larger models, model checking might need longer to complete. When executing the model checker locally, your computer has to stay on until the model is finished. During this time period, a lot of memory as well as CPU power is consumed, which might lead to the inability to use the computer further.

To allow for you to model further or do some other tasks, VECS contains the ability to send model checking jobs to a remote server. The results can be viewed later.

Why and What? In this section we give an overview over motivation and the core features of VECS.

Read more: Product

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“.

Read More