Search

The quest for feature- and family-oriented deductive verification of software product lines resulted in several proposals. In this paper we look at delta-oriented modeling of product lines and combine two new ideas: first, we extend Hahnle & Schaefer’s delta-oriented version of Liskov’s substitution principle for behavioral subtyping to work also for overridden behavior in benign cases. For this to succeed, programs need to be in a certain normal form. The required normal form turns out to be achievable in many cases by a set of program transformations, whose correctness is ensured by the recent technique of abstract execution. This is a generalization of symbolic execution that permits reasoning about abstract code elements. It is needed, because code deltas contain partially unknown code contexts in terms of “original” calls. Second, we devise a modular verification procedure for deltas based on abstract execution, representing deltas as abstract programs calling into unknown contexts. The result is a “delta-based” verification approach, where each modification of a method in a code delta is verified in isolation, but which overcomes the strict limitations of behavioral subtyping and works for many practical programs. The latter claim is substantiated with case studies and benchmarks.

We present a realization of multi software product lines in the Java programming language that permits full interoperability and hierarchical dependencies among multiple product variants. This concept, called variability modules (VM), is implemented in terms of an architectural pattern in Java and does not require any pre-processing or language extension. It can be used with any Java development environment. The VM architectural pattern comes with a dedicated UML profile, which makes it possible to present variability to non-technical stakeholders. We evaluate our approach with the help of a real-world case study.

A program containing placeholders for unspecified statements or expressions is called an abstract (or schematic) program. Placeholder symbols occur naturally in program transformation rules, as used in refactoring, compilation, optimization, or parallelization. We present a generalization of automated cost analysis that can handle abstract programs and, hence, can analyze the impact on the cost of program transformations. This kind of relational property requires provably precise cost bounds which are not always produced by cost analysis. Therefore, we certify by deductive verification that the inferred abstract cost bounds are correct and sufficiently precise. It is the first approach solving this problem. Both, abstract cost analysis and certification, are based on quantitative abstract execution (QAE) which in turn is a variation of abstract execution, a recently developed symbolic execution technique for abstract programs. To realize QAE the new concept of a cost invariant is introduced. QAE is implemented and runs fully automatically on a benchmark set consisting of representative optimization rules.

A Software Product Line (SPL) is a family of similar programs (called variants) generated from a common artifact base. A Multi SPL (MPL) is a set of interdependent SPLs (i.e., such that an SPL's variant can depend on variants from other SPLs). MPLs are challenging to model and implement efficiently, especially when different variants of the same SPL must coexist and interoperate. We address this challenge by introducing variability modules (VMs), a new language construct. A VM represents both a module and an SPL of standard (variability-free), possibly interdependent modules. Generating a variant of a VM triggers the generation of all variants required to fulfill its dependencies. Then, a set of interdependent VMs represents an MPL that can be compiled into a set of standard modules. We illustrate VMs by an example from an industrial modeling scenario, formalize them in a core calculus, provide an implementation for the Java-like modeling language ABS, and evaluate VMs by case studies.

Software has become an indispensable part of industrial production and thus influences the life cycle of manufacturing systems, as many of these systems have to be replaced or evolved due to changing requirements. Software adaptation through continuous evolution extends the service time of these systems and thus saves valuable resources. In this paper we present an interdisciplinary methodology for reengineering legacy software to increase the productive lifetime. Our proposed approach systematically reuses implicit domain knowledge to evolve, validate and commission new software from legacy code. The approach is evaluated on a CNC machine as a special type of industrial system.

Modularity and compositionality in verification frameworks occur within different contexts: the model that is the verification target, the specification of the stipulated properties, and the employed verification principle. We give a representative overview of mechanisms to achieve modularity and compositionality along the three mentioned contexts and analyze how mechanisms in different contexts are related. In many verification frameworks one of the contexts carries the main burden. It is important to clarify these relations to understand the potential and limits of the different modularity mechanisms.

Software Engineering as a discipline and, in particular, as a research field within Computer Science, is still mainly focused on methods, techniques, processes, and tools to develop software from scratch. In reality, however, greenfield scenarios are not the most common ones. It is important to realize that dynamic evolution of software became a much more common and relevant issue in recent times, and its importance keeps growing. Software refactoring, parallelization, adaptation, therefore, become central activities in the value chain: automating them can realize huge gains. Formal approaches to software modeling and analysis are poised to make a substantial contribution to software re-engineering, because they are fundamentally concerned with automation and correctness. This potential, however, is far from being realized. Formal methods tend to aim at software development ab ovo or look at some piece of given software as a static object. This state of affairs motivated a track on Automating Software Re-Engineering, where we invited a group of leading researchers with an active interest in the automation of software re-engineering to discuss the state of the art.

We propose the trace modality, a concept to uniformly express a wide range of program verification problems. To demonstrate its usefulness, we formalize several program verification problems in it: Functional Verification, Information Flow Analysis, Temporal Model Checking, Program Synthesis, Correct Compilation, and Program Evolution. To reason about the trace modality, we translate programs and specifications to regular symbolic traces and construct simulation relations on first-order symbolic automata. The idea with this uniform representation is that it helps to identify synergy potential—theoretically and practically—between so far separate verification approaches.

22nd International Conference on Fundamental Approaches to Software Engineering, FASE 2019, Prague, Czech Republic, 6 Apr 2019 - 11 Apr 2019; International journal on software tools for technology transfer : STTT (2020). doi:10.1007/s10009-020-00589-6 special issue: "Special Issue: FASE 2019", Published by Springer, Berlin

TimSort is the main sorting algorithm provided by the Java standard library and many other programming frameworks. Our original goal was functional verification of TimSort with mechanical proofs. However, during our verification attempt we discovered a bug which causes the implementation to crash by an uncaught exception. In this paper, we identify conditions under which the bug occurs, and from this we derive a bug-free version that does not compromise performance. We formally specify the new version and verify termination and the absence of exceptions including the bug. This verification is carried out mechanically with KeY, a state-of-the-art interactive verification tool for Java. We provide a detailed description and analysis of the proofs. The complexity of the proofs required extensions and new capabilities in KeY, including symbolic state merging.

We present a method to generate automatically exploits for information flow leaks in object-oriented programs. The goal, similar to white-box test generation, is to automatically produce executable, reusable test cases that challenge a given information flow policy with a very high degree of guaranteed coverage. Our approach combines self-composition and symbolic execution to create an insecurity formula for a given program and information flow policy. Satisfiability of this formula signifies the presence of information leaks and permits to use model generation for creating exploits. We support different kinds of information flow policies like noninterference, delimited information release, and information erasure. A prototypic tool implementation for Java programs of our approach is available. It generates exploits in the form of self-contained, executable JUnit tests. We evaluate our method and tool based on a set of micro-benchmarks and a case-study on e-voting.

Planning of railway tracks at Deutsche Bahn (DB) so far is done manually by planning experts with the help of CAD tools. This incurs substantial cost and planning time which is exacerbated by the complex planning rules laid down in ETCS regulations mandatory for new tracks. In a project performed for DB Netz AG we explore the possibility of automating a large part of the ETCS rail track planning process. We report on our experience in building a prototypic automated ETCS planning tool. It takes a standardized object-oriented track model as input and provides output in the same format with all required ETCS track elements placed at their correct position. The tool can be integrated into manual planning processes and allows manual fine-tuning. Our approach uses algorithmic sequencing of formalized planning rules based on the knowledge and best practices obtained from experienced track planners. The result of the planning tool can be visualized for the purpose of conformance checking with the ETCS planning rulebooks to simplify the certification process. A model-based, domain-specific test coverage criterion has been developed to validate correctness and completeness of the algorithmic rendering of the rules.

Read and write dependences of program variables are essential to determine whether and how a loop or a whole program can be parallelized. State-of-the-art tools for parallelization use approaches that over- as well as under-approximate to compute dependences and they lack a formal foundation. In this paper, we give formal semantics of read and write data dependences and present a program logic that is able to reason about dependences soundly and with full precision. The approach has been implemented in the deductive verification tool KeY for the target language Java.

Formal specification of multi-threaded programs is notoriously hard, because thread execution may be preempted at any point. In contrast, abstract concurrency models such as actors seriously restrict concurrency to obtain race-free programs. Languages with cooperative scheduling occupy a middle ground between these extremes by explicit scheduling points. They have been used to model complex, industrial concurrent systems. This paper introduces cooperative contracts, a contract-based specification approach for asynchronous method calls in presence of cooperative scheduling. It permits to specify complex concurrent behavior succinctly and intuitively. We design a compositional program logic to verify cooperative contracts and discuss how global analyses can be soundly integrated into the program logic.

Cheap and ubiquitous availability of multi-processor hardware provides a strong incentive to parallelize existing software. We aim to annotate existing sequential applications written in C with OpenMP directives that can be processed by compilers on high performance parallel computers. We adopt a model-based approach, where from sequential C-code a software model is extracted in a largely automatic fashion. The target is the modeling language ABS (Abstract Behavioral Specification), an active objects-language with formal semantics. ABS has been designed to be statically analyzable. We focus on the first stages of model-based parallelization: model extraction and validation. We define a behavior-preserving, fully automatic translation of a large fragment of sequential C that explicitly renders all possible execution sequences, then use automated test case generation to produce validation test cases.

22nd International Conference Fundamental Approaches to Software Engineering, FASE 2019, Prague, Czech Republic, 6 Apr 2019 - 11 Apr 2019; Cham : Springer, Lecture notes in computer science 11424, xiii, 446 Seiten : Diagramme (2019). doi:10.1007/978-3-030-16722-6, Published by Springer, Cham

The C programming language is well-known to have a large amount of underspecified behavior that often results in non-determinism even of sequential programs. In many application areas, not necessarily safety-critical ones, this is highly undesirable. A number of approaches and tools that statically analyze such behavior have been suggested, but they suffer from a high number of false positives and negatives. We present a novel model-based approach to analyzing non-determinism that works by automatic extraction of a faithful model of a given C program in a concurrent active object language. The extracted model renders any non-deterministic behavior of the C program in terms of explicit concurrency. This opens the door to global, semantic analyses. We give a fully formal account of the model extraction process and present an experimental evaluation of its implementation in the model extraction tool C2ABS.

Software Product Lines are an established mechanism to describe multiple variants of one software product. Current approaches however, do not offer a mechanism to support the use of multiple variants from one product line in the same application. We experienced the need for such a mechanism in an industry project with German Railways where we do not merely model a highly variable system, but a system with highly variable subsystems. We present the design challenges that arise when software product lines have to support the use of multiple variants in the same application, in particular: How to reference multiple variants, how to manage multiple variants to avoid name clashes, and how to keep multiple variants interoperable.

Formal verification of compiler correctness requires substantial effort. A particular challenge is lack of modularity and automation. Any change or update to the compiler can render existing proofs obsolete and cause considerable manual proof effort. We propose a framework for automatically proving the correctness of compilation rules based on simultaneous symbolic execution for the source and target language. The correctness of the whole system follows from the correctness of each compilation rule. To support a new source or target language it is sufficient to formalize that language in terms of symbolic execution, while the corresponding formalization of its counterpart can be re-used. The correctness of translation rules can be checked automatically. Our approach is based on a reduction of correctness assertions to formulas in a program logic capable of symbolic execution of abstract programs. We instantiate the framework for compilation from Java to LLVM IR and provide a symbolic execution system for a subset of LLVM IR.

Any complex software system exhibits a tension between the technical perspective required for its realization and the user-level perspective. We term this the “how-what gap”, represented by the questions “how is a system implemented” vs. “what is its functionality/usage”. The normative, anticipated behavior of a software system as envisaged during its development and the de facto, observed behavior emerging after its continued operation tends to drift apart, resulting in behavioral inconsistency. We discuss how behavioral consistency in software systems can be captured in technical and formal terms, we sketch a possible tool chain that could support it, and we describe some of the research challenges that must be solved. Our main idea is to combine software analysis approaches represented by various forms of static analysis and formal verification with runtime verification, monitoring, and automata learning in order to optimally leverage the de facto observed behaviour of the deployed systems.

We propose active object languages as a development tool for formal system models of distributed systems. Additionally to a formalization based on a term rewriting system, we use established Software Engineering concepts, including software product lines and object orientation that come with extensive tool support. We illustrate our modeling approach by prototyping a weak memory model. The resulting executable model is modular and has clear interfaces between communicating participants through object-oriented modeling. Relaxations of the basic memory model are expressed as self-contained variants of a software product line. As a modeling language we use the formal active object language ABS which comes with an extensive tool set. This permits rapid formalization of core ideas, early validity checks in terms of formal invariant proofs, and debugging support by executing test runs. Hence, our approach supports the prototyping of formal system models with early feedback., Comment: In Proceedings ICE 2018, arXiv:1810.02053

Software Product Lines (SPLs) are an established area of research providing approaches to describe multiple variants of a software product by representing them as a highly variable system. Multi-SPLs (MPLs) are an emerging area of research addressing approaches to describe sets of interdependent, highly variable systems, that are typically managed and developed in a decentralized fashion. Current approaches do not offer a mechanism to manage and orchestrate multiple variants from one product line within the same application. We experienced the need for such a mechanism in an industry project with Deutsche Bahn, where we do not merely model a highly variable system, but a system with highly variable subsystems. Based on MPL concepts and delta-oriented oriented programming, we present a novel solution to the design challenges arising from having to manage and interoperate multiple subsystems with multiple variants: how to reference variants, how to avoid name or type clashes, and how to keep variants interoperable.

Static analysis tools, such as resource analyzers, give useful information on software systems, especially in real-time and safety-critical applications. Therefore, the question of the reliability of the obtained results is highly important. State-of-the-art static analyzers typically combine a range of complex techniques, make use of external tools, and evolve quickly. To formally verify such systems is not a realistic option. In this work, we propose a different approach whereby, instead of the tools, we formally verify the results of the tools. The central idea of such a formal verification framework for static analysis is the method-wise translation of the information about a program gathered during its static analysis into specification contracts that contain enough information for them to be verified automatically. We instantiate this framework with costa, a state-of-the-art static analysis system for sequential Java programs, for producing resource guarantees and KeY, a state-of-the-art verification tool, for formally verifying the correctness of such resource guarantees. Resource guarantees allow to be certain that programs will run within the indicated amount of resources, which may refer to memory consumption, number of instructions executed, etc. Our results show that the proposed tool cooperation can be used for automatically producing verified resource guarantees.

Realizing the full potential of virtualized computation-the cloud-requires rethinking software development. Deployment decisions, and their validation, can and should be moved up the development chain into the design phase.

We generalize the principle of counter example-guided data abstraction refinement (CEGAR) to guided refinement of Software Product Lines (SPL) and of analysis tools. We also add a problem decomposition step. The result is a framework for formal SPL analysis via guided refinement and divide-and-conquer, through sound orchestration of multiple tools.

We use deductive verification to show safety properties for the railway operations of Deutsche Bahn. We formalize and verify safety properties for a precise, comprehensive model of operational procedures as specified in the rule books, independently of the shape and size of the actual network layout and the number or schedule of trains. We decompose a global safety property into local properties as well as compositionality and well-formedness assumptions. Then we map local state-based safety properties into history-based properties that can be proven with a high degree of automation using deductive verification. We illustrate our methodology with the proof that for any well-formed infrastructure operating according to the regulations of Deutsche Bahn the following safety property holds: whenever a train leaves a station, the next section is free and no other train on the same line runs in the opposite direction.

Language semantics that is formal and mathematically precise, is the essential prerequisite for the design of logics and calculi that permit automated reasoning about programs. The most popular approach to programming language semantics—small step operational semantics (SOS)—is not modular in the sense that it does not separate conceptual layers in the target language. SOS is also hard to relate formally to program logics and calculi. Minimalist semantic formalisms, such as automata, Petri nets, or \(\pi \)-calculus are inadequate for rich programming languages. We propose a new formal trace semantics for a concurrent, active objects language. It is designed with the explicit aim of being compatible with a sequent calculus for a program logic and has a strong model theoretic flavor. Our semantics separates sequential and object-local from concurrent computation: the former yields abstract traces which in a second stage are combined into global system behavior.

A program has secure information flow if it does not leak any secret information to publicly observable output. A large number of static and dynamic analyses have been devised to check programs for secure information flow. In this paper, we present an algorithm that can carry out a systematic and efficient attack to automatically extract secrets from an insecure program. The algorithm combines static analysis and dynamic execution. The attacker strategy learns from past experiments and chooses as its next attack one that promises maximal knowledge gain about the secret. The idea is to provide the software developer with concrete information about the severity of an information leakage.

International audience; To program parallel systems efficiently and easily, a wide range of programming models have been proposed, each with different choices concerning synchronization and communication between parallel entities. Among them, the actor model is based on loosely coupled parallel entities that communicate by means of asynchronous messages and mailboxes. Some actor languages provide a strong integration with object-oriented concepts; these are often called active object languages. This paper reviews four major actor and active object languages and compares them according to carefully chosen dimensions that cover central aspects of the programming paradigms and their implementation.

This paper presents a unified model for two complementary approaches of code reuse: Traits and Delta-Oriented Programming DOP. Traits are used to modularly construct classes, while DOP is a modular approach to construct Software Product Lines. In this paper, we identify the common structure of these two approaches, present a core calculus that combine Traits and DOP in a unified framework, provide an implementation for the ABS modelling language, and illustrate its application in an industrial modeling scenario.

We present a comprehensive model of railway operations written in the abstract behavioral specification (ABS) language. The model is based on specifications taken from the rulebooks of Deutsche Bahn AG. It is statically analyzable and executable, hence allows to use static and dynamic analysis within one and the same formalism. We are able to combine aspects of micro- and macroscopic modeling and provide a way to inspect changes in the rulebooks. We illustrate the static analysis capability by a safety analysis based on invariant reasoning that only relies on assumptions about the underlying railway infrastructure instead of explicitly exploring the state space. A concrete infrastructure layout and train schedule can be used as input to the model to examine dynamic properties such as delays. We illustrate the capability for dynamic analysis by demonstrating the effect that different ways of dealing with faulty signals have on delays.

In this article, the authors give an overview of tool-based verification of hardware and software systems and discuss the relation between verification and logical reasoning. Here, "verification"' refers to reasoning-based methods to establish dependability. This isn't restricted to proofs of functional correctness; it also includes other scenarios such as test generation and bug finding. The authors describe the main verification scenarios and methods that are in use today and the extent to which they depend on logical reasoning. From this discussion, they distill current trends and new opportunities for the interaction between verification and reasoning.

We demonstrate by a case study of an industrial distributed system how performance, resource consumption, and deployment on the cloud can be formally modeled and analyzed using the abstract behavioral specification language Real-Time ABS. These non-functional aspects of the system are integrated with an existing formal model of the functional system behavior, achieving a separation of concerns between the functional and non-functional aspects in the integrated model. The resource costs associated with execution in the system depend on the size of local data structures, which evolve over time; we derive corresponding worst-case cost estimations by static analysis techniques and integrate them into our resource-sensitive model. The model is further parameterized with respect to deployment scenarios which capture different application-level management policies for virtualized resources. The model is validated against the existing system's performance characteristics and used to simulate, analyze, and compare deployment scenarios on the cloud.

Feature-based approaches to software design, like delta-oriented programming, are well-suited to support multi-product software development paradigms, such as Software Product Lines. Currently, the popular UML notation does not support delta-oriented software design, so that several ad-hoc notations tend to be used. This paper presents a systematic approach to import concepts from delta-oriented programming into the mainstream notation UML. This is done with minimal overhead by specifying a new, slim, delta-oriented UML profile. It is compatible with languages that support delta-oriented programming such as DeltaJ and ABS. The usefulness of the profile is evaluated with a case study.

Theorem provers have highly complex interfaces, but there are not many systematic studies of their usability and effectiveness. Specifically, for interactive theorem provers the ability to quickly comprehend intermediate proof situations is of pivotal importance. In this paper we present the (as far as we know) first empirical study that systematically compares the effectiveness of different user interfaces of an interactive theorem prover. We juxtapose two different user interfaces of the interactive verifier KeY: the traditional one which focuses on proof objects and a more recent one that provides a view akin to an interactive debugger. We carefully designed a controlled experiment where users were given various proof understanding tasks that had to be solved with alternating interfaces. We provide statistical evidence that the conjectured higher effectivity of the debugger-like interface is not just a hunch.

The Symbolic Execution Debugger (SED) is an extension of the Eclipse debug platform for interactive symbolic execution. Like a traditional debugger, the SED can be used to locate the origin of a defect and to increase program understanding. However, as it is based on symbolic execution, all execution paths are explored simultaneously. We demonstrate an extension of the SED called Interactive Verification Debugger (IVD) for inspection and understanding of formal verification attempts. By a number of novel views, the IVD allows to quickly comprehend interactive proof situations and to debug the reasons for a proof attempt that got stuck. It is possible to perform interactive proofs completely from within the IVD. It can be experimentally demonstrated that the IVD is more effective in understanding proof attempts than a conventional prover user interface. A screencast explaining proof attempt inspection with the IVD is available at youtu.be/8e-q9Jf1h_w.

While correctness-by-construction and post-hoc verification are traditionally considered to provide two opposing views on proving software systems to be free from errors, nowadays numerous techniques and application fields witness initiatives that try to integrate elements of both ends of the spectrum. The ultimate aim is not merely to improve the correctness of software systems but also to improve their time-to-market, and to do so at a reasonable cost. This track brings together researchers and practitioners interested in the inherent 'tension' that is usually felt when trying to balance the pros and cons of correctness-by-construction versus post-hoc verification.

Symbolic execution is a software analysis technique that has been used with success in the past years in program testing and verification. A main bottleneck of symbolic execution is the path explosion problem: the number of paths in a symbolic execution tree is exponential in the number of static branches of the executed program. Here we put forward an abstraction-based framework for state merging in symbolic execution. We show that it subsumes existing approaches and prove soundness. The method was implemented in the verification system KeY. Our empirical evaluation shows that reductions in proof size of up to 80 % are possible by state merging when applied to complex verification problems; new proofs become feasible that were out of reach so far.

We propose to formally model requirements and interoperability constraints among components of a railway system to enable automated, incremental analysis and validation mechanisms. The goal is to provide the basis for a technology that can drastically reduce the time and cost for certification by making it possible to trace changes from requirements via design to implementation.

This chapter gives a systematic tutorial introduction on how to perform formal program verification with the KeY system. It illustrates a number of complications and pitfalls, notably programs with loops, and shows how to deal with them. After working through this tutorial, you should be able to formally verify with KeY the correctness of simple Java programs, such as standard sorting algorithms, gcd, etc.

The KeY System has been developed for over a decade. During this time, the field of Formal Methods as well as Computer Science in general has changed considerably. Based on an analysis of this trajectory of changes we argue why, after all these years, the project is still relevant and what the challenges in the coming years might be. At the same time we give a brief overview of the various tools based on KeY technology and explain their architecture.

We present a novel approach to automatically generate invariants for loops manipulating arrays. The intention is to achieve formal verification of programs over arrays without the need for user-specified loop invariants. Many loops iterate and manipulate collections. Finding useful, i.e., sufficiently precise invariants for those loops is a challenging task, in particular, if the iteration order is complex. Our approach partitions an array and provides an abstraction for each of these partitions. Symbolic pivot elements are used to compute the partitions. In addition we integrate a faithful and precise program logic for sequential Java programs with abstract interpretation using an extensible multi-layered framework to compute array invariants. The presented approach has been implemented. Results of experiments are reported.

Static analysis of software with deductive methods is a highly dynamic field of research on the verge of becoming a mainstream technology in software engineering. It consists of a large portfolio of - mostly fully automated - analyses: formal verification, test generation, security analysis, visualization, and debugging. All of them are realized in the state-of-art deductive verification framework KeY. This book is the definitive guide to KeY that lets you explore the full potential of deductive software verification in practice. It contains the complete theory behind KeY for active researchers who want to understand it in depth or use it in their own work. But the book also features fully self-contained chapters on the Java Modeling Language and on Using KeY that require nothing else than familiarity with Java. All other chapters are accessible for graduate students (M.Sc. level and beyond). The KeY framework is free and open software, downloadable from the book companion website which contains also all code examples mentioned in this book.

This chapter presents the usage and different use cases of the Symbolic Execution Debugger (SED), an interactive debugger based on symbolic execution. In addition, the extendable architecture of the SED and the underlying symbolic execution engine based on KeY are discussed.

We propose a new and systematic framework for proof reuse in the context of deductive software verification. The framework generalizes abstract contracts into incremental proof repositories. Abstract contracts enable a separation of concerns between called methods and their implementations, facilitating proof reuse. Proof repositories allow the systematic caching of partial proofs that can be adapted to different method implementations. The framework provides flexible support for compositional verification in the context of, e.g., partly developed programs, evolution of programs and contracts, and product variability.