Seminar: Modellbasierte Software-Verifikation: Grundlagen und industrielle Praxis

Lehrstuhl Technische Informatik
Dozenten Prof. Dr. habil. Kropf
Dr. Ruf
Betreuer Dr. Ruf
Dr. Lämmermann
Dr. Lettnin
Prof. Dr. habil. Kropf
Heckeler
Vorbesprechung         30.04.2009, 17:00 Uhr, A104
Umfang 2 SWS / 4 LP
PrĂĽfungsfach      Technische Informatik
Eintrag im LSF Modellbasierte Software-Verifikation: Grundlagen und industrielle Praxis

Beschreibung

Zuverlässigkeit, Sicherheit, Korrektheit und Robustheit von Software werden immer wichtiger. Immer wieder treten Fehler auf, darunter auch kritische, die auf gedanklich-logische Irrtümer in Spezifikation und Implementierung der Software zurückzuführen sind. Dabei spielen Compiler und Systemsoftware eine ebenso wichtige Rolle wie die verwendeten Softwaretechniken und Programmiersprachen. Zur Vermeidung von Fehlern werden die verwendeten Sprachen oft in den erlaubten Sprachkonstrukten eingeschränkt, um z.B. dynamische Fehlfunktionen (Speicherüberläufe, Speicherlecks u.ä.) zu verhindern, aber auch, um die Analyse und Verifikation zu vereinfachen.
Die Verifikations-Techniken reichen dabei von der statischen Analyse der Programme und deren  Spezifikation bis hin zu Kombinationen aus maschinellen Beweissystemen und Model-Checkern. Neben Fehlervermeidung ist auch Fehlertoleranz (z.B. durch Redundanz, Mehrfachauslegung) fĂĽr Software ein interessanter Ansatz. Dazu werden Techniken, wie LaufzeitprĂĽfung, Beobachterprozesse, Monitoring, KonsistenzprĂĽfung eingesetzt.
Mehr und mehr stehen Qualitätsprüfung und die Garantie zur Einhaltung von Eigenschaften bei Software im Vordergrund. Ein Beispiel wäre z.B. die Zertifizierung sicherheitsrelevanter Systeme. In diesem Zusammenhang sind auch Bibliotheken, Werkzeuge, Compiler, Systemkomponenten und Fremdsoftware von Bedeutung, für die die Hersteller ebenfalls verantwortlich sind. Die Beherrschung dieser komplexen Zusammenhänge ist nicht nur für Systeme relevant, von denen Gefahr für Leib und Leben von Menschen ausgeht, sondern auch bei wirtschaftlichem Gefahrenpotential Software-basierter Systeme, z.B. im Bereich der Security.

Ziel dieses Seminars ist es einen Einblick in die Theorie der Software-Verifikation und die aktuellen, in der Forschung entwickelten, Tools zu geben, ohne den Fokus auf die heute eingesetzten industriellen Methoden zu verlieren.

Die Dozenten haben einschlägige Erfahrungen im Entwurf und der Verifikation von Systemen im industriellen Umfeld.

 

Themenvergabe:

Die Themenvergabe erfolgt am 30.04.2009. AuĂźerdem werden an diesem Tag auch die weiteren Termine fĂĽr das Block-Seminar bekanntgegeben.

Bemerkung

Randbedingungen fĂĽrs Seminar

Von den Teilnehmerinnen und Teilnehmnern wird eine weitgehend selbstständige Erarbeitung des jeweiligen Themengebiets incl. Literaturbeschaffung und -recherche erwartet. Literaturhinweise werden natürlich gegeben, eine bedarfsgesteuerte Betreuung ist sichergestellt.

Vortragsdauer und Themenaufbau

Der Vortrag soll einen Dauer von 25 Minuten haben und folgenden Aufbau besitzen:

  • Einleitung mit Motivation (ca. 5 Minuten im Vortrag)
  • Theorie zum jeweiligen Thema (ca. 10-15 Minuten im Vortrag)
  • Praktische Anwendung / Fallbeispiele (restliche Zeit, mind. 5. Minuten)
  • Zusammenfassung (2 Minuten im Vortrag)

Bedingungen fĂĽr den Seminarschein / Benotung

Um den Schein zu erhalten muss

  • eine Vortragsgliederung 4 Wochen vor dem Vortragstermin mit dem Betreuer durchgesprochen sein
  • eine erste Vortragsversion 2 Wochen vor dem Vortragstermin mit dem Betreuer durchgesprochen sein (vorzugsweise PowerPoint oder PDF)
  • ein Vortrag (25 Minuten + Diskussion) gehalten werden
  • eine schriftliche Ausarbeitung abgegeben werden (5-10 Seiten in PostScript- oder PDF-Format)
  • bei allen Seminarterminen anwesend sein

Die Seminarleistung wird auf Wunsch benotet. Zur Bewertung werden folgende Kriterien herangezogen:

  • Einhaltung der Termine
  • Qualität der durchgefĂĽhrten Literaturrecherche
  • Inhaltliche Qualität des Vortrags
  • Qualität der Präesntation incl. Zeiteinhaltung
  • Qualität der Ausarbeitung
  • Grad der Sebstständigkeit (davon unberĂĽhrt sind natĂĽrlich Diskussionen mit dem Betreuer ĂĽber Auswahl der zu präsentierenden Themen, Eignung zur Präsentation etc. - solche Diskussionen sind sogar explizit erwĂĽnscht)

Themen

Nr.

Titel

Abstract

1

A Comparative Study of Industrial Static Analysis Tools

Tools based on static analysis can be used to find defects in programs. Tools that do shallow analyses based on pattern matching have existed since the 1980's and although they can analyze large programs they have the drawback of producing a massive amount of warnings that have to be manually analyzed to see if they are real defects or not. Recent technology advances has brought forward tools that do deeper analyses that discover more defects and produce a limited amount of false warnings. These tools can still handle large industrial applications with millions lines of code. This article surveys the underlying supporting technology of three state-of-the-art static analysis tools. The survey relies on information in research articles and manuals, and includes the types of defects checked for (such as memory management, arithmetics, security vulnerabilities), soundness, value and aliasing analyses, incrementality and IDE integration. This survey is complemented by practical experiences from evaluations at the Ericsson telecom company.

2

A Formal Model of Memory Peculiarities for the Verification of Low-Level Operating-System Code

This paper presents our solutions to some problems we encountered in an ongoing attempt to verify the micro-hypervisor currently developed within the Robin project. The problems that we discuss are (1) effcient automatic reasoning for type-correct programs in virtual memory, and (2) modeling memory-mapped devices with alignment requirements. The discussed solutions are integrated in our verification environment for operating-system kernels in the interactive theorem prover PVS. This verification environment will ultimately be used for the verification of the Robin micro-hypervisor. As a proof of concept we include an example verification of a very simple piece of code in our environment.

3

Specification of Conditions for Error Diagnostics

This paper describes the basic concepts of error diagnostics and an associated rule system whose application helps to identify potential hardware/software locations of errors which caused a failure observed while executing tests of embedded systems. Further on, an overview over the "Avionics Smoke Detection System" is given, where the main algorithms have been applied. The methods, techniques and tools described here rely on the preceding investigations performed with respect to signal flow and the observation of causal chains in distributed test benches during test suite executions. These results have been elaborated in the KATO project within the German aerospace research programme LUFO III.

4

Symbolic and Abstract Interpretation for C/C++ Programs

We present a construction technique for abstract interpretations which is generic in the choice of data abstractions. The technique is specialised on C/C++ code, internally represented by the GIMPLE control flow graph as generated by the gcc compiler. The generic interpreter handles program transitions in a symbolic way, while recording a history of symbolic memory valuations. An abstract interpreter is instantiated by selecting appropriate lattices for the data types under consideration. This selection induces an instance of the generic transition relation. All resulting abstract interpretations can handle pointer arithmetic, type casts, unions and the aliasing problems involved. It is illustrated how switching between abstractions can improve the efficiency of the verification process. The concepts described in this paper are implemented in the test automation and static analysis tool RT-Tester which is used for the verification of embedded systems in the fields of avionics, railways and automotive control.

5

Proving Correctness of an Efficient Abstraction for Interrupt Handling

This paper presents an approach to the efficient abstraction of interrupt handling in microcontroller systems. Such systems usually operate in uncertain environments, giving rise to a high degree of nondeterminism in the corresponding formal models, which in turn aggravates the state explosion problem. Careful handling of nondeterminism is therefore crucial for obtaining efficient model checking tools. Here, we support this goal by developing a formal computation model and an abstraction method, called interrupt nondeterminism, which instantiates nondeterministic values only if and when this is required by the application code. It is shown how this symbolic technique can be integrated into our explicit CTL model checking tool [mc]square by introducing lazy states. A lazy state consists of explicit and symbolic parts and therefore, represents several concrete states. With regard to interrupt handling, we also give a simulation relation between the concrete and the abstract state space, thus establishing the correctness of our technique. Furthermore, a case study is presented in which three different programs are used to demonstrate the effectiveness of our method.

6

[mc]square: A Model Checker for Microcontroller Code

The paper presents details of a model checker for microcontroller-based embedded systems, called [mc]square. The purpose of the tool is to make model checking technology applicable in an embedded systems industry context. Consequently, it does not implement new theory but combines existing techniques to achieve the necessary efficiency and usability in a novel application area. One of the pragmatic requirements has been that model checking must be possible without any kind of manual preprocessing of the code. In its core, [mc]square is an explicit state, CTL model checker which builds the state space from the hardware-specific assembly code. The paper describes the tool features in detail and illustrates its abilities using two realistic examples.

7

ACSL: ANSI C Specification Language

This document is a reference manual for ACSL, an acronym for “ANSI C Specification Language”. This is a Behavioral Interface Specification Language (a.k.a. BISL) implemented in the F RAMA -C framework. As suggested by its name, it aims at specifying behavioral properties of C source code. The main inspiration for this language comes from the specification language of the C ADUCEUS tool [8, 9] for deductive verification of behavioral properties of C programs. It is itself inspired from the Java Modeling Language (JML [17]) which aims at similar goals for Java source code: indeed it aims both at runtime assertion checking and static verification using the ESC/JAVA 2 tool [13], where we aim at static verification and deductive verification (see Appendix A.2 for a detailed comparison between ACSL and JML). Going back further in history, JML design was guided by the general design-by-contract principle proposed by Bertrand Meyer, who took his own inspiration from the concepts of preconditions and postconditions on a routine, going back at least to Dijkstra, Floyd and Hoare in the late 60’s and early 70’s, and originally implemented in the E IFFEL language. In this document, we assume that the reader has a good knowledge of the ANSI C programming language [12, 11].

8

The software model checker BLAST

Blast is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, Blast either statically proves that the program satisfies the safety property, or provides an execution path that exhibits a violation of the property (or, since the problem is undecidable, does not terminate). Blast constructs, explores, and refines abstractions of the program state space based on lazy predicate abstraction and interpolation-based predicate discovery. This paper gives an introduction to Blast and demonstrates, through two case studies, how it can be applied to program verification and test-case generation. In the first case study, we use Blast to statically prove memory safety for C programs. We use CCured, a type-based memory-safety analyzer, to annotate a program with run-time assertions that check for safe memory operations. Then, we use Blast to remove as many of the run-time checks as possible (by proving that these checks never fail), and to generate execution scenarios that violate the assertions for the remaining run-time checks. In our second case study, we use Blast to automatically generate test suites that guarantee full coverage with respect to a given predicate. Given a C program and a target predicate p, Blast determines the program locations q for which there exists a program execution that reaches q with p true, and automatically generates a set of test vectors that cause such executions. Our experiments show that Blast can provide automated, precise, and scalable analysis for C programs.

9

A Tool for Checking ANSI-C Programs

We present a tool for the formal verification of ANSI-C programs using Bounded Model Checking (BMC). The emphasis is on usability: the tool supports almost all ANSI-C language features, including pointer constructs, dynamic memory allocation, recursion, and the float and double data types. From the perspective of the user, the verification is highly automated: the only input required is the BMC bound. The tool is integrated into a graphical user interface. This is essential for presenting long counterexample traces: the tool allows stepping through the trace in the same way a debugger allows stepping through a program.

10

JML: A Notation for Detailed Design

JML is a behavioral interface specification language tailored to Java. It is designed to be written and read by working software engineers, and should require only modest mathematical training. It uses Eiffel-style syntax combined with model-based semantics, as in VDM and Larch. JML supports quantifiers, specification-only variables, and other enhancements that make it more expressive for specification than Eiffel and easier to use than VDM and Larch. JML [Leavens-Baker-Ruby01], which stands for “Java Modeling Language,” is a behavioral interface specification language (BISL) [Wing87] designed to specify Java [Arnold- Gosling98] [Gosling-Joy-Steele96] modules. Java modules are classes and interfaces. A behavioral interface specification describes both the details of a module’s interface with clients, and its behavior from the client’s point of view. Such specifications are not good for the specification of whole programs, but are good for recording detailed design decisions or documentation of intended behavior, for a software module. The goal of this chapter is to explain JML and the concepts behind its approach to specification. Since JML is used in detailed design of Java modules, we use the detailed design of an interface and class for priority queues as an example. The rest of this section explains interfaces and behavioral interface specification. In the next section we describe how to specify new types as conceptual models for detailed design. Following that we finish the example by giving the details of a class specification. We conclude after mentioning some other features of JML.

11

Bounded Model Checking of Concurrent Programs

We propose a SAT-based bounded verification technique, called TCBMC, for threaded C programs. Our work is based on CBMC, which models sequential C programs in which the number of executions for each loop and the depth of recursion are bounded. The novelty of our approach is in bounding the number of context switches allowed among threads. Thus, we obtain an efficient modeling that can be sent to a SAT solver for property checking. We also suggest a novel technique for modeling mutexes and Pthread conditions in concurrent programs. Using this bounded technique, we can detect bugs that invalidate safety properties. These include races and deadlocks, the detection for which is crucial for concurrent programs.

12

Temporal Properties Verification of System Level Design

In this paper, we propose a new approach to integrate temporal assertions in system level design of real time systems. To achieve this, one should have more abstract mechanisms to evaluate the assertions and one should check more abstract structures of the design. Satisfying these needs, it becomes possible to include assertions in hardware as well as in software modules, enabling the verification at the system level. Afterwards, during system refinements it will also be possible to reuse the same assertions at lower levels of abstraction, reducing the time of verification of the systems. Nowadays, between 40-70% of the design time is consumed to locate and correct the design errors. To exemplify our approach, we have verified temporal properties in modules of a digital video broadcasting real time system.

13

Efficient and Customizable Integration of Temporal Properties into SystemC

In this paper we describe our enhanced extension of SystemC with temporal properties. The two main tasks involved are synthesis of checker automata corresponding to given temporal logics formulae and integration of property specification into the SystemC framework. For synthesis of checker automata we rely on an intermediate language (IL) that is directly generated from PSL or FLTL properties in a bottom-up fashion. IL can either be translated to native code in a preprocessing step or it can be executed directly in a simple virtual machine. Our temporal SystemC checker supports both alternatives. Properties can be added dyamically any time during simulation. A dedicated observer process is responsible for checking all active properties continuously against the current system state during simulation. The actual executing property checkers can be customized according to the users needs. When special states are reached, i.e. finding a validation or violation of the property, a policy class dispatches to user-defined action handlers.

14

SymC - A Symbolic Bounded Property Checker

Bugs in hardware cost money. Whenever an error creeps into a design, time and money must be spent to locate the problem and correct it. With the growing complexity of digital systems, and the tremendous pressure for early-time-to- market schedules, the need for verification tools that can help designers catch bugs at an early stage in the design process cannot be overemphasized. However, as per statistics verification takes nearly 75% of the design time. Traditional methods of verification are empirical in nature and are based on extensive simulation of hand-written or automatically generated diagnostic test vectors. Although provably effective in early stages of the debugging process, their effectiveness drops quickly along the maturity of the design. Hence, func- tional verification has problems in catching the corner cases, therefore the formal verification complements it in order to cope up with the design growth. In the formal verification approach efficient search procedures are used to automatically determine if the state space of a design satisfies an abstract logical specification (properties). In general reachability analysis is known to be a key component of formal verification. For large classes of properties, verification can be reduced to reachability analysis. The term reachability analysis corresponds to the set of states that can be reached by means of traversal step from a set of defined initial states. The typical problem of such analysis is beyond some steps of traversal, the system can not handle the overwhelming state space and hence the memory overflow problem. There is constant work on finding algorithms to reduce the memory requirement bottlenecks. One such approach to reduce the memory requirement is symbolic reachability analysis, where Binary Decision Diagrams (BDDs) are used as data structures to represent the state space. However, large designs may require many millions of BDD nodes that often causes memory overflow. This phenomenon is well known as BDD blow-up. There are several proposed solutions to deal with the large memory requirements of BDDs. The first novel proposal is to avoid the traditional fix-point iteration and the other is to have a bounded steps of traversal. This two proposals are realized in symbolic means by the tool SymC. This manual gives the user a clear picture of how the verification engine of SymC works and the syntax and the command line options.

15

Interactive Verification of UML State Machines

We propose a new technique for interactive formal verification of temporal properties of UML state machines. We introduce a formal, operational semantics of UML state machines and give an overview of the proof method which is based on symbolic execution with induction. Usefulness of the approach is demonstrated by example of an automatic teller machine. The approach is implemented in the KIV system.