Together with Ansys, we held a webinar on Formal Verification for Model-Based Development. Prover supplies the model checker PSL, which powers Ansys new SCADE Suite Design Verifier. It provides the new Design Verifier with a great leap in performance and enables state-of-the-art formal verification of SCADE-models, including IEEE 754 floating point arithmetic.

The new Design Verifier also allows to optionally add EN50128/ISO26262 approved verification using Prover Certifier. These and other exciting features are presented in the webinar.

If you are interested in model-based development in SCADE and want to know more about all the possibilities introduced by the new Design Verifier, be sure not to miss the joint webinar with Ansys presenting the new SCADE Suite Design Verifier. The recorded webinar is hosted by Ansys and you can watch it by registering here.

Inlägget Model based development webinar with Ansys dök först upp på Prover - Engineering a Safer World.

Triple redundant sensor voter

In order to meet high redundancy requirements in avionics, a common technique is to use triple redundant sensor voters. To create a reliable signal, the outputs of three identical sensors are composed into a single signal by a voting component. The voting mechanism averages/centers the set of three input values over time to avoid being overly affected by a single faulty sensor.

The sensor voter model can be thought of as consisting of a set of floating point latches that are updated at every reading. The output is computed from the input of the three sensors and from these latches. If one disregards the floating point rounding, the latches and the output have piecewise linear definitions. The rounding makes the model non-linear.

Depending on the type of sensors (range, measurement uncertainty, etc) a typical voting algorithm needs to be configured by setting different constants(thresholds etc). The resulting behavior of the sensor voter, and checks that it is sufficiently reliable, is traditionally tested by massive simulation, which is very costly. Besides being costly, simulation can only give partial coverage.

Examples of typical requirements for the sensor voter implementation are:

– Given a bound on sensor errors (for non-faulty sensors), the error of the voter output must be sufficiently bounded.

– Given a bound on signal change (between two readings), the change in voter output must be sufficiently bounded.

To get full coverage one can instead of simulation, perform formal verification. One efficient way is to analyze the sensor voter with an SMT solver assuming that the arithmetic operations are exact (no rounding), since in this case the system is piecewise linear. The downside is that then additional argumentation is needed to take into account the “errors” introduced by rounding, i.e. handling the difference between operations on real (mathematical) numbers and operations on floating point numbers (which are rounded).

Instead of working with real numbers, a better and more complete solution would be to precisely model the floating point numbers and their operations(including rounding) when performing formal verification. A stumbling block for this approach has been performance issues. Modeling floating point arithmetic at bit level requires a significant boost in verification tool performance. This is the problem we have addressed when implementing floating point numbers in PSL.

Excellent Results

In order to really test the performance of floating point arithmetic in PSL we used double precision (64-bit) IEEE 754 floats in the HLL model. Performance often tends to degrade rapidly with increased precision, in particular when models are non-linear.

To reach the required performance boost and to fully utilize modern processor architectures, PSL uses powerful parallelization and machine learning to optimize the proof strategy.

The two requirements mentioned above were proved together five times, one for each rounding mode defined in IEEE 754. The running time on a modern multi-core processor was between 2 and 3 minutes, depending on the rounding mode.

Even though these results are impressive, as mentioned in Floating Point Model Checking, floating point verification is notoriously hard and the performance depends a lot on the complexity of the actual models. Also one needs to be very careful in order to keep the full precision of the verification valid throughout the real system:

– One needs control over possible rewritings/optimizations in the compiler, and

– one needs to make sure that the platform, on which the software is executed, exactly implements the IEEE 754 standard for the functionality which is actually used.

That said, PSL sets a high standard for floating point performance, combining precision with power. It gives the required boost to allow efficient floating point verification.

Inlägget Floating point model checking put to the test dök först upp på Prover - Engineering a Safer World.

Characteristics of specific application configuration

Specific Application Configuration (SAC) often involves large amounts of safety critical data organized in an inhomogeneous fashion. Data might be given as scheme plans, control tables, and/or in written documents, notes, etc. In some cases, the data is only communicated verbally or is even implicit as a common understanding among involved engineers.

The typical configuration process therefore tends to be error prone and time consuming. This also applies to any independent checking and verification of the final configuration. Over time, maintenance also becomes even more difficult.

Weakly and partially specified configuration data distributed over many types of sources is not an ideal way for an efficient and reliable process.

A way forward?

A way forward is to have a well specified set of SAC data organized in a uniform way in a “human friendly” open format. Such a format would also make it possible to use tool support for performing trusted computations on the SAC data for checking static requirements and for producing derived data.

In a generic approach this requires a Generic Application Configuration (GAC) containing the specification of the SAC data. The GAC is a natural place for specifying static checks and derived data.

Geographical data would preferably be represented in some compact easily reviewable format, and there should be support for tabular data.

The layout configuration format – A uniformapproach

The Layout Configuration Format (LCF) and its supporting tools released by Prover address these problems. It realizes a CENELEC SIL-4 compliant process that gives:

• a general and consistent way to represent all required SAC data for any given interlocking in a compact and review friendly file format
• a generic way to specify which SAC data is required and how it should be used for any given interlocking type
• an interface that is used to document how to collect and interpret the various pieces of data that make up the configuration of the specific application, in order to map it to LCF
• a method to configure algorithms to compute derived SAC data from given SAC data in a trusted way, in order to minimize the amount of data to create and review
• a highly configurable method for transforming SAC data to standardized tables and variable mappings for code generation and sign-off verification
• a format with accompanying tools that are independent of signaling principles, design tools, and interlocking platform.

Find out more about LCF here.

Inlägget Challenges in digitizing specific application configurations dök först upp på Prover - Engineering a Safer World.