Deductive Verification Based Abstraction for Software Model Checking

• The research community working on formal software verification has historically evolved into two main camps, grouped around two verification methods that are typically referred to as Deductive Verification and Model Checking. In this paper, we present an approach that applies deductive verification to formally justify abstract models for model checking in the TLA framework. We present a proof-of-concept tool chain for C programs, based on Frama-C for deductive verification and TLA+ for model checking. As a theoretical foundation, we summarise a previously developed abstract contract theory as a framework for combining these two methods. Since the contract theory adheres to the principles of contract based design, this justifies the use of the approach in a real-world system design setting. We evaluate our approach on two case studies: a simple C program simulating opening and closing of files, as well as a C program based on real software from the automotive industry.

Ämnesord

NATURVETENSKAP  -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Sciences -- Computer Sciences (hsv//eng)

Nyckelord

Contracts

Deductive verification

Model checking

Publikations- och innehållstyp

ref (ämneskategori)

kon (ämneskategori)