Satisfiability-based verification techniques, leveraging modern Boolean satisfiability (SAT) and Satisfiability Modulo Theories (SMT) solvers, have demonstrated efficacy in addressing practical problem instances within program analysis.However, current SMT solver implementations often encounter limitations when addressing non-linear arithmetic problems, particularly those involving floating point (FP) operations.This poses a significant challenge for safety critical applications, where accurate and reliable calculations based on FP numbers and elementary mathematical functions are essential.This paper shows how an alternative formulation of the satisfiability problem for FP calculations allows for exploiting parallelism for FP constraint solving.By combining global optimization approaches with parallel execution on modern multi-core CPUs, we construct a portfolio-based semidecision procedure specifically tailored to handle FP arithmetic.We demonstrate the potential of this approach to complement conventional methods through the evaluation of various benchmarks.

Abstract This special issue is dedicated to the presentation of novel results in the scope of program analysis, verification, and testing of software to improve its quality. The papers included in the special issue present approaches that successfully combine model-based test case generation, reasoning about functional equivalence, data mining, classification, and the combination of abstraction with model-checking, to address real software applications in realistic settings.

We consider the problem of efficiently checking a set of safety properties P1,...,Pkof one design. We introduce a new approach called JA-verification, where JA stands for “JustAssume” (as opposed to “assume-guarantee”). In this approach, when proving a property Pi, one assumes that every property Pjfor j ≠ i holds. The process of proving properties either results in showing that P1,...,Pkhold without any assumptions or finding a “debugging set” of properties. The latter identifies a subset of failed properties that are the first to break. The design behaviors that cause the properties in the debugging set to fail must be fixed first. Importantly, in our approach, there is no need to prove the assumptions used. We describe the theory behind our approach and report experimental results that demonstrate substantial gains in performance, especially in the cases where a small debugging set exists.

Choreographies are contracts specifying from a global point of view the legal interactions that must take place among a set of services. Such a contract may serve as a reference in the development of concurrent distributed system, whether it is achieved following a top-down or a bottom-up approach. In this article, we present VerChor, a generic, modular, and extensible framework for supporting the development based on choreographies. It relies on a choreography intermediate format (CIF) into which several existing choreography description languages can be transformed. VerChor builds around a set of formal properties whose verification is central to choreography-based development. To support this development process, we propose a connection between CIF and the CADP verification toolbox, which enables the full automation of the aforementioned properties. Finally, we illustrate a practical use of the VerChor framework through its integration with the Eclipse BPMN 2.0 designer.

Although model-based approaches can yield very precises safety analysis, they are rarely used in practice. The reason is, that most techniques are very difficult to apply and almost always require separate models and tools. In this paper we present an outline for the integration of different model-based safety analysis and safety optimization methods into a single tool framework. We present the envisioned work-flow and some of the requirements for the tool integration. Because of its wide acceptance, platform independence and its well-documented API, we chose the Eclipse platform as framework foundation.

Dependability is often a very abstract concept. The reason is that dependability implications shall be very rare and are often not even wanted to happen during testing. In particular for software-intensive systems, it is very hard to find correct causal relationships/minimal cut sets. Modern model-based approaches help here by computing for example minimal cut sets automatically. However, these methods always rely on a correct model of the environment. In addition, the results are often not traceable or understandable for humans. Therefore, we suggest combining model-based analysis for deriving safety properties with virtual realities for ensuring model validity and trace-ability of results.

An important property of embedded systems is dependability. Today this addresses mostly safety and reliability. Guaranteeing these properties is normally done by adding redundancy to the system. This approach is expensive and can not cope with changing environments. Therefore new designs are researched, which allow systems to self-adapt and self-heal. For broad acceptance in industry it is important, that organic systems can be modeled and analyzed with standard modeling tools and languages. We present a case study of an adaptive production automation cell modelled in the Lustre language using the SCADE suite and the verification of functional properties. SCADE is used widely in industry, especially in safety critical applications. Being able to model and verify adaptive systems in SCADE could increase their acceptance for these target areas.

In this paper we present a technique for safety analysis of self-adaptive systems with formal methods. Self-adaptive systems are characterized by the ability to dynamically (self-)adapt and reorganize. The aim of this approach is to make the systems more dependable. But in general it is unclear how big the benefit is compared to a traditional design. We propose a dependability analysis based on the results of safety analysis to measure the quality of self-x capabilities of an adaptive system with formal methods. This is important for unbiased and evidence-based decision making in early design phases. To illustrate the results we show the application of the method to a case study from the domain of production automation.