VECS contains several concepts like Components, Hierarchies, Formulas in its language. The following article gives an overview over each concept. Therefore this articles uses a description of the concept and a small code example.

Components

Description

Components comprise a fundamental structure in a SAML model. Each component represents a state machine, where state variables and transition rules are defined. A SAML model consists of an arbitrary number of components.

A component contains its name <component name> an arbitrary number of state variable definition <state variable definition i> and an arbitrary number of update rules <update rule j>. The component name must match [a-zA-Z][_#a-z0-9A-Z]*. State variables and their corresponding transition rules can only be defined inside components. Each component is also a namespace, and thus, component names must be unique within their namespace. This means that its not possible to have identically named components in one namespace.

Nested components are also allowed by SAML. This is done without any special keywords simply by defining one component inside another one. Indentation of inner components is not required, but is good practices to improve readability. There is no limit to the level of nesting for components, and each component may contain several subcomponents. Each component must be identified according to the namespace concept. This means that a component has a canonical name that is comprised of its own name and the names of all components that it is nested in, in hierarchical order, separated by a period. Similarly, all state variables have a canonical name, comprised of the canonical name of their parent component, a period, and its own name. When conditions or expressions in one component refer to state variables from other components, these need to be referred to by their canonical name.

Hierarchies have no semantics with respect to the model behavior, they are only a means to structure the model for better comprehension by a human reader. That is, moving one global component to become a subcomponent of another component does not change the model semantics. One coincidental exception is changing the hierarchy in a model containing several state variables with identical names. Since these are referenced through a qualified name (not necessarily a fully qualified one) that includes part of the hierarchy, changing the hierarchy (e.g. moving a subcomponent from one component to another) may switch the referenced variable to another one with identical name.

Hierarchies

One of the biggest problems in every kind of programming language is readability. Within SAML, readability can be achieved by using hierarchically structured models that allow to group together elements within logical containers. A namespace concept allows relative and absolute referencing of these elements. VECS supports the creation of hierarchies, which allow the user to find the wanted element by simply walking through the hierarchy layers. Each container can be collapsed to hide parts of the model that are irrelevant for the current modeling part.


Formulas

Description

Symbolic constants are used to increase model readability and to make model variation easier. In a similar way as constants formulas are use to define numeric expressions, which are defined once and used multiple time in a model. Thus, we consider a formula as a stateless, parameter-free, typed, named expression that commonly is an abbreviation for conditions or state variables.

A formula is defined by a data type <data type>, a symbolic name <name>, and an expression <expression>. Similar as for symbolic constants the data type refers to the type of expression (float, integer or boolean). The name of the formula has the form of [a-zA-Z][a-zA-Z0-9_]*. The expression has the respective data type (float, integer or boolean). In contrast to expressions for constants, these expressions can refer to arbitrary state variables, as they are re-evaluated for each new time step. Note that formulas cannot have parameters (SAML does not support full-fledged functions because they may result in an infinity loop during model creation).

Templates

Description

Templates are an abstract definition of modules that can be instantiated and used at more than one place. A template as such is like a class (without inheritance). The syntax consists of two separate parts: the definition of the template and the instantiations. A template consists of two separate parts, the definition of the template and the instantiations.

A template itself is an abstract description of a component. All interaction with its environment is defined in terms of underspecified constants and formulas. These constants and formulas are called an interface. As soon as it is instantiated, the template is turned into a specific component. For the proper instantiation the formulas and constants listed in the interface must be defined with actual values.

Failures

Description

SAML allows for the easy and convenient creation of failure occurrence patterns. This failure pattern defines whether a certain failure occurs at a specific time or not. The basic form allows an occurrence of a failure occur and an optional recover recover.

The general form consists of four different forms of failures. The basic idea is to divide the failure model into failure occurrence pattern and a specific local failure behavior.

The occurrence pattern specifies the type of occurrence. This can be a transient or a persistent failure. Persistent failures only occur once and afterwards stay in the failure state, whereas transient failures can occur at every step.

It is also possible to describe the failures based on their mode. Per-time failures describe the occurrence of the failure in a given time interval. The per-demand failures describe failures which can only occur if there is a request/demand.

Based on this classification, four main patterns can be identified. These are combinations of per-demand/per-time and transient/persistent and can be defined using special keywords in SAML.

The types transient/persistent are determined by the keyword “recovers”. The keywords “recover none” define a persistent fault. Per-demand is determined by the keyword “demand”, otherwise is the fault of type per-time.

The behavior of the failure, e.g. what kind of impact the failure has on the model, has to be created separately, as this is the part which is dependent on the model. Obviously, it would be possible to combine the behavior and the occurrence within the functional model. By separating the two concerns, the model becomes more readable.

Failure components do not only help to divide your model into a functional and a failure model. It also allows you to specify within your specifications the occurrence or non-occurrence of this failure.

Consequently, this is done by the DCCA generator. With the help of explicitly specifying failures, the DCCA generator is able to create a number of failure combinations that will lead to an hazardous state of your system. This set of failures is called minimal cut set.


Enumerations

Description

As state variables can only have integer values no meaning is associated with them. Often it is useful to have meaningful names associated with the current model which ease readability. SAML supports symbolic enumerations as the value type for state variables. It defines a set of symbolic constants for states that a state variable can be in. SAML hides the (meaningless) numerical values of these symbolic enumerations from the user, which improves comprehension.

An enumeration consists of an enumeration name <enumeration name> and a symbolic value range from <value 1> to <value n>, where <value i> is the symbolic name for the individual enumeration value. The name for both the enumeration itself and the values must follow the rule for names in SAML, [a-zA-Z][a-zA-Z0-9_]*. Please note: You can only use non keyword descriptions as value. For example the usage of true and false isn't possible.

An enumeration is commonly used to declare state variables but can be also used in other ways. Each symbolic enumeration value must be identified according to the namespace concept. Note that the enumeration values are mapped to integer values. However, this mapping is opaque to the user. Thus, conditions (and boolean formulas) should compare enumerative state variables only to symbolic enumeration values of the respective enumeration, and never to integers or values of other enumerations. Integer and decimal expressions (be they in conditions, formulas or state assignments) should never perform computation with symbolic enumeration values. Only values of the corresponding evaluation should be assigned to enumeration state variables in state assignments, no expressions based on these or other state variables, and no integer or decimal values. All other behavior is undefined.

Interfaces

Description

Interfaces in SAML are construct to enhance the readability of the formal model and separate the concerns of sub-components. The overall idea is based on UML components, ports and interfaces. Generally interfaces represent a shared boundary between two components. These boundaries provide or require methods or attributes. Methods and attributes are designed to react on or trigger specific behavior of the port enclosing component.

Reusability

Description

It is possible to import other SAML models to be used in the current model. An import is defined by a file name (with a path if necessary) <SAML file path> and the import name <import name>. The file name refers to a SAML model to be imported. The import name has the form of [a-zA-Z][a-zA-Z0-9_]* and it is used to set the namespace of the imported model.

Supported Specifications Types

LTL

Description

A Linear-time Temporal Logic(LTL) formula is used to define a general temporal system behavior, like in every possible model execution, finally there is a state where engine_switch.a = engine_switch.off. It is important that LTL properties must hold for all possible execution paths of the model. In SAML, an LTL specification is marked by the keyword SPEC. The type of the specification is derived later by the usage of the specification operators.

If a LTL specification is used, VECS invokes the nuXmv model checker with the sat-based IC3 algorithm.

CTL

A Computation Tree Logic(CTL) (or Branching Time Logic) is a temporal logic specifying the system's behavior on a set of possible execution paths. A temporal behavior can either be specified for at least one path (E) or all paths (A), which are reachable from a specific system state. In contrast to LTL, CTL can be used when a more detailed behavior specification, especially for models containing nondeterminisms, is required. In SAML, CTL specifications are marked by the keyword SPEC. The type of the specification is derived later by the usage of the branching specification operators A and E.

In general, when CTL specifications must be verified, a BBD-based verification algorithm of nuXmv is invoked.

PCTL

Description

A Probabilistic Computation Tree Logic (PCTL) formula is, simplified spoken, a CTL formula extended for probabilistic modeling. If one have a probabilistic system model, PCTL provides the functionality to ask with which probability a property holds, instead of simply verify whether the property holds. Furhter, it is possible to specify probability thresholds, i.e., a minimal or maximal probability value for a given property. Additionally, in PCTL a bound for the temporal operators like F< =10 (finally, within 10 steps, a specific state is reached).

In SAML, PCTL specifications are marked by the keyword SPEC. The type of the specification is derived later by the usage of probability as P=? or Pmax=0.5.

If a PCTL specification must be verified, the Prism model checker is invoked with the given model and the corresponding specification.

Hazards

Description

A hazard specification is a propositional formula describing one specific state of the system. In general, it describes a hazardous state of the system that should not be reached under normal conditions. However, in combination with failure components (see Failure Components) it is used to invoke the Deductive Cause-Consequence Analysis (DCCA) to generate a minimal cut sets for the fault tree analysis, based on the specified hazard.

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