Tutorial [] The KeY Approach to Deductive Verification of Object -Oriented Programs

Wolfgang Ahrendt, Bernhard Beckert, Reiner Hähnle, Philipp Rümmer, Peter H. Schmitt[2ex] Www.Key-Project.Org

Description

TutorialThe KeY Approach to Deductive Veri cationof Object-Oriented ProgramsWolfgang Ahrendt, Bernhard Beckert, Reiner Hahnle,Philipp Rummer, Peter H. Schmittwww.key-project.org5th International Symposium onFormal Methods for Components and ObjectsAmsterdam, NLNovember 9, 2006Deductive Veri cation of OO Programs: FMCO 2006 1 / 57What is this Tutorial all About?It is about an approach and tool for theDesignFormal specicationDeductive veri cationofOO softwareThe approach, tool, and project is namedin the following: ’KeY’Deductive Veri cation of OO Programs: Introduction FMCO 2006 2 / 57KeY Project PartnersChalmers UTUniversity of University ofG oteborgKarlsruhe (TH) Koblenz-LandauReiner HahnlePeter H. Schmitt Bernhard BeckertWolfgang AhrendtRichard Bubel Gerd BeusterDaniel LarssonSte en Schlager Christoph GladischPhilipp RummerIsabel Tonin Vladimir KlebanovAngela WallenburgDeductive Veri cation of OO Programs: Introduction FMCO 2006 3 / 57Some Buzzwords Early OnJava as target languageDynamic logic as program logicVeri cation = symbolic execution + inductionSequent style calculus + meta variables + incremental closureProver is interactive + automatedIntegration with two standard SWE tools:TogetherCC, a commercial CASE toolEclipse, an open extensible IDESpeci cation languagesJMLOCL/UMLSmart cards as main target applicationDeductive Veri cation of OO Programs: Introduction FMCO 2006 4 / 57Part IOverview of the KeY ...

Informations

• Publié par: Octey
• Nombre de lectures: 17
• Langue: English

Extrait

eD

Tutorial The KeY Approach to Deductive Verification of Object-Oriented Programs

ductiveV

WolfgangAhrendt,BernhardBeckert,ReinerHa¨hnle, PhilippRu¨mmer,PeterH.Schmitt

erificati

www.key-project.org

5th International Symposium on Formal Methods for Components and Objects

nofoOOrPorgma:s

Amsterdam, NL November 9, 2006

MFCO20061/57

ront:ImsnFioctdu26002OCM

It is about anapproachandtoolfor the Design Formal specification Deductive verification

in the following: KeY’ ’

Theapproach,tool, andprojectis named

What is this Tutorial all About?

75/ductDeerifiiveVnofoacitgoarOOrP

of

OO software

oducIntrams:rogrOfPOoioncfitaeVirvetiucedD

Bernhard Beckert Gerd Beuster Christoph Gladisch Vladimir Klebanov

University of Koblenz-Landau

KeY Project Partners

Chalmers UT G¨oteborg

ReinerH¨ahnle Wolfgang Ahrendt Daniel Larsson PhilippR¨ummer Angela Wallenburg

University of Karlsruhe (TH)

Peter H. Schmitt Richard Bubel Steffen Schlager Isabel Tonin

600275/3noitOCMF

ontiOOofogPrmsraudeDvitcreVeacfiiO20064/57

Some Buzzwords Early On

Javaas target language Dynamic logicas program logic Verification =symbolic execution+induction Sequent stylecalculus + meta variables + incremental closure Prover isinteractive+automated Integration with two standard SWE tools: TogetherCC, a commercial CASE tool Eclipse, an open extensible IDE Specification languages JML OCL/UML Smart cardsas main target application

I:tnorudtcoiFnCM

Deductive

Verification

Overview

of

OO

Programs:

Part

of

the

I

KeY

system

FMCO

2006

5

/

57

First

Demo

Deductive

Verification

of

OO

Programs:

First

Demo

FMCO

2006

6

/

57

067/57

Supported Specification Languages: OCL

ObjectConstraintLanguage

Part of the OMG standard UML

Scope: Add formal constraints to UML (class) diagrams

F:ritseDomMFOC02ontiOOofogPrmsraudeDvitcreVeacfii

edDtiucVeveficriioatOfonorPOmargiF:srstDemoFMCO200685/7

JavaModelingLanguage Behavioral interface specification language for Java

Supported Specification Languages: JML

Comes with assertion and runtime checkers

International community effort lead by Gary T. Leavens, Iowa State building on the Larch approach

ficriVevetiucedD

differences OCL model oriented: attached to class diagrams ‘talks’ UML JML implementation oriented: attached to Java programs ‘talks’ Java specifies exceptional behaviour also JML only: restricting scope of side effects

both specify method behaviour: pre/post conditions specify admissible states: class invariants essentially full first order support inter-object navigation

OCL and JML

960075/emoFMCO2s:FirstDPOorrgmataoionOf

JML example /*@public normal_behavior @requiresa !=null; @ensures(\forall intj; j >= 0 && j < a.length; @\result>= a[j]); @ensuresa.length > 0 ==> @(\exists intj; j >= 0 && j < a.length; @\result== a[j]); @*/ public static/*@pure@*/intmax(int[] a) { if( a.length == 0 )return0; intmax = a[0], i = 1; while( i < a.length ) { if( a[i] > max ) max = a[i]; ++i; } returnmax; } Deductive Verification of OO Programs: First Demo FMCO 2006 10 / 57

KeY

Architecture

Deductive

Verification

of

OO

Programs:

First

Demo

FMCO

2006

11

/

57