Diploma Thesis - KITlfm.iti.kit.edu/download/DAScheben.pdf · Diploma Thesis Veriﬁcation of Sun...

Diploma Thesis

Verification of Sun SPOT’s Network Library

University of Karlsruhe (TH)Faculty of Computer Science

Institute of Theoretical Computer Science

Christoph Scheben

May 30, 2008

Supervising Tutors:

Prof. P. H. Schmitt, Benjamin Weiß, Frank Werner

Erklärung der Selbstständigkeit

Hiermit versichere ich, die vorliegende Arbeit selbstständig verfasst und keine anderenals die angegebenen Quellen und Hilfsmittel benutzt sowie Zitate deutlich kenntlichgemacht zu haben.

Karlsruhe, den 30. Mai 2008 Christoph Scheben

Acknowledgment

I would like to thank all people who supported me with my diploma thesis. Specialthanks go to my supervising tutors Frank Werner and Benjamin Weiß. They alwayshad time for discussions and responded immediately to all of my questions and prob-lems. As well, I’d like to thank Prof. P. H. Schmitt. Despite all his duties, he found thetime for intensive discussions and guided my thesis to the right direction. Finally, spe-cial thanks go to my family who supported me in various ways and to all proofreadersfor their helpful comments.

Thanks a lot to all of you!

Contents

1 Introduction 1

2 Foundations 3

2.1 JML . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32.1.1 Method contracts . . . . . . . . . . . . . . . . . . . . . . . . . . 42.1.2 Invariants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72.1.3 Further specification entities . . . . . . . . . . . . . . . . . . . 8

2.2 Program correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82.3 KeY . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

2.3.1 JavaDL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102.3.2 Sequences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112.3.3 Updates . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112.3.4 Modifier sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112.3.5 Using KeY . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122.3.6 Lemmata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

3 Survey of the network library 17

3.1 Design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 173.2 Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

4 Case study 27

4.1 General aspects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 274.1.1 Extent of the case study . . . . . . . . . . . . . . . . . . . . . . 284.1.2 KeY version and settings . . . . . . . . . . . . . . . . . . . . . 28

4.2 Verification strategy . . . . . . . . . . . . . . . . . . . . . . . . . . . . 294.2.1 Method verification order . . . . . . . . . . . . . . . . . . . . . 294.2.2 Proof obligation system . . . . . . . . . . . . . . . . . . . . . . 30

4.3 Achieving observed state correctness and problems related to it . . . . 314.3.1 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 324.3.2 Achieving observed state correctness . . . . . . . . . . . . . . . 324.3.3 Problems with the old JML translation . . . . . . . . . . . . . 324.3.4 Book-keeping of the invariant usages . . . . . . . . . . . . . . . 344.3.5 A problem with the strategy “Contracts” . . . . . . . . . . . . 34

ii Contents

4.3.6 Using a contract for the verification of itself . . . . . . . . . . . 364.4 The problem with bit operations and a verification example . . . . . . 37

4.4.1 The lemmata system . . . . . . . . . . . . . . . . . . . . . . . . 374.4.2 Verification example . . . . . . . . . . . . . . . . . . . . . . . . 40

4.5 Further problems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 504.5.1 The strategy “Contracts” . . . . . . . . . . . . . . . . . . . . . 504.5.2 Problems regarding the clause “assignable \nothing;” . . . 504.5.3 Strongly splitting proofs . . . . . . . . . . . . . . . . . . . . . . 544.5.4 Domains of numbers . . . . . . . . . . . . . . . . . . . . . . . . 574.5.5 Proof management . . . . . . . . . . . . . . . . . . . . . . . . . 574.5.6 Incorrect specifications . . . . . . . . . . . . . . . . . . . . . . . 584.5.7 Labeling of invariants and method contracts . . . . . . . . . . . 594.5.8 Additional features which could be useful . . . . . . . . . . . . 59

4.6 Strengths of KeY . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59

5 Conclusion 61

A Lemmata 63

A.1 General bit lemmata . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63A.1.1 Zero simplification lemmata . . . . . . . . . . . . . . . . . . . . 63A.1.2 Commutation lemmata . . . . . . . . . . . . . . . . . . . . . . 64A.1.3 Fusion lemmata . . . . . . . . . . . . . . . . . . . . . . . . . . . 69A.1.4 Estimation lemmata . . . . . . . . . . . . . . . . . . . . . . . . 74A.1.5 Comparison lemmata . . . . . . . . . . . . . . . . . . . . . . . 77

A.2 Resolution bit lemmata . . . . . . . . . . . . . . . . . . . . . . . . . . 78A.2.1 Translation lemmata . . . . . . . . . . . . . . . . . . . . . . . . 79A.2.2 Commutation lemmata . . . . . . . . . . . . . . . . . . . . . . 82A.2.3 Resolution lemmata AND . . . . . . . . . . . . . . . . . . . . . 82A.2.4 Resolution lemmata OR . . . . . . . . . . . . . . . . . . . . . . 87A.2.5 Direct resolution lemmata . . . . . . . . . . . . . . . . . . . . . 92A.2.6 Resolution lemmata twoToThePowerOf . . . . . . . . . . . . . 96A.2.7 Misk bit lemmata . . . . . . . . . . . . . . . . . . . . . . . . . 98

A.3 Additional bit lemmata . . . . . . . . . . . . . . . . . . . . . . . . . . 98

Bibliography 103

CHAPTER 1

Introduction

Although the need for verified software has always been around, verification has notyet become an integral part of the standard software engineering process. Thus onepart of the latest development in the field of software verification is the attempt tointegrate software verification into the (standard) software engineering process andmake it applicable to more and more industrial applications (⇒ [Bec07, chapter 1]).

This thesis contributes to this research area by examining which problems actuallyoccur when applying software verification to already existing commercial software. Forthis purpose part of a Java application developed by Sun Microsystems Laboratories—the network library of Sun’s Sun SPOTs—has been verified. The library has beenspecified with the popular formal specification language JML [Lea06, Bur05, Lea08]and afterwards verified with the KeY system [Bec07].

In the remainder of this chapter a short overview will be given on what Sun SPOTsare. Chapter 2 shortly introduces JML and KeY as well as some foundations onprogram verification in general. Chapter 3 gives an overview of the design and imple-mentation of the network library while chapter 4 contains the case study itself. Thethesis concludes with a summary followed by an overview of related work in chapter 5.

Sun SPOTs

Sun SPOTs are small mobile computers with a wireless network interface and somesensors attached. They are developed by Sun Microsystems Laboratories, where thefirst part of their name comes from. The second part, SPOT, is an abbreviationfor “Small Programmable Object Technology”. Sun itself describes them as follows[Sun08c]:

“We’ve created an experimental platform to inspire developers to buildthe next great toy, sensor, communication device—who knows—using Suntechnology. Our Sun SPOT devices make include a flexible hardware plat-form as well as the software and tools to make it easy to innovate, experi-ment, and prototype whatever a developer can imagine.”

And further on:

2 1 Introduction

Figure 1.1: The assembly of a Sun SPOT.

“The Sun SPOT Device is a small, wireless, battery powered experimen-tal platform. It is programmed almost entirely in Java to allow regularprogrammers to create projects that used to require specialized embed-ded system development skills. The hardware platform includes a range ofbuilt-in sensors as well as the ability to easily interface to external devices.”

Figure 1.1 shows the assembly of a Sun SPOT. The Sun SPOT’s dimensions are71.00mm × 42.40mm × 18.00mm . Thus, they are a little bit smaller than typicalmobile phones.

Sun SPOTs run the Java-Virtual-Machine “Squawk”. Squawk complies to Sun’s“Connected Limited Device Configuration (CLDC) 1.1” [Sun08a]. Like Sun pointsout in [Sun08a], “CLDC defines the base set of application programming interfacesand a virtual machine for resource-constrained devices like mobile phones, pagers, andmainstream personal digital assistants”. It is remarkable in this context that thoughSquawk is a Java-Virtual-Machine for resource-constrained devices Squawk itself iswritten in Java as far as possible, too. Consequently, great parts of the Sun SPOT’slibraries are written in Java as well. This is important to note, because KeY is adeductive verification system for the programming language Java. Thus, the fact thatespecially the network library is written almost entirely in Javaenables the verificationof the library with KeY.

Readers interested in Sun SPOTs may visit the homepage of the Sun SPOT Project[Sun08b] and / or the homepage of the Squawk Project [Sun08d] for further informa-tion.

CHAPTER 2

Foundations

This chapter introduces briefly the most important aspects of JML and gives somenotes on

• what is considered to be a correct program,

• what proof obligations have to be shown with KeY to achieve this kind of pro-gram correctness and

• what else has to be known about KeY to be able to follow the discussions of thisthesis.

It will be assumed that readers are familiar with Java as well as with first-orderpredicate logic.

2.1 JML

The JML tutorial by Leavens and Cheon [Lea06] introduces JML as follows:

“JML stands for ‘Java Modeling Language’. It is a formal behavioralinterface specification language for Java. As such it allows one to specifyboth the syntactic interface of Java code and its behavior. [...] JML usesJava’s expression syntax to write the predicates used in assertions, suchas pre- and postconditions and invariants. [...] However, Java expressionslack some expressiveness that makes more specialized assertion languagesconvenient for writing behavioral specifications. JML solves this problemby extending Java’s expressions with various specification constructs, suchas quantifiers. [...] JML incorporates many ideas and concepts from model-oriented specification languages, which allows one to write specificationsthat are suitable for formal verification.”

4 2 Foundations

JML specifications are incorporated directly to the Java source code using a specialkind of comment. They have to be enclosed in special annotation characters to distin-guish them from normal Java comments. These “annotation” comments conform tothe syntax /*@ · @*/ or //@ · .

JML can be used as design by contract (DBC) style specification language. UsingJML for this purpose, one mainly makes use of two specification entities: methodcontracts and invariants. These will be considered in the following two sections. Sec-tion 2.1.3 gives some notes on further specification entities.

2.1.1 Method contracts

Method contracts specify the behavior of methods. They normally consist of a pre-condition, a post-condition and an assignable-clause. A method contract mct of thiskind states that, if the pre-condition of mct is valid in the pre-state of the invocationof the associated method m, then m guarantees that the post-condition of mct holdsafter the invocation of m and that at most the locations listed in its assignable-clauseare modified. A pre-condition is specified via the keyword “requires” followed by apredicate—in the context of JML this is an expression which evaluates to boolean—andfinally a semicolon. Such a specification will be called requires-clause. A post-conditionis specified equivalently to a pre-condition but with the keyword “ensures” instead of“requires”. Such a specification will be called ensures-clause. Finally, an assignable-clause is specified via the keyword “assignable” followed by a comma separated listof locations and a semicolon. Listing 2.1 shows a first simple example of a methodcontract in JML.

The contract of listing 2.1 starts with a publicity modifier and the keyword “normal-

_behavior” not mentioned so far. The publicity of a contract is normally the sameas the one of its method and thus won’t be discussed further. Details regardingpublicity modifiers can be found in [Lea06], [Bec07, chapter 5] or [Lea08]. The key-word “normal_behavior” specifies that the method will terminate normally if thepre-condition of the contract is fulfilled.

Abrupt termination can be specified using the keyword “exceptional_behavior”.In this case it has to be specified which exceptions can be thrown within a signals-only-clause. A signals-only-clause consists of the keyword “signals_only” followed by acomma separated list of exceptions and finally a semicolon. Additionally, for each ofthe listed exceptions a signals-clause should be specified. Such a clause starts with thekeyword “signals” followed by an exception enclosed in perentheses, a predicate andfinally a semicolon. The signals-clause states which conditions hold if the particularexception is thrown. A contract specified as exceptional_behavior normally doesn’tcontain an (explicit) ensures-clause. A simple example for a contract specifying anexceptional_behavior is shown in listing 2.2. In this context the assignable-clause“assignable \nothing;” indicates that no location will be altered.

A method contract may have more than one requires-clause as well as more thanone ensures-clause. In such cases the pre-condition is the conjunction of all requires-clauses and the post-condition is the conjunction of all ensures-clauses. Additionally,

2.1 JML 5

1 /*@ public normal_behavior

2 @ requires 0 <= outgoingHops

3 @ && outgoingHops <= Integer. MAX_VALUE;

4 @ ensures getOutgoingHops() == outgoingHops;

5 @ assignable hops;

6 @*/

7 public void setOutgoingHops(int outgoingHops) {

8 this.hops = outgoingHops;

9 }

Listing 2.1: Simple example of a method contract in JML.

1 /*@ public exceptional_behavior

2 @ requires sourceAddressOffset == -1;

3 @ signals_only IllegalStateException;

4 @ signals ( IllegalStateException) true;

5 @ assignable \ nothing;

6 @*/

7 public void setSourceAddress(long addr) {

8 if ( sourceAddressOffset == -1) {

9 throw new IllegalStateException(" Field not valid for

this packet ");

10 }

11 setLongAt(sourceAddressOffset , addr);

12 }

Listing 2.2: Simple example of a method contract which specifies anexceptional_behavior. Of course, this contract is not a complete specification ofthe method setSourceAddress(·) nor is it part of the specification used in the casestudy. However, the intention of this example is to give a simple example of a methodcontract which specifies an exceptional_behavior—and not to discuss details whichunnecessarily complicate the example.

a method may have more than one contract, which will usually occur if a method canterminate abruptly. In this case its normal behavior as well as its exceptional behaviorwill be specified by two different contracts as shown in listing 2.3.

This more complex specification uses the following additional keywords:

• \result: This keyword refers to the return value of the method.

• (\forall T x; exp1; exp2): This expression quantifies over all elements oftype T. It evaluates to true iff the expression exp1 ==> exp2 evaluates to truefor all x ∈ T.

6 2 Foundations


2 @ requires offsetsInitialised == true;

3 @ requires 0 <= destinationAddressOffset;

4 @ ensures ( getFrameControl() & DST_ADDR_BITS)

5 @ == DST_ADDR_16

6 @ ==> ( 0 <= \ result

7 @ && \result <= (( long)1 < <(8*Utils. SIZE_OF_SHORT)) -1

8 @ && (\forall int i;

9 @ 0 <= i && i < Utils. SIZE_OF_SHORT;

10 @ (((( long) 255) << (8 * i)) & \result )

11 @ == (( long)(buffer [ destinationAddressOffset+i]

12 @ & 255) << (8 * i))));

13 @ ensures ! ( ( getFrameControl() & DST_ADDR_BITS)

14 @ == DST_ADDR_16)

15 @ ==> ( Long. MIN_VALUE <= \ result

16 @ && \result <= Long. MAX_VALUE

17 @ && (\forall int i;

18 @ 0 <= i && i < Utils. SIZE_OF_LONG;

19 @ (((( long) 255) << (8 * i)) & \result )

20 @ == (( long)(buffer [ destinationAddressOffset+i]

21 @ & 255) << (8 * i))));


23 @ also

24 @ public exceptional_behavior

25 @ requires destinationAddressOffset == -1;




29 @*/

30 public /*@ pure @*/ long getDestinationAddress() {

31 if ( destinationAddressOffset == -1) {

32 throw new IllegalStateException("Field not valid for

this packet");

33 }

34 long result = 0;

35 if (( getFrameControl() & DST_ADDR_BITS) == DST_ADDR_16) {

36 result = getShortAt( destinationAddressOffset);

37 } else {

38 result = getLongAt( destinationAddressOffset );

39 }

40 return result ;

41 }

Listing 2.3: A more complex example for a JML specification of a method.

2.1 JML 7

1 /*@ private normal_behavior

2 @ requires lph != null;

3 @ requires rp. offsetsInitialised;

4 @ requires 0 <= rp. payloadOffset;

5 @ requires 0 <= parseIndex;

6 @ requires parseIndex

7 @ < rp. buffer. length -2 - rp. getPayloadOffset();

8 @ ensures rp. getMACPayloadAt(\ old( parseIndex))

9 @ == LowPanHeader. DISPATCH_LOWPAN_BC0;

10 @ ensures rp. getMACPayloadAt(\ old( parseIndex) + 1)

11 @ == (byte)( lph. getOutgoingBCastSeqNo () & 255);

12 @ ensures bCastIndex == \old( parseIndex) + 1;

13 @ ensures parseIndex == \old( parseIndex) + 2;

14 @ assignable bCastIndex , parseIndex ,

15 @ rp. buffer[ parseIndex+rp. getPayloadOffset()..

parseIndex+rp. getPayloadOffset() +1];

16 @*/

17 private void writeBroadcastHeader( LowPanHeader lph) {

18 rp. setMACPayloadAt( parseIndex++, LowPanHeader.

DISPATCH_LOWPAN_BC0);

19 bCastIndex = parseIndex;

20 rp. setMACPayloadAt( parseIndex++, (byte)(lph.

getOutgoingBCastSeqNo () & 0xff));

21 }

Listing 2.4: Example of an JML specification with the keyword \old(·).

• pure: This keyword specifies that a method has no side effects. If a method isused in another JML specification, it may not have side effects and thus has tobe specified as pure.

Additionally, the keyword \old(·) is often important to be able to express particularstatements. It can be used in post-conditions to refer to the evaluation of an expressionaccording to the pre-state of the method invocation (cp. listing 2.4).

These are only the most important keywords and clauses regarding method con-tracts. A more detailed introduction can be found in [Lea06] or [Bec07, chapter 5].The complete specification can be found in [Lea08].

2.1.2 Invariants

Since JML specifications are written to the Java source code, invariants have to bedefined in classes and / or interfaces, too—though they apply universally to the wholeprogram. JML provides two kinds of invariants, so-called static invariants and instanceinvariants.

8 2 Foundations

A static invariant is specified via the keywords “static invariant” followed bya predicate and finally a semicolon. It states that the predicate is valid in everyobservable state.1 Which states are observable will be discussed in section 2.2. Thefollowing listing shows an example of a static invariant:

1 /*@ public static invariant

2 @ (\ forall RadioPacket rp;

3 @ \ created(rp);

4 @ rp.buffer .length == rp. BUFFER_SIZE);

5 @*/

An instance invariant is specified equivalently to a static invariant but with the key-words “instance invariant” instead of “static invariant”. The difference froma static invariant is that this invariant quantifies implicitly over all created objects ofthe class it is defined in. Thus, if the static invariant from above would be located inthe class RadioPacket, then it could be translated to an instance invariant as follows:

1 /*@ public instance invariant buffer .length == BUFFER_SIZE; @*/

In this case study solely instance invariants have been used. A more detailed intro-duction to invariants can be found in [Lea06], [Lea08] or [Bec07, chapter 5] again.

2.1.3 Further specification entities

JML offers further specification entities, e. g. ghost fields, model fields and model meth-ods. In principle, these are important entities, too, which are used in the case study aswell. However, since this thesis does not refer directly to the parts of the specificationwhere these entities are used, the entities won’t be considered here. Readers interestedin further entities should refer to [Bec07, chapter 5] or [Lea08].

The next section will deal with the notion of “program correctness” as used in thecontext of this thesis.

2.2 Program correctness

This section introduces the notion of “program correctness” as used in the contextof this thesis. Additionally, it will be discussed which proof obligations have to beshown with KeY to achieve this kind of program correctness. The presentation follows[Bec07, chapter 8], which discusses the topic in much greater detail.

1 This is how invariants are interpreted by KeY. The official interpretation of JML is that thepredicate has to be valid in every visible state. For a discussion of the visible state semanticsplease refer to [Lea08] or [Bec07, chapter 8].

2.2 Program correctness 9

Definition 1. A Program P is called observed state correct w. r. t. a specificationSpec, if

1. all methods m of P fulfill all their method contracts mct ∈ Spec,

2. all invariants of Spec are preserved by all methods of P (in context of JMLthis implies that a method has to preserve an invariant even if the invariant isdeclared in another class than the method itself) and

3. all invariants are valid in the initial program state of P .

The intention of this definition is described by [Bec07, chapter 8.2] as follows:

“The mental model behind this notion of correctness is that of an ob-server of P . We think of an observer as a set of classes that may run allpublic methods of P . The observer sees all internal details of P , all valuesstored in all fields and arrays of all of P , but only in the pre-state andpost-state. He does not see intermediate states. He has access to all publicfields and can run a public method in a state satisfying its preconditionand observe whether the final state satisfies its postcondition. He can see,whether the pre-state satisfies an additional property I and he can checkwhether I is again true in the post-state. When all observers only observebehavior of P consistent with Spec, we call P observed-state correct. Onthe other hand, if there is an observer which observes behavior which differsfrom Spec, then P is incorrect.”

In order to achieve this kind of program correctness KeY provides several proofobligations:

• If mct ∈ Spec is a method contract for the method m ∈ P and I is a setof invariants, then the proof of the proof obligation EnsuresPost(mct; I) showsthat m ensures the post-condition of mct in the case that the pre-condition ofmct and the invariants Φ ∈ I hold on the invocation of m.

• If mct ∈ Spec is a method contract for the method m ∈ P and I is a set ofinvariants, then the proof of the proof obligation RespectsModifies(mct; I) showsthat m alters at most the locations listed in the assignable-clause of mct if thepre-condition of mct and the invariants Φ ∈ I hold on the invocation of m.

• If m ∈ P is a method and I as well as I ′ are sets of invariants, then the proof ofthe proof obligation PreservesInv(m; I; I ′) shows that m ensures the validity ofall invariants Φ′ ∈ I ′ if the invariants Φ ∈ I can be assumed.

• If Φ is an invariant, then the proof obligation InitInv(Φ) shows that Φ is validin the initial program state of P .

10 2 Foundations

Thus the first part of definition 1 is covered by the proof obligations EnsuresPost(·)and RespectsModifies(·), the second part by the obligation PreservesInv(·) and the lastpart by the proof obligation InitInv(·). KeY provides some additional proof obliga-tions which can replace some of the above but these won’t be considered here. For adiscussion of all proof obligations available please refer to [Bec07, chapter 8].

The next section deals with aspects of KeY which are important to know to be ableto follow the discussions in chapter 4.

2.3 KeY

As [Uni08] points out, “the KeY System is a formal software development tool thataims to integrate design, implementation, formal specification, and formal verificationof object-oriented software as seamlessly as possible. At the core of the system is anovel theorem prover for the first-order Dynamic Logic for Java with a user-friendlygraphical interface.”

This section will summarize the most important aspects of KeY as briefly as possible.This includes short introductions to JavaDL, sequences, updates, modifier sets, theusage of KeY and the usage of lemmata. Detailed discussions on all of these aspectscan be found in [Bec07].

2.3.1 JavaDL

The first-order Dynamic Logic for Java—or shortly “JavaDL”—is a logic for reasoningabout Java programs. In short—for readers who are familiar with modal logics—JavaDL is a multi modal logic with modal operators <π> and [π] for each programsequence π. The states of the modal logic are identified with structures of typed first-order predicate logic. The accessibility relation ρ is defined according to the programP considered: If S1 and S2 are (program) states and π is a program sequence, then(S1, π, S2) is an element of ρ (written (S1, π, S2) ∈ ρ) iff π started in S1 terminatesnormally in S2 according to the Java language specification.

For readers who are not familiar with modal logics, the following description mightgive an impression of JavaDL: When a program is executed, it passes several programstates. Thus, if one aims to verify a program, the logic which shall be used for thispurpose has to be able to refer to different program states and how to get from oneprogram state to another. For this purpose JavaDL provides modal operators <π> and[π] for each program sequence π. These operators can be placed before an arbitraryformula φ and the resulting construct (<π>φ or [π]φ) is a formula again. For example

x = 0→ <x++;>x = 1

is a JavaDL formula. It states that, if x = 0 is fulfilled before executing the programsequence x++;, then the program sequence will terminate and x = 1 will hold afterits execution. The statement that x++; will terminate is implied by the usage of theoperator < · >. If no termination is required, the operator [ · ] can be used instead.

2.3 KeY 11

2.3.2 Sequences

For the resolution of JavaDL formula, KeY uses a sequence calculus. A sequence isa comma separated list Γ of formulae followed by a sequence arrow “==>” followedby a comma separated list ∆ of formulae again. A sequence Γ ==>∆ is interpretedaccording to the formula

(∧

γ∈Γ

γ)→ (∨

δ∈∆

δ).

Thus, for example the formula

x = 0→ <x++;>x = 1

could be written as sequence as

x = 0 ==> <x++;>x = 1

or as

==> x = 0→ <x++;>x = 1

or as

==> ¬(x = 0), <x++;>x = 1.

This kind of sequences is displayed by KeY and can be modified with KeY throughoutthe verification of a program. Most parts of the resolution of sequences are performedautomatically by KeY, but the user can—and sometimes has to—apply rules manually,too. How rules can be applied will be discussed in section 2.3.5.

2.3.3 Updates

JavaDL formula (and thus sequences, too) may contain updates. Updates are generatedwhen program statements in modalities are executed symbolically and are placed—enclosed in braces—directly before the modality. They can be thought of as a simplelanguage for describing program transitions. Since KeY manages updates totally au-tomatically in general, in this thesis they are of interest only as far as they occurin sequences—with one exception: In section 4.5.2 the rule “update_cut” has to beapplied to an update. As the name of the rule indicates, in this case the user has toguide KeY a bit by stating in which way an update can be simplified.

2.3.4 Modifier sets

Because the theorem prover of KeY is based on a calculus for JavaDL formula, JMLspecifications have to be translated to JavaDL. This translation is fully automated,

12 2 Foundations

but nevertheless there is one aspect on this translation one should be aware of in orderto be able to understand the discussions in sections 4.2.2 and 4.5.2: KeY uses modifiersets to represent assignable-clauses of JML. Similar to assignable-clauses, modifier setscan be thought of as a list of locations which are allowed to be altered, e. g. in thecontext of a method invocation. But there is one difference between the interpretationof a modifier set and an assignable-clause which will become important in the sectionsmentioned: If a modifier set is empty (i. e. if it lists no locations), then really nolocation may change. Thus, the program won’t change its state. In contrast, theJML specification allows the creation of objects and even the modification of newlycreated objects in case of an empty assignable-clause. Hence, if the translation ofJML to JavaDL shall conform to the JML specification, an assignable-clause can’t betranslated to a modifier set one-to-one. Readers should be aware of this fact whenreading sections 4.2.2 and 4.5.2.

2.3.5 Using KeY

This section briefly introduces the user interface of KeY. The user interface is dividedinto three parts (cp. figure 2.1):

• A big pane on the right which shows the sequence representing the currentlyselected goal,

• a small pane on the top left which lists the proof obligations loaded and

• a tabbed pane on the bottom left with tabs for

– the proof history (the tab “Proof”),

– a list of currently open goals (the tab “Goals”),

– a pane for choosing the rule application strategies (the tab “Proof SearchStrategy”),

– a summary of all available rules (the tab “Rules”) and finally

– a pane for some user specific constraints (the tab “User Constraint”).

The minimum which has to be known about the usage of the user interface is

• how to load proof obligations,

• how to start and control the automatic rule application and

• how to apply rules manually.

The remainder of this section will discuss these aspects.

2.3 KeY 13

Figure 2.1: The user interface of KeY.

Loading proof obligations

A proof obligation can be loaded by selecting the menu item “Load” in the menu“File” and choosing the base folder of the Java program to be verified. After KeYhas parsed the program as well as its JML specification, a dialog will appear whichlists all available kinds (EnsuresPost, RespectsModifies, PreservesInv etc.) of proofobligations for all methods and all classes. The selection of a proof obligation typewill open a new dialog where the parameters of the proof obligation kind (if available)can be selected. For example, in context of the proof obligation type EnsuresPost theparameters mct (the method contract) and I (the set of assumed invariants) have tobe selected. After the last selections have been confirmed, the proof obligation will becreated as a JavaDL formula and will appear in the pane on the right. Additionally,the top left pane will show a short description of the proof obligation. If further proofobligations are loaded via the menu item “Proof Obligation Browser” in the menu“Tools”, the user is able to toggle between them by selection of the particular short

14 2 Foundations

description.

Starting the automatic rule application

The automatic rule application to suitably transform the formula under considerationcan be started by clicking on the ◮ -button—either in the toolbar or in the tab“Proof Search Strategy”. It can be controlled via the settings in the tab “Proof SearchStrategy”. For a discussion of the available strategies please refer to e. g. [Bec07,chapter 10] or [Ahr07].

Applying rules manually

In order to apply rules manually, KeY provides an easy to use, context sensitivehighlighting and selection mechanism. When the mouse is positioned over a functionor predicate symbol, the corresponding term or formula will be highlighted. Clickingon such a symbol will open a context menu which lists all rules which are (manually)applicable to the term or formula. The selection of a rule from the context menu willapply this rule.

Some rules require additional information. In such cases a dialog for entering theinformation will open after the rule has been selected from the context menu.

More detailed introductions to the user interface of KeY can be found in [Bec07,chapter 10] or [Ahr07].

2.3.6 Lemmata

In KeY most rules are formulated as taclets. Taclets are rules which are defined withthe help of a special language. Using this language, the user has the possibility toextend KeYs rule base by further rules. These rules—or taclets—normally should beproven to be correct with the help of the standard rule base and thus can be seen aslemmata. Listing 2.5 shows an example of such a taclet.

The remainder of this section will briefly describe the most important keywords ofthe taclet language. [Bec07, chapter 4] discusses taclets in more detail.

• \schemaVariables{·}: In the scope of this keyword schema variables are definedwhich can be used within rules. When a rule is applied, these schema variablesare instantiated by KeY with explicit terms or formula of the defined type.

• \functions{·}: In the scope of this keyword new function symbols can be de-fined. These can be used within rules.

• \predicates{·}: In the scope of this keyword new predicate symbols can bedefined. These can be used within rules.

• \rules{·}: In the scope of this keyword new rules can be defined.

• \assumes{·}: Can be used within the definition of a rule. The specified conditionmust hold when the rule is applied.

2.3 KeY 15

1 \ schemaVariables {

2 \term int x;

3 \term numbers n;

4 }

5

6 \ functions {

7 int andBitwise(int , int , int);

8 }

9

10 \ rules {

11 translateAndJlong_automatic {

12 \find(

13 andJlong(x, Z(n))

14 )

15 \ sameUpdateLevel

16 \ replacewith(

17 moduloLong( andBitwise( toTwoComplJlong(x),

toTwoComplJlong(Z(n)), 64))

18 )

19 \ heuristics( userTaclets3)

20 };

21 }

Listing 2.5: Example of a taclet.

• \find{·}: Can be used within the definition of a rule. The rule can be appliedto the specified term or formula.

• \replacewith{·}: Can be used within the definition of a rule. Replaces theterm or formula specified via the find-clause with the term or formula specifiedin the scope of this keyword.

• \add{·}: Can be used within the definition of a rule. Adds the specified formulaeither to the antecedent (before the sequence arrow) or the succedent (after thesequence arrow) of the sequence depending on the position of the sequence arrow==> in the scope of this keyword.

Additionally, semicolons in the definition of a rule—e. g. between two replace-clauses—specify a splitting of the proof in #semicolons + 1 new branches.

Further examples can be found in appendix A.

16 2 Foundations

CHAPTER 3

Survey of the network library

3.1 Design

Note: Because the author had no access to further design documentation than the—as far as design is concerned insufficient—in-code-documentation of the source code,this section is based on the standards IEEE 802.15.4 [IEE06] and RFC 4944 [RFC07],which the network library claims to implement in its in-code-documentation. Thus thissection reflects the design of the network library as the standards intend it to be, whichmight be different from the one actually chosen by Sun—even though a different designwould mean that the network library would not be totally standard-conforming.

The Sun SPOT’s network library (figure 3.6) is based on the four-layered TCP/ IPModel [RFC89]: the Application Layer, the Transport Layer and the Network Layerof the library comply directly to the corresponding layers of the TCP/ IP Model. TheNetwork Access Layer on the other hand has been replaced by two (sub-) layers: aMedia Access Control (MAC) Sublayer and a Physical Layer. The MAC Sublayerand the Physical Layer comply to the IEEE 802.15.4 standard for Low-Rate WirelessPersonal Area Networks (LoWPAN) [IEE06]. The IEEE 802.15.4 standard is based onthe seven-layered Open Systems Interconnection Reference Model (OSI Model) [ISO96]and specifies a Data Link Layer and a Physical Layer for LoWPANs. In this context theData Link Layer has been split into three sublayers: the Logical Link Control (LLC),the Service-Specific Convergence Sublayer (SSCS) and the MAC Sublayer. Though thelayers of the TCP/ IP Model can be assigned roughly to the layers of the OSI Model(like shown in figure 3.6), the TCP/ IP Model is not OSI Model compliant. Thus, anadaption layer, namely the LoWPAN Adaption Layer, has been placed between theNetwork Layer and the MAC Sublayer in the Sun SPOT’s network library. Since theverified part of the network library is located in the LoWPAN Adaption Layer andthe MAC Sublayer, the remainder of this chapter focuses mainly on these two layers.

The MAC Sublayer as well as the Physical Layer provide a management service—notfurther considered here—and a data service. The data service of the MAC Sublayer(the MAC data service) enables the transmission and reception of MAC protocol dataunits (MPD units) across the data service of the Physical Layer (the PHY data service)

18 3 Survey of the network library

Figure 3.1: Frame structures and their relations: PHY protocol data (PPD) unit,MAC protocol data (MPD) unit and LoWPAN encapsulation frame.

[IEE06]. These MPD units are sequences of octets which are structured like shownin figure 3.1: they consist of a header with a frame control, a sequence number, someaddressing fields and an optional security header, followed by the payload and a footerwith a frame check sequence. The structure of the MPD units will be of interest duringthe verification process. The complete specification of the MAC data service can befound in [IEE06, chapter 7].

Because—like mentioned above—the IEEE 802.15.4 standard is based on the OSIModel and the TCP/ IP Model is not OSI Model compliant, there is the need foran adaption layer to overcome the differences in the architectures. This is the roleof the LoWPAN Adaption Layer. It complies to the proposed standard1 RFC 4944[RFC07] and offers a data service on top of the MAC data service which provides en-capsulation of higher level (e. g. IPv6) packets, header compression (for IPv6 packets),fragmentation and—in cooperation with a routing manager—mesh routing.

The LoWPAN Adaption Layer creates an encapsulation frame with headers for thedifferent functionalities and passes it to the MAC data service. Like the MPD unitthe LoWPAN encapsulation frame is a sequence of octets with a particular structure.This structure is defined by the RFC 4944 standard as shown in figure 3.1: it consistsof an optional mesh header, an optional broadcast header, an optional fragmentationheader, a protocol header and finally the payload. The order of the headers is fixedto the order they are listed.

The presence or absence of an optional header can be detected via some uniquebit pattern at the beginning of each header. Figures 3.2 to 3.5 show the structuresof the headers in more detail. The complete specifications can be found in [RFC07,sections 5.1, 5.2, 5.3, 10 and 11.1].

1 In the following, the word “proposed” will be skipped in favor of better readability.

3.1 Design 19

Figure 3.2: Mesh header structure. The optional additional hops left byte (opt. add.HopsLft) is created only if the number of left hops is greater than 14. Its existence isindicated by the HopsLft value of 0xF.

Figure 3.3: Broadcast header structure.

Figure 3.4: Fragmentation header structure. Top: first fragment. Bottom: second andfollowing fragments.

Figure 3.5: Protocol header structure.

So far, readers should have a brief overview of the design of the parts of the networklibrary important for the verification. The next section provides an overview of theimplementation of these parts.


Figure 3.6: Sun SPOT’s network library architecture and related architectures.

3.2 Implementation 21

3.2 Implementation

The MAC Sublayer consists of an interface and five classes, the interface I802_15_4-

_MAC and the classes MACLayer, MACBase, RadioPacket, MACException and MAC_In-

validParameterException. The MAC management service and the MAC data ser-vice are provided by the classes MACLayer and MACBase. MPD units are imple-mented as byte arrays and each MPD unit is encapsulated into an object of theclass RadioPacket. The class RadioPacket is responsible for the correctness of thestructure of the contained MPD unit and provides methods for correctly reading in-formation from and writing information to it. The remainder two classes, the classesMACException and MAC_InvalidParameterException, are used to signal errors: theclass MACException signals an unexpected error in a received RadioPacket while theclass MAC_InvalidParameterException signals that an invalid parameter has beenpassed to the MAC Sublayer.

The LoWPAN Adaption Layer consists of an interface and four classes, the interfaceILowPan and the classes LowPan, LowPanHeader, LowPanHeaderInfo and LowPanPac-

ket. The class LowPan provides the data service of the LoWPAN Adaption Layer. Incontrast to MPD units, LoWPAN encapsulation frames are not implemented as enti-ties of their own but they are embedded directly into the payload area of a MPD unit.1

Each embedded LoWPAN encapsulation frame is itself encapsulated into an object ofthe class LowPanPacket. An object of the class LowPanPacket accesses the LoWPANencapsulation frame via a reference to an object of the class RadioPacket which againcontains the MPD unit the LoWPAN encapsulation frame is embedded in. The classLowPanPacket is responsible for the correctness of the structure of the LoWPAN en-capsulation frame and provides methods for correctly reading information from andwriting information to it. The remainder two classes, the classes LowPanHeader andLowPanHeaderInfo, are both used to store header information of the LoWPAN encap-sulation frame. Objects of the class LowPanHeader are intended to collect all headerinformation necessary for creating and sending a LoWPAN encapsulation frame. Thus,all information can be written at a single blow to the LoWPAN encapsulation frame.This has the advantage that it is clear which of the optional headers actually arepresent and thus which header has to be written to which position of the payloadarea of the encapsulating MPD unit. The class LowPanHeaderInfo on the other handstores all header information of a LoWPAN encapsulation frame after reception anddecapsulation. This includes information like timestamps etc. which are not neededin the former case.

The remainder of this section focuses on the classes effectively involved in the veri-fication process and gives a deeper insight into the implementation of the data serviceof the LoWPAN Adaption Layer.

The classes involved into the verification process are the classes LowPan, LowPan-

1 Thus, the LoWPAN Adaption Layer has to create MPD units. This is not totally conforming tothe IEEE 802.15.4 standard since the IEEE 802.15.4 standard requires the MPD unit creation tobe part of the MAC Sublayer [IEE06, section 7.1.1.1].


com.sun.spot.peripheral.radio com.sun.spot.util

UtilsRadioPacketLowPan LowPanPacket

LowPanHeader

creates and sends uses

Figure 3.7: Class diagram of the classes involved into the verification process.

class LowPan LowPanHeader LowPanPacket RadioPacket Utils

#methods 31 29 56 61 34#attributes 18 32 31 33 3

Table 3.1: Number of methods and attributes of the classes involved into the verifica-tion process.

Header, LowPanPacket, RadioPacket and the utility class Utils. Amongst others, theclass Utils provides methods for writing numbers (shorts, integers and longs) to andreading them from byte arrays. These methods are used by the class RadioPacket.Figure 3.7 shows a class diagram of all classes involved into the verification processwhile table 3.1 gives an overview of their number of methods and attributes. Fig-ures 3.8 to 3.10 list all methods and attributes of the involved classes.

The central class in the class diagram is the class LowPan. Like mentioned above,this class provides the data service of the LoWPAN Adaption Layer. To send data overthe data service, the service requires the data in form of a byte array. Additionally itneeds a destination address in form of a 64 bit IEEE 802.15.2 address or a 16 bit RFC4944 short address, a protocol family number and a protocol number. The normalsend and reception mechanism is initiated by the invocation of the method

1 public long send(

2 byte protocolFamily ,

3 byte protocolNum ,

4 long toAddress ,

5 byte[] buffer ,

6 int startOffset ,

7 int endOffset

8 );


or the method

1 public boolean send(

2 byte protocolFamily ,

3 byte protocolNum ,

4 long toAddress ,

5 byte [] buffer ,

6 int startOffset ,

7 int endOffset ,

8 boolean failIfNotSingleHop

9 );

and includes the following steps:

1. If mesh routing is enabled, the next destination on the route to the final desti-nation will be determined. For this purpose the method makes use of a routingmanager which won’t be considered any further.

2. If the data does not fit into a single LoWPAN encapsulation frame, the datawill be fragmented. In this case, the method sendInFragments will be invokedwhich creates a commensurate number of MPD units with embedded LoWPANencapsulation frames. If the data does fit into a single LoWPAN encapsulationframe, the method sendInOnePacket will be invoked instead. The main differ-ence to the method sendInFragments is that no fragmentation header has to bewritten and that the method implementation is simpler for obvious reasons.

3. The created MPD units will be passed to the MAC Sublayer which is responsiblefor completing the send procedure.

4. The MAC Sublayer of the next destination (hopefully) receives the sent MPDunits and notifies the LoWPAN Adaption Layer by calling the method receive(

RadioPacket packet) for each received MPD unit.

5. The method receive(RadioPacket packet) extracts the LoWPAN encapsu-lation frame header from the LoWPAN encapsulation frame embedded in thepassed MPD unit. If the final destination of the LoWPAN encapsulation framehas been reached, the data will be reassembled via the method reassembly(Low-

PanPacket lpp) and passed to the specified superior protocol (via the protocolfamily and number). Otherwise the LoWPAN encapsulation frame will be for-warded via the method forwardMeshPacket(LowPanPacket lpp) to the nextdestination on the route to the final destination.

There are some variations of this mechanism—for example for broadcasting—whichinvolve other methods than the ones mentioned above. Broadcasting for example isprovided by the method sendBroadcast(byte protocolNum, byte[] buffer, int

startOffset, int endOffset, int hops).


LowPan

- routeLock : Object

- MAX_BROADCAST_DELTA : int

- ourAddress : long

- dataListener : Vector

- routeListener : Vector

- datagramTag : int

- broadcastSeqNo : int

- protocolTable : IntHashtable

- protocolFamilyTable : IntHashtable

- availRoutes : Hashtable

- lowPan : ILowPan

- routingManager : com::sun::spot::peripheral::radio::mhrp::interfaces::IRoutingManager

- packetDispatcher : IRadioPacketDispatcher

- reassemblyBuffers : Hashtable

- bCastSeqNos : Hashtable

- reassemblyTimer : Timer

- REASSEMBLEY_EXPIRATION_TIME : long

+ fragments : RadioPacket[]

+ getInstance() : ILowPan

# LowPan(ourAddress : long, aodvManager : com::sun::spot::peripheral::radio::mhrp::interfaces::IRoutingManager, radioPacketDispatcher : IRadioPacketDispatcher)

+ setRoutingManager(newRoutingManager : com::sun::spot::peripheral::radio::mhrp::interfaces::IRoutingManager) : com::sun::spot::peripheral::radio::mhrp::interfaces::IRoutingManager

+ registerProtocolFamily(protocolFamily : byte, protocolMan : IProtocolManager)

+ registerProtocol(protocolNum : byte, protocolMan : IProtocolManager)

+ deregisterProtocol(protocolNum : byte)

+ deregisterProtocolFamily(protocolFamily : byte)

+ registerDataEventListener(dataListener : IDataEventListener)

+ registerRouteEventListener(routeListener : IRouteEventListener)

+ registerMHEventListener(mhListener : com::sun::spot::peripheral::radio::mhrp::interfaces::IMHEventListener)

+ deregisterDataEventListener(listener : IDataEventListener)

+ deregisterRouteEventListener(listener : IRouteEventListener)

+ routeFound(info : com::sun::spot::peripheral::radio::mhrp::RouteInfo, uniqueKey : Object)

+ receive(packet : RadioPacket)

# validateSeqNo(lpp : LowPanPacket) : boolean

+ getRoutingManager() : com::sun::spot::peripheral::radio::mhrp::interfaces::IRoutingManager

+ eqPos(i : int, j : int) : int

+ send(protocolFamily : byte, protocolNum : byte, toAddress : long, buffer : byte[], startOffset : int, endOffset : int) : long

+ send(protocolFamily : byte, protocolNum : byte, toAddress : long, buffer : byte[], startOffset : int, endOffset : int, failIfNotSingleHop : boolean) : boolean

- sendPrim(protocolFamily : byte, protocolNum : byte, toAddress : long, buffer : byte[], startOffset : int, endOffset : int, failIfNotSingleHop : boolean, lpp : LowPanPacket) : boolean

+ sendWithoutMeshingOrFragmentation(protocolNum : byte, toAddress : long, buffer : byte[], startOffset : int, endOffset : int)

+ sendBroadcast(protocolNum : byte, buffer : byte[], startOffset : int, endOffset : int, hops : int) : long

- setSequenceNumber(lph : LowPanHeader)

- sendInOnePacket(routeInfoOrNull : com::sun::spot::peripheral::radio::mhrp::RouteInfo, protocolNum : byte, buffer : byte[], startOffset : int, endOffset : int, lpp : LowPanPacket, lph : LowPanHeader)

- sendInFragments(routeInfoOrNull : com::sun::spot::peripheral::radio::mhrp::RouteInfo, protocolNum : byte, buffer : byte[], startOffset : int, endOffset : int, lpp : LowPanPacket, lph : LowPanHeader, freeSpace : byte)

- findNextHop(destinationAddress : long) : com::sun::spot::peripheral::radio::mhrp::RouteInfo

- readPacket(lpp : LowPanPacket, startPos : int, length : int)

- forwardMeshPacket(lpp : LowPanPacket)

- getProtocolFamilyFor(protocolFam : byte) : IProtocolManager

- getProtocolFor(protocolNum : byte) : IProtocolManager

- reassembly(lpp : LowPanPacket)

+ setOurAddress(addr : long)

Figure 3.8: The class LowPan.

The verification of the implementation of the send mechanism including fragmenta-tion and packaging but excluding mesh routing is the topic of the next chapter.


RadioPacket

- MAX_DATA_LENGTH : int

- BUFFER_SIZE : int

- MAX_HEADER_LENGTH : int

+ MIN_PAYLOAD_LENGTH : int

- LENGTH_OFFSET : int

- FCF_OFFSET : int

- DSN_OFFSET : int

- LINK_QUALITY_STEPS : int

- CORRELATION_LOW : int

- CORRELATION_HIGH : int

- FRAME_TYPE : int

- FRAME_TYPE_DATA : int

- FRAME_TYPE_ACK : int

~ ACK_REQUEST : int

- INTRA_PAN : int

- DST_ADDR_BITS : int

- DST_ADDR_NONE : int

- DST_ADDR_16 : int

- DST_ADDR_64 : int

- SRC_ADDR_BITS : int

- SRC_ADDR_NONE : int

- SRC_ADDR_16 : int

- SRC_ADDR_64 : int

- destinationPanOffset : int

- destinationAddressOffset : int

- sourceAddressOffset : int

- payloadOffset : int

- dsnOK : boolean

~ buffer : byte[]

~ rssi : int

~ corr : int

~ timestamp : long

- offsetsInitialised : boolean

+ getDataPacket() : RadioPacket

+ getAckPacket() : RadioPacket

+ getBroadcastPacket() : RadioPacket

- RadioPacket()

- initAsData()

- setOffsets()

- initAsBroadcast()

- initAsAck()

+ getDestinationAddress() : long

+ setDestinationAddress(addr : long)

+ getSourceAddress() : long

+ setSourceAddress(addr : long)

+ getSourcePanID() : int

+ getDestinationPanID() : int

+ setDestinationPanID(id : int)

+ getDataSequenceNumber() : byte

+ getFrameControl() : int

~ setFrameControl(fc : int)

+ getMACPayloadAt(offset : int) : byte

+ setMACPayloadAt(offset : int, value : byte)

+ setMACPayloadLength(macPayloadLength : int)

+ getLinkQuality() : int

+ getCorr() : int

+ getRssi() : int

+ isSeqOK() : boolean

+ setSeqOK(dsnOK : boolean)

+ getMACPayloadLength() : int

~ getLength() : int

~ setLength(l : int)

+ decodeFrameControl()

+ copyFrom(otherRP : RadioPacket)

+ writeOnto(dataOutputStream : DataOutputStream)

+ readFrom(dataInputStream : DataInputStream) : RadioPacket

+ readWithoutTimestampFrom(dataInputStream : DataInputStream) : RadioPacket

+ writeOnto(outputBuffer : byte[], startingOffset : int) : int

+ writeWithoutTimestampOnto(outputBuffer : byte[], startingOffset : int) : int

+ readFrom(inputBuffer : byte[], startingOffset : int) : RadioPacket

+ isAck() : boolean

+ isData() : boolean

+ ackRequest() : boolean

~ setDSN(macDSN : byte)

+ getMACPayloadIntAt(macPayloadOffset : int) : int

- getLongAt(offset : int) : long

- getIntAt(offset : int) : int

+ getMACPayloadLongAt(macPayloadOffset : int) : long

- setLongAt(offset : int, value : long)

+ setMACPayloadIntAt(macPayloadOffset : int, value : int)

+ setMACPayloadLongAt(macPayloadOffset : int, value : long)

- getShortAt(offset : int) : int

+ getMACPayloadShortAt(macPayloadOffset : int) : int

+ setMACPayloadShortAt(macPayloadOffset : int, value : int)

- setShortAt(offset : int, value : int)

- setFCS(s : short)

+ getFCS() : short

+ calculateAndSetFCS()

+ isFCSValid() : boolean

+ getMaxMacPayloadSize() : int

~ getPayloadOffset() : int

~ dump()

+ toString() : String

+ getTimestamp() : long

LowPanPacket

# DISPATCH_MASK : byte

- F_BIT : byte

- O_BIT : byte

- HOPSLEFT_BITS : byte

- FRAG_FIRST : byte

- FRAG_INTERIOR : byte

- FRAG_LAST : byte

# DATA_PACKET : int

# BROADCAST_PACKET : int

- rp : RadioPacket

- meshed : boolean

- meshIndex : int

- extendedHops : boolean

- hopsLeftIndex : int

- origAddrIndex : int

- destAddrIndex : int

- destLen : int

- origLen : int

- bCast : boolean

- bCastIndex : int

- fragged : boolean

- fragIndex : int

- fragTagIndex : int

- fragSizeIndex : int

- fragOffsetIndex : int

- extendedProtocol : boolean

- protocolDispatchIndex : int

- protocolIndex : int

- lppPayloadOffset : int

- lppPayloadSize : int

- parseIndex : int

+ LowPanPacket(type : int)

+ LowPanPacket(packet : RadioPacket)

- parse_fragment(dispatch : byte)

~ parse_mesh(dispatch : byte)

- parse_broadcast(dispatch : byte)

- parse_esc(dispatch : byte)

- parse_family(dispatch : byte)

# parse()

- writeMeshHeader(lph : LowPanHeader)

- writeBroadcastHeader(lph : LowPanHeader)

- writeFragmentHeader(lph : LowPanHeader)

- writeProtocolHeader(lph : LowPanHeader)

+ writeHeaderAndPayload(lph : LowPanHeader, buffer : byte[], start : int, end : int)

+ getHopsLeft() : byte

+ setHopsLeft(hopsLeft : int)

+ getDestLen() : int

+ setDestLen(destLen : int)

+ getOrigLen() : int

+ setOrigLen(origLen : int)

+ getOriginatorAddress() : long

+ setOriginatorAddress(origAddr : long)

+ getFDestinationAddress() : long

+ setFDestinationAddress(destAddr : long)

+ getBCastSeqNo() : int

+ setBCastSeqNo(bCastSeqNo : int)

+ setFragType(type : byte)

+ getFragType() : byte

+ setFragTag(tag : short)

+ getFragTag() : short

+ setFragSize(size : short)

+ getFragSize() : short

+ getFragOff() : byte

+ setFragOff(fragOff : byte)

+ isFirstFrag() : boolean

+ getProtocolFamily() : byte

+ setProtocolFamily(protocolFamily : byte)

+ getProtocol() : byte

+ setProtocol(protocol : byte)

+ setProtocol(family : byte, protocol : byte)

+ isMeshed() : boolean

+ setMeshed(meshed : boolean)

+ isBCast() : boolean

+ setBCast(bCast : boolean)

+ isFragged() : boolean

+ setFragged(fragged : boolean)

+ getRPSourceAddress() : long

+ getRadioPacket() : RadioPacket

+ setRPDestinationAddress(addr : long)

+ setRPSourceAddress(addr : long)

+ getPayloadSize() : int

+ setPayloadSize(payloadSize : int)

+ getHeaderLength() : int

+ isExtendedProtocol() : boolean

+ setExtendedProtocol(extendedProtocol : boolean)

+ getLppPayloadOffset() : int

+ toString() : String

Figure 3.9: The classes RadioPacket and LowPanPacket.


LowPanHeader

- meshed : boolean

- fragged : boolean

- bCast : boolean

- hops : int

- bCastSeqNo : int

- fragType : int

- fragTag : int

- fragSize : int

- fragOffset : int

- protocolFamily : int

- protocolNo : int

- origLen : int

- destLen : int

- outgoingOriginatorAddress : long

- outgoingDestinationAddress : long

# UNFRAGMENTED : byte

# LAST_FRAGMENT : byte

# FIRST_FRAGMENT : byte

# INTERIOR_FRAGMENT : byte

+ DISPATCH_LOWPAN_IPV6 : byte

+ DISPATCH_LOWPAN_HC1 : byte

+ DISPATCH_LOWPAN_BC0 : byte

+ DISPATCH_ESC : byte

+ DISPATCH_SPOT : byte

+ FAMILY_DEFINED_PROTO : byte

# DISPATCH_FRAG : byte

# DISPATCH_MESH : byte

# MAX_PROTOCOL_HEADER_LENGTH : byte

# BROADCAST_HEADER_LENGTH : byte

# MAX_FRAGMENTATION_HEADER_LENGTH : byte

# MAX_MESH_HEADER_LENGTH : byte

+ MAX_UNFRAG_HEADER_LENGTH : byte

+ LowPanHeader()

+ getLength() : int

+ isFirstFrag() : boolean

+ isExtendedProtocol() : boolean

+ getOutgoingHops() : int

+ setOutgoingHops(outgoingHops : int)

+ getOutgoingBCastSeqNo() : int

+ setOutgoingBCastSeqNo(outgoingBCastSeqNo : int)

+ getOutgoingFragType() : int

+ setOutgoingFragType(outgoingFragType : int)

+ getOutgoingFragTag() : int

+ setOutgoingFragTag(outgoingFragTag : int)

+ getOutgoingFragSize() : int

+ setOutgoingFragSize(outgoingFragSize : int)

+ getOutgoingFragOffset() : byte

+ setOutgoingFragOffset(outgoingFragOffset : int)

+ getOutgoingOriginatorAddress() : long

+ setOutgoingOriginatorAddress(outgoingOriginatorAddress : long)

+ getOutgoingDestinationAddress() : long

+ setOutgoingDestinationAddress(outgoingDestinationAddress : long)

+ getProtocolNo() : byte

+ isMeshed() : boolean

+ setMeshed(meshed : boolean)

+ isFragged() : boolean

+ setFragged(fragged : boolean)

+ isBCast() : boolean

+ setBCast(bCast : boolean)

+ getProtocolFamily() : byte

+ setProtocolInfo(protocolFamily : byte, protocolNo : byte)

Utils

+ SIZE_OF_SHORT : int

+ SIZE_OF_INT : int

+ SIZE_OF_LONG : int

+ log(message : String)

+ copy(aByteArray : byte[]) : byte[]

+ readNumber(number : String) : int

+ readLong(number : String) : long

+ addressPadding(address : int, padBoundary : int) : int

+ readLittleEndLong(byteArray : byte[], offset : int) : long

+ readLittleEndInt(byteArray : byte[], offset : int) : int

+ readBigEndInt(byteArray : byte[], offset : int) : int

+ readLittleEndShort(byteArray : byte[], offset : int) : int

+ readBigEndShort(byteArray : byte[], offset : int) : int

+ readBigEndLong(byteArray : byte[], offset : int) : long

+ writeBigEndLong(byteArray : byte[], offset : int, value : long)

+ writeLittleEndLong(byteArray : byte[], offset : int, value : long)

+ writeBigEndInt(byteArray : byte[], offset : int, value : int)

+ writeLittleEndInt(byteArray : byte[], offset : int, value : int)

+ writeLittleEndShort(byteArray : byte[], offset : int, value : int)

+ writeBigEndShort(byteArray : byte[], offset : int, value : int)

- readLittleEndNumber(byteArray : byte[], offset : int, numberOfBytes : int) : long

- readBigEndNumber(byteArray : byte[], offset : int, numberOfBytes : int) : long

- writeBigEndNumber(byteArray : byte[], offset : int, numberOfBytes : int, value : long)

- writeLittleEndNumber(byteArray : byte[], offset : int, numberOfBytes : int, value : long)

+ writeNullTerminatedString(byteArray : byte[], offset : int, string : String)

+ readNullTerminatedString(byteArray : byte[], offset : int) : String

+ readDoublyNullTerminatedString(byteArray : byte[], offset : int) : String

+ as6BitNumber(number : int) : int

+ sleep(milliseconds : long)

+ getManifestProperty(manifestPropertyName : String, valueIfNotInManifest : String) : String

+ getManifestProperty(manifestPropertyName : String, valueIfNotInManifest : int) : int

+ getSystemProperty(propertyName : String, valueIfNotDefined : int) : int

+ enumToVector(drivers : Enumeration) : Vector

+ stringify(b : byte[]) : String

+ withSpacesReplacedByZeros(string : String) : String

+ isOptionSelected(optionName : String, defaultIfAbsent : boolean) : boolean

+ split(s : String, marker : char) : String[]

Figure 3.10: The classes LowPanHeader and Utils.

CHAPTER 4

Case study

This chapter is structured as follows: At first some general aspects of this case studywill be considered. This includes an overview of the extent of the case study and somenotes on the KeY version used. Afterwards, the decisions concerning the strategymade in this case study will be discussed. This includes a discussion on the methodverification order as well as a discussion on the system of proof obligations used. Thelatter leads to a discussion on what has to be paid attention to in order to achieveobserved state correctness and which problems arise in this context (section 4.3).Section 4.4 deals with problems concerning bit operations and provides a detailedverification example. It is followed by a section on various other problems whichrevealed during the verification process. Finally section 4.6 points out some of KeYsstrengths.

4.1 General aspects

Though the intention of this case study is more to examine which problems actuallyoccur when applying software verification to commercial software rather than verifyinga very particular piece of software, there are particular reasons why the Sun SPOTsnetwork library in general and the examined part in particular has been chosen:

1. A network library is probably not the most standard topic when dealing withdeductive software verification based on symbolic execution and thus it is inter-esting to investigate whether special problems arise when verifying such kind ofsoftware.1 (This chapter will show that this actually came true.)

2. The Sun SPOTs network library is based on the Java specification CLDC (Con-nected Limited Device Configuration) 1.1 which had not been investigated with

1 At a first glance, verifying a network library might seem to be more the domain of model checkersthan of a deductive verification system based on symbolic execution like KeY. But verifying anetwork library doesn’t mean to verify a network protocol but to verify that the implementationof a network protocol fulfills its specification.

28 4 Case study

KeY yet.

3. A bug in the Sun SPOTs network library had been reported probably residingin the part chosen for verification. It was of interest whether this bug couldbe detected by the verification. But as far as this thesis proceeded with theverification, the bug seems not to reside in the chosen part.

As already mentioned in the last chapter, the part of the network library chosento be examined is the send mechanism including fragmentation and packaging butexcluding mesh routing of the LoWPAN Adaption Layer as described in section 3.2.

4.1.1 Extent of the case study

The send mechanism involves about 100 methods whereof about 80 have been verified.Because of a lack of time it was not possible to verify all involved methods. Thelack of time arose mainly from three major problems which were revealed duringthe verification process. The discussion of these problems will claim great parts of thesections 4.3 to 4.5. Table 4.1 shows the distribution of the method sizes of the involvedclasses. Over all, most methods were quite small which is a positive observation incontext of software verification.

Altogether the specification contains 1 486 lines of JML comments. These havebeen proven in 351 proofs with a total number of 1 383 919 deductive steps. The mostextensive proof consists of 183 211 steps while the average number of steps is 3 942.8.The median number of steps is 124. The number of interactions can only be estimatedbut the average number of interactions should be around 7 while the median is about2 and the maximal number of interactions in a single proof is approximately 140. Butthese numbers do not take into account all user interactions (e. g. the switching ofrule application strategies) nor do they take the complexity of the interactions intoconsideration.

4.1.2 KeY version and settings

Because the Sun SPOTs network library is based on the Java-Virtual-Machine Squawkwhich implements the Java specification CLDC, KeY had to be adapted to work withSquawk. This was done mainly (but not exclusively) by replacing KeYs normal Javalanguage base by stubs of the Squawk classes and by recompiling KeY.1 Though thisprocess required the help of the KeY staff, the possibility to do so in a few days showsthe flexibility of the KeY system. The KeY version finally used for the verificationwas a side branch (the side branch “schebenSwquak”) of the version 1.3.204-beta.

1 A stub of a class contains mainly its method signatures without any implementation. They canbe generated automatically from class files.

4.2 Verification strategy 29

Size very small(1 - 2 loc)

small(3 - 8 loc)

medium(9 - 25 loc)

big(> 25 loc)

Utils 75% 25% 0% 0%RadioPacket 50% 44% 4% 2%LowPanHeader 94% 3% 3% 0%LowPanPacket 10% 50% 30% 10%LowPan 20% 20% 20% 40%

Table 4.1: Distribution of the method sizes. The method sizes are measured in lines ofcode (loc).

The preferences of KeY were left to their defaults1 except the setting of the integersemantics: This one was set to the Java integer semantics (intRules:javaSemantics).This is related to the fact that the specifications contain bit operations and that theJava integer semantics is the only integer semantics which is able to handle bit oper-ations within specifications.

The topic of the next section will be the discussion of the verification strategy usedin this case study.

4.2 Verification strategy

When verifying a piece of software, one has to make two strategy decisions:

1. In which principle order shall the methods be verified?

2. Which proof obligations shall be verified to obtain observed state correctness?

The decisions made in this case study will be discussed in the two following sections.

4.2.1 Method verification order

The first attempt to verify the send mechanism was from “top to bottom” starting withthe methods send(·) followed by the methods they invoke and so on. But the attemptto verify the first methods revealed that it is nearly impossible to “guess” correct andsignificant formal specifications in absence of an extensive informal specification. Thisleads to the following effect: imagine a method a which invokes a method b. Becauseof the strategy “top to bottom” a will be verified before b but with the help of the

1 The defaults are (from top to bottom): assertions:On, initialisation:disableStatic-

Initialisation, intRules:arithmeticSemanticsCheckingOF, javacard:jcOFF, nullPointer-

Policy:nullCheck, programRules:java, throughout:toutOn, transactionAbort:abortOn,transactions:transactionsOn, Delete effectless update 2�, One Pass Simplification 2�, PrestateRemember Updates 2�, Poststate Remember Accumulator 2�, Minimize Interaction 2� , DnDDirection Sensitive 2�, Sound 2�, Proof Assistant 2�

30 4 Case study

specification of b. Thus, if the subsequent verification of b reveals that the specificationof b was not totally correct, the least what has to be done is to adjust the specificationof b and to redo the proof of a. But in many cases it will be necessary to adjust thespecification of a, too. This again has influence on all methods invoking a and so on.Thus, this strategy is impracticable in the present case.

Therefore, the verification strategy actually chosen is the contrary one, the strategy“bottom up”: at first all methods which either invoke no other method or which invokeonly methods which can be trivially specified (like methods whose functionality is outof the scope of the restricted functionality of the send mechanism) were specified andverified. Afterwards, step by step, those methods were dealt with which invoke solelyalready verified methods. The disadvantage of this strategy is that there is a lot ofwork to do before getting only close to the method one initially was interested in.Nevertheless, in this case it seems to be the only practical strategy.

4.2.2 Proof obligation system

When verifying a piece of software, one has to come to another strategy decision aswell: the decision which proof obligations should be verified to obtain observed statecorrectness. The obligations chosen in this case study are the following ones:

• For all methods m and all method contracts mct for m the proof obligations

EnsuresPost(mct; I) and RespectsModifies(mct; I)

have been proven for some set of invariants I.

• For all methods m which have at least one contract which specifies a non emptymodifier set and for all invariants Φ the proof obligation

PreservesInv(m; I; {Φ})

has been proven for some set of invariants I.

Since solely instance invariants have been used within the specification and theproof obligation InitInv(Φ) is trivially true for instance invariants Φ (cf. [Bec07, sec-tion 8.3.1]), the proof obligation InitInv(Φ) hasn’t been proven explicitly. For a similarreason there is no need to verify the proof obligation PreservesInv(m; I; {Φ}) for meth-ods m whose contracts solely specify empty modifier sets. This is due to the fact that,if m fulfills the proof obligation RespectsModifies(mct; I) for all of its method con-tracts mct, then all invariants are trivially preserved by m since m can’t change theprogram state if m is used according to its specifications (cf. [Bec07, lemma 8.14]).At the moment KeY interprets the JML assignable-clause “assignable \nothing;”as empty modifier set though this does not strictly accord with the JML specification(cp. section 2.3). Since the specification of a method as pure adds an implicit contract

4.3 Achieving observed state correctness and problems related to it 31

1 /*@ private behavior

2 @ requires true;

3 @ diverges false;


5 @*/

to the method (cf. [Lea08, section 7.1.1.3]), one advantage of KeYs current interpreta-tion (beside others, which are out of the scope of this thesis) is that the proof obligationPreservesInv(m; I; {Φ}) needs not to be proven for methods which are pure with re-spect to KeYs interpretation. On the other hand, this interpretation leads to someproblems—especially in connection with the specification of methods as pure—whichwill be discussed in section 4.5.2.

It might be surprising that the decision for the invariant proving strategy fell onproving PreservesInv(m; I; {Φ}) for all methods m (except the ones discussed above)and all invariants Φ since at a first glance this seems to result in about #methods ·#invariants proofs and thus in an explosion of the number of proofs. But the numberof proofs does not explode because the following condition holds for an arbitrarymethod m and arbitrary sets of invariants I and I ′:

For all Φ ∈ I ′ : PreservesInv(m; I; I ′) � PreservesInv(m; I; {Φ})

Thus, if one would use the set of all invariants as I ′, then only #methods proofs wouldbe necessary. Of course, the proof for PreservesInv(m; I; I ′) will split into at least |I ′|branches: one for each Φ ∈ I ′. But since the proofs for these branches are trivial inthis case study in most cases, the whole proof normally can be closed automaticallyby KeY. Thus, the user saves a lot of time by combining several proof obligations toone obligation since considerably less proof obligations have to be loaded and managedby the user. To enable the possibility to verify the program “class wise” and thus toachieve some locality within the verification process, not all invariants of the wholeprogram but all invariants of a class have been proven to hold for a method in oneproof. This approach results in about #classes · #methods proofs whereof most aresimple. This is acceptable in the scope of this thesis. On the other hand this way oneavoids the need of guards which often entail additional non trivial proof obligations(cf. [Bec07, chapter 8]).

In the next section it will be considered which additional things have to be paidattention to to achieve observed state correctness and which problems arise in thiscontext.

4.3 Achieving observed state correctness and problems related to it

This section discusses some problems which occur in connection with the applicationof method contracts. All these problems have one thing in common: they either inhibitthe possibility to achieve observed state correctness or they may lead to a violation ofthe observed state correctness.

32 4 Case study

But before these problems are discussed, some notions shall be introduced.

4.3.1 Definitions

Let mct be a method contract for a method m and let Φ be an invariant. The set ofinvariants I which is selected as assumption for a proof obligation (e. g. the proof obli-gation EnsuresPost(mct; I)) will be referred to as proof assumption. The union J =I1∪I2∪

⋃

Φ IΦ of the proof assumptions for the proof obligations EnsuresPost(mct; I1),RespectsModifies(mct; I2) and PreservesInv(m; IΦ; {Φ}) will be referred to as contractassumption. The set of invariants which is selected in the context of a contract appli-cation as assumed (e. g. via the “Contract Configurator” which appears when applyingthe rule “Use Operation Contract”) will be referred to as assumed-selection. The setof invariants which is selected in the context of a contract application as ensured (e. g.via the “Contract Configurator”) will be referred to as ensured-selection.

4.3.2 Achieving observed state correctness

To achieve observed state correctness there is one important thing to do beside provinga correct combination of proof obligations: every time a method contract mct is used aslemma in a proof one has to show that the contract assumption of mct is fulfilled in thepre-state of the contract application. This can be achieved by selecting the invariantsof the contract assumption as assumed-selection since KeY will automatically createa side branch in the proof tree in which it has to be shown that the assumed-selectionis fulfilled in the pre-state of the contract application.

4.3.3 Problems with the old JML translation

The following problem arose in the context of the application of method contracts: thecase study started with a KeY version which—if the specifications were formulatedin JML—fixed the proof assumption of every proof obligation regarding a methodm or a method contract mct for m to the set of all invariants defined in the sameclass as m. Thus, the contract assumption of every method contract mct was fixedto the set of all invariants defined in the same class as mct. Therefore the contractassumption of a contract mct often contained a lot of invariants which wouldn’t havebeen necessary to assume to verify m against mct. Thus, on every contract applicationone had to show for a lot of invariants superfluously that they were fulfilled in thepre-state of the contract application. While this is feasible for proofs with a smallnumber of contract applications, it becomes impracticable for proofs which involve alot of contract applications. In this context one should be aware of the fact that, ifa method a is verified against its specification, a contract mctb of a method b mightbe applied not only in the case that a invokes b, but in the case that b is used in thespecification of a, too.

Another problem is that sometimes it is necessary to include invariants of variousclasses in the proof assumption of a proof obligation to be able to succeed with its


1 public class Example1 {

2 /*@ public instance invariant x >= 0; @*/

3

4 private /*@ spec_public @*/ int x;

5

6 public Example1() {

7 x = 0;

8 }

9


11 @ requires true;

12 @ ensures \result >= 0;


14 @*/

15 public int a() {

16 return x;

17 }

18


20 @ requires true;


22 @ assignable x;

23 @*/

24 public int b() {

25 x = -1;

26 int y = a();

27 x = 1;

28 return y;

29 }

30 }

Listing 4.1: Contract application example 1. If the user tries to verify the method b()

against its specification and forgets about selecting the invariant x >= 0 when applyingthe method contract of a(), then he is able to succeed with the verification though b()

obviously doesn’t fulfill its contract.

verification. Thus, some proof obligations were not verifiable with the KeY versionused at the beginning.

To overcome these problems, KeY was updated to the newest version (version1.3.204-beta). This version allows to select arbitrary sets of invariants as proof as-sumption even in connection with JML specifications. While the possibility to selectexactly those invariants which are needed to succeed with the verification task actu-ally solved the problems, the update of the KeY version unfortunately forced to redoall proofs. This is related to the fact that the new KeY version provides other proofobligations—the ones described in section 2.2—than the older version. Redoing the

34 4 Case study

proofs took a lot of time which in the end lacked to complete the verification of thesend mechanism.

4.3.4 Book-keeping of the invariant usages

A problem still persisting in the context of the contract application is that the userhas to do the book-keeping of the invariant usages on his own (meaning withoutsupport of KeY). Hence, KeY is not able to check the users assumed-selection inthe “Contract Configurator”. This enables the user to create corrupted proofs byaccidentally forgetting to select an important invariant as demonstrated by the simpleexample in listing 4.1. On the other hand, the probability of accidentally creating acorrupted proof is low if the user does the book-keeping and the invariant selectioncarefully.

4.3.5 A problem with the strategy “Contracts”

In the context of the contract application and the invariant book-keeping another prob-lem existed and still exists in a slightly modified way in the actual KeY version: the(normally very useful) strategy “Contracts” used the empty set as assumed-selectionwhen applying a contract automatically. Thus this strategy was able to create cor-rupted proofs and hence was useless. In the actual KeY version, the invariants of theclass a method contract is defined in is used as assumed-selection. This is a bit betterthan selecting the empty set but corrupted proofs still can be produced. In addi-tion, this selection bears the same problem already discussed at the beginning of thissection: one would have to show all of these invariants on every contract application.

A strategy to overcome these problems could be to implement the strategy “Con-tracts” in a way that the assumed-selection as well as the ensured-selection would beset to the proof assumption. If additionally the proof assumption is set at least to theunion of the contract assumptions of all contracts applicable in the proof (which by theway often is a necessary selection), the strategy “Contracts” would no longer producecorrupted proofs for obvious reasons. Note that this proposal is not only correct butreasonable, too. This is related to the fact that sometimes these choices are necessary:Imagine the situation of listing 4.2. Suppose one wants to show that the method c()

fulfills the proof obligation

EnsuresPost(mctc; {public instance invariant x >= 0;})

for its method contract mctc with the help of the method contract mcta of the methoda() and the method contract mctb of the method b(). Suppose further that thecontract assumption of mcta is the empty set ∅ and that the contract assumption ofmctb is the set Ix := {Φx} with Φx := public instance invariant x >= 0;. Toapply mctb correctly, one has to show that Φx holds in the pre-state of the invocationof b() which is the same program state as the post-state of the invocation of a().Because a() modifies the attribute x, it can’t be ensured offhand that Φx holds afterthe invocation of a(). On the other hand, one is able to ensure that Φx holds after



2 /*@ public instance invariant x >= 0; @*/

3

4 private /*@ spec_public @*/ int x;

5

6 public Example2() {

7 x = 0;

8 }

9


11 @ requires true;

12 @ ensures true;

13 @ assignable x;

14 @*/

15 public void a() {

16 x = 1;

17 }

18


20 @ requires true;



23 @*/

24 public int b() {

25 return x;

26 }

27


29 @ requires true;


31 @ assignable x;

32 @*/

33 public int c() {

34 a();

35 return b();

36 }

37 }

Listing 4.2: Contract application example 2.

the invocation of a() if PreservesInv(m; Ix; Ix) has been shown and if Φx holds in thepre-state of the invocation of a(). As mentioned above, the latter can be ensured bysetting the assumed-selection to Ix when applying mcta . To tell KeY that Φx holdsafter the invocation of a one has to add Φx to the ensured-selection, too. Thus, in thiscase one has to select the proof assumption Ix as assumed-selection as well as ensured-

36 4 Case study

1 /* ---- Used invariants ----

2 * normal_behavior

3 * public instance invariant buffer != null;

4 * public instance invariant buffer .length == BUFFER_SIZE;

5 * public instance invariant offsetsInitialised

6 * ==> -1 <= destinationAddressOffset

7 * && destinationAddressOffset

8 * < buffer. length - Utils. SIZE_OF_LONG;

9 */


11 @ ensures isData ();

12 @ ensures sourceAddressOffset == 8;

13 @ ensures destinationAddressOffset == 6;

14 @ ensures destinationPanOffset == 4;

15 @ ensures payloadOffset == sourceAddressOffset + 8;

16 @ ensures offsetsInitialised == true;

17 @ assignable destinationPanOffset ,

18 @ destinationAddressOffset ,

19 @ sourceAddressOffset , payloadOffset ,

20 @ buffer [ FCF_OFFSET.. FCF_OFFSET+ Utils. SIZE_OF_SHORT -1] ,

21 @ buffer [6..6+ Utils. SIZE_OF_LONG],

22 @ buffer [ LENGTH_OFFSET], offsetsInitialised;

23 @*/

24 private void initAsBroadcast() {

25 setFrameControl( FRAME_TYPE_DATA | INTRA_PAN | DST_ADDR_16 |

SRC_ADDR_64);

26 setOffsets();

27 setDestinationAddress (0 xFFFF);

28 setLength( payloadOffset - 1); // subtract one for length

byte

29 }

Listing 4.3: Method initAsBroadcast() of the class RadioPacket.

selection to be able to succeed with the proof—though the contract assumption ofmcta (the empty set) is merely a subset of the proof assumption. An example for thissituation within the case study is the method initAsBroadcast() of listing 4.3. Inthis case the method setOffsets() plays the role of the method a(), the methodsetDestinationAddress(·) plays the role of the method b() and the third invariantplays the role of Φx.

4.3.6 Using a contract for the verification of itself

A last problem which sometimes lead to corrupted proofs was that—in older KeYversions—it was possible to use a method contract mct for the verification of itself.

4.4 The problem with bit operations and a verification example 37

This was problematic especially in the context of the strategy “Contracts”: every timethe strategy “Contracts” had the chance to use mct for the verification of itself thestrategy did. This of course resulted in corrupted proofs. In the actual KeY versionit is no longer possible to use mct for the verification of itself and thus this problemwith the strategy “Contracts” does no longer exist.

The next section serves two aims: to discuss problems in connection with bit oper-ations and to provide a detailed verification example.

4.4 The problem with bit operations and a verification example

A characteristic of libraries of embedded systems which distinguishes them from “stan-dard” applications is that they normally make extensive use of bit operations. Thisrevealed to be a problem because in the beginning KeY was able to resolve bit oper-ations solely in the case that both operands were concrete numbers. But this is notsufficient—at least in the context of embedded code. Thus, the possibility to expandbit operations for arbitrary operands has been introduced into the actual KeY version.Unfortunately, the expansion of and- and or-operations creates huge terms with a lotof arithmetic operations (cp. listing 4.4) and thus—in most proofs—a user can’t profitfrom it. Hence, in the context of this case study a system of lemmata for bit operationshas been developed. It consists of 120 lemmata and is powerful enough to handle atleast all bit operations occurring in the context of this case study.

The next section gives some notes on the way the lemmata system works. After-wards, section 4.4.2 goes step-by-step through a verification example which makes useof this lemmata system.

4.4.1 The lemmata system

The lemmata system consists of two parts: the “general bit lemmata” and the “res-olution bit lemmata”. The task of the general bit lemmata is mainly to simplify thestructure of nested bit operations and to order nested bit operations in a way whichcan be resolved easily. Additionally, some bit operations can be estimated or elimi-nated directly with the help of the general bit lemmata. If no general bit lemmata isapplicable any more, the resolution bit lemmata can be used to resolve the remainingbit operations per divide and conquer strategy.

General bit lemmata

The general bit lemmata operate on bit operations without altering them mainly byusing the following three ways:

1. by commutation of bit operations (cp. appendix A.1.2),

2. by fusion of bit operations (e. g. and(and(a, b), b) will be replaced by and(a, b);cp. appendix A.1.3) and

38 4 Case study

1 moduloLong(

2 0

3 + toTwoComplJlong(x)/1%2 * ( toTwoComplJlong(y) /1%2) * 1




7 + toTwoComplJlong(x) /16%2 * ( toTwoComplJlong(y)/16%2) * 16



10 + toTwoComplJlong(x) /128%2 * ( toTwoComplJlong(y) /128%2) * 128



13 + toTwoComplJlong(x) /1024%2 * ( toTwoComplJlong(y) /1024%2) *

1024

14 < ... 52 lines skipped ... >

15 + toTwoComplJlong(x) / 9223372036854775808 % 2 * (

toTwoComplJlong(y) / 9223372036854775808 % 2) *

9223372036854775808)

Listing 4.4: Expansion of andJlong.

3. by estimation of bit operations (cp. appendix A.1.4).

For particular reasons the estimation lemmata will work reasonable only if the termsmoduloLong(·) and moduloInt(·) will no further be resolved. Thus, the arithmetictreatment should be set to basic treatment when using the general bit lemmata.1 Whilethe estimation lemmata and the fusion lemmata directly eliminate bit operations, therole of the commutation lemmata is to order the bit operations in a way which

• allows the application of as many fusion lemmata as possible and which

• can be resolved easily in the case that no general bit lemmata are applicable anymore.

The order of bit operations which revealed to be the best in the context of this casestudy is to commutate or-operations outwards, and-operations to the middle and shift-operations to the inner. This can be explained by the fact that shift-operations nor-mally can be resolved easily and that nested and-operations often evaluate to zero.

1 The basic arithmetic treatment provides simplification of polynomial expressions, computation ofGröbner Bases for polynomials in the antecedent and the (partial) Omega procedure for handlinglinear inequations but won’t expand defined symbols like moduloLong(·), moduloInt(·), /, %,inLong(·), inInt(·) etc..


Resolution bit lemmata

After no general bit lemmata is applicable any more, the remaining bit operationsoften can be resolved quite efficiently with the help of the resolution bit lemmata.The resolution lemmata operate on and- and or-operations per divide and conquerstrategy. If xl...xr and yl...yr are bit patterns and bitOp is an and- or or-operation,then the strategy works as follows:

if bitOp(xl . . . xr, yl . . . yr) can be resolved directly thenreturn the result of the direct resolution;

else

m← ⌈ l+r2⌉;

a← resolve bitOp(xl . . . xm, yl . . . ym) recursively;b← resolve bitOp(xm−1 . . . xr, ym−1 . . . yr) recursively;return a · 2m−r + b;

If one considers e. g. the resolution of the term andJlong(x, 4278190080), one getsschematically the following resolution chain (4278190080 equals the bit pattern 03218024):

andJlong(x, 4278190080)

and(x63 . . . x0, 03218024, 64bit)

and(x63 . . . x32, 032, 32bit) · 232 + and(x31 . . . x0, 1

8024, 32bit)

0 · 232 + and(x31 . . . x16, 1808, 16bit) · 216 + and(x15 . . . x0, 0

16, 16bit)

(

and(x31 . . . x24, 18, 8bit) · 28 + and(x23 . . . x16, 0

8, 8bit))

· 216 + 0

((

(x div 224) mod 28)

· 28 + 0)

· 216

(

(x div 224) mod 28)

· 224

As the example shows, the divide and conquer strategy is efficient in the case that atleast one operand consists of a small number of 0 - and 1-blocks. In this case study es-pecially and-operations often have at least one operand of the form 0 . . . 0 1 . . . 1 0 . . . 0.Thus, the divide and conquer strategy can be applied quite efficiently to those terms.All shift-operations occurring in this case study can be expanded efficiently and thusare resolved directly without usage of the divide and conquer strategy.

A disadvantage of the current lemmata system is that KeY is not forced to resolve abit operation directly if possible but has the choice to apply the next step of the divideand conquer strategy instead. This reduces the efficiency of the lemmata system inconnection with the automatic rule application.

Another problem is that not all of the lemmata are verifiable with KeY at themoment. This is due to the high complexity of the expanded and- and or-operationswhich leads to a high consumption of memory. Thus, the lemmata system is more anaxiom system at the moment.

The next section deals with a verification example which has to make use of the

40 4 Case study

lemmata system.

4.4.2 Verification example

The method readLittleEndNumber(·) (cp. listing 4.5) is an example for a methodwith a lot of bit operations and thus provides a good impression on how the lemmatasystem works. Additionally, the proofs regarding this method belong to the mostextensive ones of this case study. This might be surprising because the method isquite small. The size of the proofs results probably from three facts:

1. The method contains a loop.

2. Sometimes the bit operations are not handled optimally by the lemmata system.

3. The proof branches quite strongly.

As the name of the method readLittleEndNumber(·) indicates, this method is usedfor reading numbers (shorts, ints and longs) from a byte array according to the littleendian format. The kind of number to be read is specified by its number of bytes: 2bytes for shorts, 4 bytes for ints and 8 bytes for longs. In any case, the number willbe returned as long and has to be converted to its intended format by the caller.

Specification

The method is specified as follows. The specification consists of three contracts: onefor each kind of number to be read. Each contract specifies a normal_behavior

(thus guarantees normal termination) and consists of three requires-clauses as well asthree ensures-clauses and the assignable-clause “assignable \nothing;”. The firstrequires-clause of each contract specifies the kind of number the contract is used for.The second requires-clause limits the domain of the offset to assure that no Array-

IndexOutOfBoundsException can be thrown. The third requires-clause will be ig-nored for the moment. Its sense will be discussed in section 4.5.4. The task of theensures-clauses is to specify that the result of the method equals the number repre-sented in the byte array. This task consists of two parts:

1. The domain of the result has to be limited to the desired values.

2. It has to be specified that the (i+ offset)-th byte of the buffer equals the bits 8ito 8i+ 7 of the result.

The first part is specified by the former two ensures-clauses of each contract. Theseensures-clauses directly reflect the statement of point 1. The second part is specifiedby the third ensures-clause of each contract. The structure of the third ensures-clauseis visualized by figure 4.1.



2 @ requires numberOfBytes == SIZE_OF_SHORT;

3 @ requires 0 <= offset

4 @ && offset <= byteArray.length - SIZE_OF_SHORT;

5 @ requires byteArray.length <= Integer. MAX_VALUE;

6 @ ensures 0 <= \result ;

7 @ ensures \ result <= ((long)1 << (8* SIZE_OF_SHORT)) - 1;

8 @ ensures (\ forall int i; 0 <= i && i < SIZE_OF_SHORT;

9 @ (((( long) 255) << (8 * i)) & \ result )

10 @ == (( long)( byteArray[offset +i]&255) << (8*i))

11 @ );


13 @ also

14 @ private normal_behavior

15 @ requires numberOfBytes == SIZE_OF_INT;


17 @ && offset <= byteArray.length - SIZE_OF_INT;


19 @ ensures 0 <= \result ;

20 @ ensures \ result <= ((long)1 << (8 * SIZE_OF_INT)) - 1;

21 @ ensures (\ forall int i; 0 <= i && i < SIZE_OF_INT;

22 @ (((( long) 255) << (8 * i)) & \ result )


24 @ );


26 @ also

27 @ private normal_behavior

28 @ requires numberOfBytes == SIZE_OF_LONG;


30 @ && offset <= byteArray.length - SIZE_OF_LONG;


32 @ ensures Long. MIN_VALUE <= \result ;

33 @ ensures \ result <= Long. MAX_VALUE;

34 @ ensures (\ forall int i; 0 <= i && i < SIZE_OF_LONG;

35 @ (((( long) 255) << (8 * i)) & \ result )


37 @ );


39 @*/

40 private /*@ pure @*/ static long readLittleEndNumber(byte []

byteArray , int offset , int numberOfBytes) {

41 long result = 0;

42 for (int i= numberOfBytes -1; i >=0; i--) {

43 result = (result << 8) | ( byteArray[ offset +i] & 0xFF);

44 }

45 return result ;

46 }

Listing 4.5: The method readLittleEndNumber(·) of the class Utils.

42 4 Case study

Figure 4.1: Visualization of the ensures-clause “ensures ( \forall int i; 0

<= i && i < SIZE_OF_INT; ((((long)255)<< (8 * i))& \result)== ((long)(

byteArray[offset+i] & 255)<< (8 * i)));” for offset = 0 and i = 2 (byteArray isabbreviated by b).

Verification

In the remainder of this chapter the verification of the proof obligation EnsuresPost(mctint ; ∅) shall be considered where mctint is the method contract used for integers.

At the beginning the proof obligation has to be loaded (cf. section 2.3.5) and therule application strategies have to be set according to figure 4.2. In case of the methodreadLittleEndNumber(·) the best strategy for handling loops is to unroll them. Thisis due to the fact that in case of the contract mctint the body of the loop occur-ring in the method has to be executed exactly four times. Starting the automaticrule application by clicking on the ◮ -button results in three open goals, one foreach ensures-clause of the contract. The goal which corresponds to the ensures-clause“ensures 0 <= \result;” (figure 4.5) and the goal which corresponds to the ensures-clause “ensures \result <= ((long)1 << (8 * SIZE_OF_INT))- 1;” (figure 4.6) can nofurther be handled without support for estimation of bit operations. Thus, the remain-ing goal (figure 4.7) shall be considered first.

Because the two big estimations (orJlong(·) <= 4294967295 and orJlong(·) >=

0) in the antecedent are fulfilled, one should eliminate them with the rule “replaceknown left” at first. (The rule “replace known left” replaces a formula in the antecedentwith “true”.) The last thing that can be done without the help of bit lemmata is toinstantiate the symbol i_0 by its values 0 to 3. This is reasonable because it is easierto verify the equivalence of the bytes one by one as implied by figure 4.1 than trying toverify the formula at a single blow. The last step transforms the current goal into fournew goals: One for the comparison of each byte of the buffer with the correspondingpart of the result. To close these goals one obviously needs support for bit operations(cp. figure 4.8).

Thus, at this point one should load the bit lemmata located in the files “generalBit-

Lemmata.key” and “resolvingBitLemmata.key” and set the rule application strate-gies according to figure 4.3. Setting the strategy “user-specific taclets 1” to high


Figure 4.2: Rule application strategies at the beginning of the verification of themethod readLittleEndNumber(·).

priority will enable the application of the general bit lemmata (cp. section 4.4.1 andappendix A.1). Because the estimation lemmata will work reasonable only if theterms moduloLong(·) and moduloInt(·) will be resolved no further (cp. section 4.4.1)and because the general bit lemmata themselves introduce terms moduloLong(·) andmoduloInt(·), the arithmetic treatment has been set to basic treatment (cp. fig-ure 4.3).

After starting the automatic rule application again, one obtains several open goals.These can be closed with the help of the resolution bit lemmata (cp. section 4.4.1 andappendix A.2). To enable the resolution lemmata, one has to set the “user-specifictaclets 2” to high priority and the “user-specific taclets 3” to low priority. To getreasonable results, one should set the arithmetic treatment to “DefOps” again (cp.figure 4.4). Starting the automatic rule application (may be a couple of times) shouldclose the remaining goals—at least if the user can provide the required amount of mem-ory. But it is advisable to guide KeY a bit to reduce the required amount of memoryconsiderably. This can be achieved by applying the automatic rule application strat-egy locally to the outermost and-operations first. Afterwards—if all and-operationshave been resolved—the automatic rule application can be applied to the remaining

44 4 Case study

Figure 4.3: Rule application strategies for applying general bit lemmata.

goals more efficiently.The discussion of further problems which have been revealed during the verification

process will be the topic of the next section.


Figure 4.4: Rule application strategies for applying resolution bit lemmata.

46 4 Case study

Figure 4.5: readLittleEndNumber(·) goal 1.

48 4 Case study


50 4 Case study

4.5 Further problems

This section discusses further problems which have been revealed during the verifica-tion process. Additionally, this section proposes some features which might be usefulfor future verifications.

4.5.1 The strategy “Contracts”

Besides the problem already discussed in section 4.3 there is another problem withthe strategy “Contracts”: If a method has more than one contract, the strategy “Con-tracts” selects one of them arbitrarily. Unfortunately, this choice often fells on acontract whose expressiveness is insufficient in the context it is used by the strategy(imagine e. g. the choice of a purity contract in context of an EnsuresPost-proof). Forthis reason the strategy is useless in many cases. A possibility to overcome this prob-lem could be to combine all contracts of a method to one big contract. But this had tobe done by KeY and can not—and should not—be done by the user for three reasons:

• The user has no influence on the creation of the implicit purity contract.

• Combining contracts often makes the specification confusing and proving thecombined contract is often more complicated than proving every part on itsown.

• The combination of contracts normally is not trivial. For example, it is obviouslynot possible to simply pack up pre-conditions and post-conditions. Instead, pre-conditions normally have to be moved into post-conditions. One problem in thiscontext is that this movement has to be done universally for all methods. Forexample, imagine the situation of listing 4.6. If one changes the contract mctb

of b(·) to


2 @ requires true;

3 @ ensures (x >= 0) ==> (\ result == 1);


5 @*/

and leaves the contract mcta of a(·) untouched, then mctb is no longer verifiablewith the help of mcta because the pre-condition of mcta can’t be guaranteed tohold any more. Thus one would have to move the pre-condition of mcta to itspost-condition, too.

4.5.2 Problems regarding the clause “assignable \nothing;”

As mentioned in section 4.2.2, the clause “assignable \nothing;” is interpreted bythe actual KeY version as empty modifier set. And as mentioned in section 2.3, this

4.5 Further problems 51


2 public Example3() {}

3


5 @ requires x >= 0;

6 @ ensures \result == 1;


8 @*/

9 public int a(int x) {

10 if (x >= 0) {

11 return 1;

12 } else {

13 return -1;

14 }

15 }

16


18 @ requires x >= 0;

19 @ ensures \result == 1;


21 @*/

22 public int b(int x) {

23 return a(x);

24 }

25 }

Listing 4.6: Example for moving a pre-condition.

interpretation is not strictly conform to the JML specification: The JML specificatione. g. allows the creation of objects within methods specified as “assignable \nothing;”.This is not allowed within methods specified via an empty modifier set. Thus, somemethods can’t be specified as “assignable \nothing;” in JML specifications usedby KeY which normally would be specified this way. For example, if the methodgetSourceAddress() would be specified via the exceptional_behavior






6 @*/

7 public /*@ pure @*/ long getSourceAddress() {

8 if ( sourceAddressOffset == -1) {

9 throw new IllegalStateException(" Field not valid for

this packet ");

52 4 Case study

10 }

11 return getLongAt( sourceAddressOffset);

12 }

then the RespectsModifies-proof regarding this contract will fail because the contractdoes not allow the creation of the IllegalStateException in KeYs interpretationof the contract. To overcome this problem a new keyword has been introduced: Thekeyword \object_creation(·). This keyword does not belong to the official JMLstandard but will be interpreted by KeY. It can be used in the following way: If anobject of type T is allowed to be created, the term “\object_creation(T)” has to beadded to the assignable-clause as well as to the post-condition. Thus, a specificationof the method getSourceAddress() which can be verified with KeY is the followingone:




4 @ signals ( IllegalStateException)

5 @ \ object_creation( IllegalStateException);

6 @ assignable \ object_creation( IllegalStateException);

7 @*/

It is useful to know that it will be necessary to apply the rule “update_cut” to beable to close the proof of the proof obligation RespectsModifies(mctexp, ∅) when usingthe latter method contract mctexp. This rule has to be applied to the second updateof figure 4.9 and has to be instantiated as follows:

1 {java.lang. IllegalStateException.<nextToCreate >:= nextToCreate_1

||

2 \for int x; \if (x >= java.lang. IllegalStateException.<

nextToCreate >) java.lang. IllegalStateException::<get >(x).<

created >:=

3 created_1(java.lang. IllegalStateException::<get >(x)) ||



initialized >:=

5 initialized_1(java.lang. IllegalStateException ::<get >(x)) ||



transient >:=

7 transient_1(java.lang. IllegalStateException::<get >(x)) ||


nextToCreate >) java.lang. IllegalStateException::<get >(x).

objectTimesFinalized :=

9 objectTimesFinalized_1(java.lang. IllegalStateException::<get

>(x))}


Figure 4.9: Proof regarding getSourceAddress() before applying the update_cut.

54 4 Case study

10 \<{

11 java.lang.Object . anonMethod() @java.lang.Object ;

12 }\> true

Applying the automatic rule application strategy with the arithmetic treatment “Def-Ops” and the normal logical splitting should close the proof.

But there is a situation in which the solution of creating a modified specificationusing the keyword \object_creation(·) instead of “assignable \nothing;” is notapplicable: This is the case if a method is declared as pure. In this case the implicitcontract

1 /*@ private behavior

2 @ requires true;

3 @ diverges false;


5 @*/

will be added automatically to the method by KeY. However, for the method get-

SourceAddress() this contract is obviously not verifiable with respect to KeYs in-terpretation of the contract. On the other hand getSourceAddress() is pure withrespect to the JML standard. And since the JML standard requires methods whichare themselves used in other specifications to be specified as pure (which ensures thatthe method is free from side effects), it is mandatory to specify getSourceAddress()

as pure—at least if one aims to write standard-conforming JML specifications. Thus,here is a gap between JML and its interpretation by KeY which can’t be closed at themoment.

4.5.3 Strongly splitting proofs

The structure of some methods implies that proofs split strongly when they are verifiedwith KeY. This results in extensive proofs which sometimes can’t be closed with anactual standard PC1.

The first kind of such methods are those which invoke a lot of other methods andwhose specifications refer to a lot of methods, too. If they have to be verified againsttheir specifications with the help of method contracts, this can result in very exten-sive proofs. An example for such a method is writeFragmentHeader(·) of the classLowPanPacket:


2 @ requires lph != null;

3 @ requires rp. offsetsInitialised;

1 PCs with up to 3GB RAM.


4 @ requires 0 <= rp. payloadOffset;

5 @ requires 0 <= parseIndex;

6 @ ensures lph. getOutgoingFragType ()

7 @ == LowPanHeader. UNFRAGMENTED

8 @ ==> true;

9 @ ensures lph. getOutgoingFragType ()

10 @ == LowPanHeader. FIRST_FRAGMENT

11 @ ==> rp. getMACPayloadAt(\ old( parseIndex))

12 @ == ( (int) FRAG_FIRST

13 @ | (int)(( byte)(

14 @ (lph. getOutgoingFragSize() >>8) & 7)))

15 @ && parseIndex == \ old( parseIndex) + 4;

16 @ ensures ( lph. getOutgoingFragType ()

17 @ == LowPanHeader. LAST_FRAGMENT

18 @ || lph. getOutgoingFragType ()

19 @ == LowPanHeader. INTERIOR_FRAGMENT)

20 @ ==> rp. getMACPayloadAt(\old( parseIndex))

21 @ == ( (int) FRAG_INTERIOR

22 @ | (int)(( byte)(

23 @ (lph. getOutgoingFragSize() >>8) & 7)))

24 @ && rp. getMACPayloadAt(\ old( parseIndex) + 4)

25 @ == lph. getOutgoingFragOffset ()

26 @ && fragOffsetIndex == \old( parseIndex) + 4

27 @ && parseIndex == \ old( parseIndex) + 5;

28 @ ensures ( lph. getOutgoingFragType ()

29 @ == LowPanHeader. FIRST_FRAGMENT


31 @ == LowPanHeader. LAST_FRAGMENT


33 @ == LowPanHeader. INTERIOR_FRAGMENT)

34 @ ==> rp. getMACPayloadAt(\ old( parseIndex) + 1)

35 @ == (byte)(lph. getOutgoingFragSize () & 255)

36 @ && rp. getMACPayloadShortAt (\ old( parseIndex)+1)

37 @ == (short)(lph. getOutgoingFragTag() & 65535)

38 @ && fragIndex == \old( parseIndex)

39 @ && fragSizeIndex == \old( parseIndex)

40 @ && fragTagIndex == \old( parseIndex) + 2;

41 @ assignable fragIndex , fragSizeIndex , fragTagIndex ,

42 @ fragOffsetIndex , parseIndex ,

43 @ rp. buffer[ parseIndex+rp. getPayloadOffset()..

parseIndex+rp. getPayloadOffset() +4];

44 @*/

45 private void writeFragmentHeader( LowPanHeader lph) {

46 byte b = 0x00;

47 // Initialize top part of first byte

48 switch (lph. getOutgoingFragType()) {

49 case LowPanHeader. UNFRAGMENTED: {

50 //there is no header if we’re unfragmented , silly ’

51 return ;

56 4 Case study

52 }

53 case LowPanHeader. FIRST_FRAGMENT: {

54 b = FRAG_FIRST;

55 break;

56 }

57 case LowPanHeader. LAST_FRAGMENT:

58 case LowPanHeader. INTERIOR_FRAGMENT: {

59 b = FRAG_INTERIOR;

60 break;

61 }

62 }

63 b |= (byte)(( lph. getOutgoingFragSize() >> 8) & 0x07);

64 fragIndex = fragSizeIndex = parseIndex;

65 rp. setMACPayloadAt( parseIndex++, b);

66

67 // last 8 bytes of Size fit in 1 byte

68 rp. setMACPayloadAt( parseIndex++, (byte)(lph.

getOutgoingFragSize() & 0xff));

69

70 // Now two bytes of tag info

71 fragTagIndex = parseIndex;

72 rp. setMACPayloadShortAt( parseIndex++, (short)(lph.

getOutgoingFragTag() & 0xffff));

73 parseIndex++; // skip lower byte we just wrote

74 if (lph. getOutgoingFragType() != LowPanHeader. FIRST_FRAGMENT){

75 fragOffsetIndex = parseIndex;

76 rp. setMACPayloadAt( parseIndex++, lph. getOutgoingFragOffset ()

);

77 }

78 }

This method was not verifiable with 3GB of main memory. Though this problemmight solve itself because the main memory of computers will grow further in future,one should think about whether it wouldn’t be possible to swap the top of the prooftree to the harddisk.

Another kind of such methods are the ones which contain a lot of if-statements. Aquite moderate example for such a method is getLength() of the class LowPanHeader:

1 /**

2 * Calculates the number of bytes this LowPanHeader will take

3 * @return returns the length, in number of bytes , of the

LowPanHeader

4 */

5 /* ---- Used invariants ----

6 * normal_behavior none

7 * purity none

8 */



10 @ ensures \ result

11 @ == meshedHeaderLength( isMeshed())

12 @ + bCastHeaderLength( isBCast())

13 @ + fraggedHeaderLength( isFragged(), isFirstFrag())

14 @ + extendedProtocolLength( isExtendedProtocol ());


16 @*/

17 public /*@ pure @*/ int getLength() {

18 int len = 0; // Protocol Family & Number

19 if (isMeshed()) len += (1 + destLen + origLen);

20 if (isBCast()) len += 2;

21 if (isFragged()) {

22 len += MAX_FRAGMENTATION_HEADER_LENGTH ;

23 if ( isFirstFrag()) len -=1; // first fragments are 1

byte less (no offset byte)

24 }

25 len += ( isExtendedProtocol()) ? 2 : 1;

26 return len;

27 }

Anyhow, the EnsuresPost-proof for this method consists of 42 541 rule applications.

4.5.4 Domains of numbers

When the specification of the method readLittleEndNumber(·) had been consid-ered in section 4.4.2, the explanation of the requires-clause “requires byteArray.

length <= Integer.MAX_VALUE;” had been skipped. This clause normally should besuperfluously because the attribute length is of type int. But when translating theJML specifications to JavaDL in the actual KeY version the information concerningthe restricted domain of the attribute length gets lost and thus has to be addedexplicitly to the specification. This way the requires-clause above guarantees that noArrayIndexOutOfBoundsException will be thrown. These kinds of specifications werenecessary at various locations in the case study.

4.5.5 Proof management

As already mentioned in section 4.1.1, this case study consists of 351 proofs. Thisquite big number of proofs causes management problems:

1. It has to be clear, which proof obligations already have been proven and whichfurther proof obligations have to be shown.

2. If a specification or implementation changes, it has to be tracked which proofshave to be redone.

At the moment the proofs have to be managed by the user without support of KeY.This is unsafe, especially in the second case, because it is difficult to keep track of

58 4 Case study

which changes affect which proofs. Therefore, if the user makes a mistake within theproof management, the global correctness can no longer be guaranteed. Thus, somesupport by KeY would be valuable.

A first step could be to automatically save all successful proofs according to a reason-able structure. This could enable KeY to check at least the first point. Additionally,it would relieve the user from a lot of work.

4.5.6 Incorrect specifications

A problem occurring in connection with the Java integer semantics in an increasingdegree is that mistakes in the specification sometimes are hard to find. For examplethe following specification of the method setLongAt(·) of the class RadioPacket


2 @ requires 0 <= offset;

3 @ requires offset + Utils. SIZE_OF_LONG <= buffer. length ;

4 @ requires Long. MIN_VALUE <= value;

5 @ requires value <= Long. MAX_VALUE;

6 @ ensures getLongAt(offset ) == value;

7 @ assignable buffer [offset .. offset +Utils. SIZE_OF_LONG -1];

8 @*/

9 private void setLongAt(int offset , long value) {

10 Utils. writeLittleEndLong(buffer , offset , value);

11 }

looks well at a first glance. But the verification of setLongAt(·) against this specifica-tion will fail. This is related to the following fact: If offset is chosen big enough, thenan overflow will occur when adding Utils.SIZE_OF_LONG to offset. Thus offset +

Utils.SIZE_OF_LONG will be smaller than buffer.length though offset is biggerthan intended and an ArrayIndexOutOfBoundsException will occur.

The right specification of the method setLongAt(·) is the following one:


2 @ requires 0 <= offset;

3 @ requires offset <= buffer .length - Utils. SIZE_OF_LONG;

4 @ requires Long. MIN_VALUE <= value;

5 @ requires value <= Long. MAX_VALUE;

6 @ ensures getLongAt(offset ) == value;

7 @ assignable buffer [offset .. offset +Utils. SIZE_OF_LONG -1];

8 @*/

In this case no overflow does occur: Utils.SIZE_OF_LONG is a constant with value 8and the invariant “public instance invariant buffer.length == BUFFER_SIZE;” en-sures that the value of buffer.length always equals the constant BUFFER_SIZE whichagain equals the value 128.

4.6 Strengths of KeY 59

Another mistake in a specification which is hard to find occurs if one specifies acontract mct with a pre-condition which resolves to false for some unfortunate cir-cumstances. In this case the proof regarding mct will succeed. This mistake normallywill not be revealed until mct is used as lemma in another proof. Such a proof won’tclose since the pre-condition of mct can’t be fulfilled. But the mistake can revealedby KeY earlier: If a proof closes without the need to expand the body of the relatedmethod, in most cases there will be something wrong (at least if the proof obligationintends the expansion of the method body). Though this can be checked manually bythe user, it would be helpful if KeY would warn the user automatically in the casethat a proof closes without the expansion of the method body.

4.5.7 Labeling of invariants and method contracts

As e. g. the last example in section 4.3 shows, it is a little bit cumbersome to referto particular method contracts and invariants defined in JML because they have noidentifiers. Although this is no “real problem”, it would be nice if JML would offerthe possibility to label method contracts and invariants. This would ease the book-keeping of the invariant usages and make the (manual) selection of invariants (e. g. inthe “Contract Configurator”) a bit more clear.

4.5.8 Additional features which could be useful

In the following some features are listed which are not very important but neverthelesscould be useful.

The first of these features is a search function for terms and formulae in the currentlyselected goal. Sometimes one is quite sure that particular terms or formulae occursomewhere within a goal but it is difficult to find them. Thus, the possibility to searchfor terms and formulae would ease the verification process in such cases.

Secondly, it would be useful if the parsers included in KeY could be called separatelywithout the need to start KeY. This applies especially to the parser responsible forchecking lemmata-files.

At least it would be useful if KeY would display a summary of all user interactions(including the switching of rule application strategies etc.) of a proof when the proof isloaded again. This would be helpful in order to redo proofs if the proof reuse algorithmfails.

Whereas a lot of problems have been discussed in the last sections, the next sectiondeals with KeYs strengths.

4.6 Strengths of KeY

Besides all of the smaller or greater problems discussed in the previous sections oneshould not forget about emphasizing that KeY performs a lot of things well. As usualthe problem with things functioning well is that there is not much to tell about them.Nevertheless, this section is intended to stress some of KeYs strengths.

60 4 Case study

The first thing which should be mentioned is KeYs clear and easy to use userinterface. It concentrates on its main task: To provide a transparent and easy to useinterface to present and manipulate the JavaDL formulae of the goals currently open.The JavaDL formulae in connection with the proof history always reflect the currentstep of the symbolic execution clearly and thus the user always has an overview ofwhat is currently happening (consider the verification example of section 4.4 underthis aspect again). Additionally, the manual application of rules via the focusing andhighlighting mechanism for terms and formulae is easy, efficient, and clear. Thus, theimportant tasks of the user interface are solved very well.

Secondly, the automatic rule application strategy—if one leaves aside the currentproblems with the strategy “Contracts” and the bit operations—performs very well,too, and thus enables a high degree of automatization. This can be substantiated bya median number of 2 interactions per proof as well as an average number of about 7interactions. The number of interactions could be reduced significantly if the problemswith the strategy “Contracts” were solved.

Thus the strength of KeY is to combine an easy and transparent to use user interfacewith a powerful theorem prover.

The next section will summarize the results of the case study and conclude thethesis.

CHAPTER 5

Conclusion

In this case study it has been examined which problems actually occur when applyingsoftware verification to already existing commercial software. For this purpose a partof the Sun SPOT’s network library—the send mechanism of the LoWPAN AdaptionLayer—has been specified with the popular formal specification language JML andverified with the KeY system afterwards. The problems which have been revealed inthis context have been discussed in detail in this thesis. The most annoying problemsare the ones regarding the automated contract application strategy “Contracts” as wellas the low support for bit operations. The lack of a book-keeping system for invariantusages, the lack of a proof management system and the partially high consumptionof memory are further problems which complicate the verification task. To be ableto succeed with the verification, KeY has been adapted to work with the virtualmachine Squawk and a first approach for a lemmata system for bit operations has beendeveloped. But in spite of all these problems this case study shows that principally itis possible to formally verify actual commercial software. However, it is still a timeexpensive task for the reasons mentioned above. On the other hand, the problemsmentioned seem to be solvable (as the solutions proposed for some of the problemsmight show) and thus one is looking forward to future KeY releases.

Readers interested in related work might want to take a look at [Bec07, chapter 14],[Bec07, chapter 15], [Mos07] or [Sch07]. [Bec07, chapter 14] considers the verificationof the commercial program “Demoney” with KeY. The implementation of Demoneyis based on the Java Card specification. Thus, this case study discusses particularlysome Java Card related aspects. [Bec07, chapter 15] discusses the formal verifica-tion of a Java implementation of the Schorr-Waite-Algorithm and hence provides anexample of the verification of the implementation of a complex algorithm. The im-plementation has been specified via JavaDL and verified with KeY. [Mos07] considersthe verification of a reference implementation of the Java Card API—also with KeYin connection with JavaDL. Finally, [Mos07] examines the verification of the MondexCase Study. Mondex is an electronic purse hosted on a smart card. The consideredJava Card implementation of the Mondex protocoll has been specified with JML andverified with KeY.

62 5 Conclusion

APPENDIX A

Lemmata

A.1 General bit lemmata

General rule set for the manipulation of bit-operations.The heuristics “simplify” within some of these rules should be replaced by a better

fitting heuristics (which should have a higher priority than the heuristics “userTa-clets3”).

Strategy Priority

userTaclets1 highuserTaclets2 off (reserved for resolution rules)userTaclets3 off (reserved for resolution rules)

The schema variables used in this rule set are defined as follows:


2 \term int x, y, z, a, b, c, offset ;

3 \term jlong jlx , jly , jlz;

4 \term numbers m, n;

5 \term jbyte getByte1 , getByte2;

6 \term jbyte [] byteArray;

7 \ variables jint i, j;

8 \ variables int r;

9 }

A.1.1 Zero simplification lemmata

Listing A.1: Lemma andZeroJlong.

1 /** @proof lemmata/ andZeroJlong.proof ( definition) */

2 andZeroJlong {

64 A Lemmata

3 \find(

4 andJlong(x, 0)

5 )

6 \ sameUpdateLevel

7 \ replacewith(

8 0

9 )

10 \ heuristics(simplify)

11 };

Listing A.2: Lemma andZeroJint.

1 /** @proof lemmata/ andZeroJint.proof ( definition) */

2 andZeroJint {

3 \find(

4 andJint(x, 0)

5 )

6 \ sameUpdateLevel

7 \ replacewith(

8 0

9 )


11 };

A.1.2 Commutation lemmata

Listing A.3: Lemma swapNumberToTheRightAndJlong.

1 /** @proof lemmata/ swapNumberToTheRightAndJlong .proof (

definition) */

2 swapNumberToTheRightAndJlong {

3 \find(

4 andJlong(Z(n), y)

5 )

6 \ sameUpdateLevel

7 \ replacewith(

8 andJlong(y, Z(n))

9 )


11 };

Listing A.4: Lemma swapNumberToTheRightAndJint.

A.1 General bit lemmata 65

1 /** @proof lemmata/ swapNumberToTheRightAndJint . proof ( definition

) */

2 swapNumberToTheRightAndJint {

3 \find(

4 andJint(Z(n), y)

5 )

6 \ sameUpdateLevel

7 \ replacewith(

8 andJint(y, Z(n))

9 )


11 };

Listing A.5: Lemma swapNumberToTheRightOrJlong.

1 /** @proof lemmata/ swapNumberToTheRightOrJlong . proof ( definition

) */

2 swapNumberToTheRightOrJlong {

3 \find(

4 orJlong(Z(n), y)

5 )

6 \ sameUpdateLevel

7 \ replacewith(

8 orJlong(y, Z(n))

9 )


11 };

Listing A.6: Lemma swapNumberToTheRightOrJint.

1 /** @proof lemmata/ swapNumberToTheRightOrJint .proof ( definition)

*/

2 swapNumberToTheRightOrJint {

3 \find(

4 orJint (Z(n), y)

5 )

6 \ sameUpdateLevel

7 \ replacewith(

8 orJint (y, Z(n))

9 )


11 };

66 A Lemmata

Listing A.7: Lemma swapNumberToInnerAndJlong.

1 swapNumberToInnerAndJlong {

2 \find(

3 andJlong( andJlong(x, Z(n)), Z(m))

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 andJlong(x, andJlong(Z(n), Z(m)))

8 )


10 };

Listing A.8: Lemma swapNumberToInnerAndJint.

1 swapNumberToInnerAndJint {

2 \find(

3 andJint(andJint(x, Z(n)), Z(m))

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 andJint(x, andJint(Z(n), Z(m)))

8 )


10 };

Listing A.9: Lemma swapNumberToInnerOrJlong.

1 swapNumberToInnerOrJlong {

2 \find(

3 orJlong(orJlong(x, Z(n)), Z(m))

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 orJlong(x, orJlong(Z(n), Z(m)))

8 )


10 };

Listing A.10: Lemma swapNumberToInnerOrJint.

1 swapNumberToInnerOrJint {

2 \find(

3 orJint( orJint(x, Z(n)), Z(m))


4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 orJint (x, orJint (Z(n), Z(m)))

8 )


10 };

Listing A.11: Lemma shiftleftAndJlong.

1 shiftleftAndJlong {

2 \find(

3 shiftleftJlong( andJlong(x, y), z)

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 andJlong( shiftleftJlong(x, z), shiftleftJlong(y, z))

8 )


10 };

Listing A.12: Lemma shiftleftOrJlong.

1 shiftleftOrJlong {

2 \find(

3 shiftleftJlong( orJlong(x, y), z)

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 orJlong( shiftleftJlong(x, z), shiftleftJlong(y, z))

8 )


10 };

Listing A.13: Lemma shiftleftAndJint.

1 shiftleftAndJint {

2 \find(

3 shiftleftJint( andJint(x, y), z)

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 andJint( shiftleftJint(x, z), shiftleftJint(y, z))

8 )

68 A Lemmata


10 };

Listing A.14: Lemma shiftleftOrJint.

1 shiftleftOrJint {

2 \find(

3 shiftleftJint( orJint (x, y), z)

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 orJint( shiftleftJint(x, z), shiftleftJint(y, z))

8 )


10 };

Listing A.15: Lemma andOrJlong.

1 andOrJlong {

2 \find(

3 andJlong(orJlong(x, y), z)

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 orJlong(andJlong(x, z), andJlong(y, z))

8 )


10 };

Listing A.16: Lemma andOrJint.

1 /** @proof lemmata/ andOrJint.proof ( cognet) */

2 andOrJint {

3 \find(

4 andJint(orJint (x, y), z)

5 )

6 \ sameUpdateLevel

7 \ replacewith(

8 orJint( andJint(x, z), andJint(y, z))

9 )


11 };


A.1.3 Fusion lemmata

Listing A.17: Lemma mergeAndJlong.

1 mergeAndJlong {

2 \find(

3 andJlong( andJlong(x, a), a)

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 andJlong(x, a)

8 )

9 \ heuristics( simplify)

10 };

Listing A.18: Lemma mergeAndJint.

1 /** @proof lemmata/ mergeAndJint.proof (cognet ) */

2 mergeAndJint {

3 \find(

4 andJint( andJint(x, a), a)

5 )

6 \ sameUpdateLevel

7 \ replacewith(

8 andJint(x, a)

9 )


11 };

Listing A.19: Lemma mergeAndJlongAndJint.

1 mergeAndJlongAndJint {

2 \find(

3 andJlong( andJint(x, a), a)

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 andJint(x, a)

8 )


10 };

70 A Lemmata

Listing A.20: Lemma mergeAndJintAndJlong.

1 mergeAndJintAndJlong {

2 \find(

3 andJint(andJlong(x, a), a)

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 andJint(x, a)

8 )


10 };

Listing A.21: Lemma mergeOrJlong.

1 mergeOrJlong {

2 \find(

3 orJlong(orJlong(x, a), a)

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 orJlong(x, a)

8 )


10 };

Listing A.22: Lemma mergeOrJint.

1 /** @proof lemmata/ mergeOrJint.proof (cognet ) */

2 mergeOrJint {

3 \find(

4 orJint( orJint(x, a), a)

5 )

6 \ sameUpdateLevel

7 \ replacewith(

8 orJint(x, a)

9 )


11 };

Listing A.23: Lemma mergeOrJintOrJlong.

1 mergeOrJintOrJlong {

2 \find(


3 orJint (orJlong(x, a), a)

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 orJint (x, a)

8 )


10 };

Listing A.24: Lemma mergeModuloLongAndJlong.

1 /** @proof lemmata/ mergeModuloLongAndJlong.proof ( resolution

lemmata) */

2 mergeModuloLongAndJlong {

3 \find(

4 moduloLong( andJlong(x, y))

5 )

6 \ sameUpdateLevel

7 \ replacewith(

8 andJlong(x, y)

9 )


11 };

Listing A.25: Lemma mergeModuloIntAndJint.

1 /** @proof lemmata/ mergeModuloIntAndJint. proof ( resolution

lemmata) */

2 mergeModuloIntAndJint {

3 \find(

4 moduloInt(andJint(x, y))

5 )

6 \ sameUpdateLevel

7 \ replacewith(

8 andJint(x, y)

9 )


11 };

Listing A.26: Lemma mergeModuloLongAndJint.

1 /** @proof lemmata/ mergeModuloLongAndJint.proof ( resolution

lemmata) */

2 mergeModuloLongAndJint {

72 A Lemmata

3 \find(

4 moduloLong(andJint(x, y))

5 )

6 \ sameUpdateLevel

7 \ replacewith(

8 andJint(x, y)

9 )


11 };

Listing A.27: Lemma mergeModuloLongOrJlong.

1 /** @proof lemmata/ mergeModuloLongOrJlong.proof ( resolution

lemmata) */

2 mergeModuloLongOrJlong {

3 \find(

4 moduloLong(orJlong(x, y))

5 )

6 \ sameUpdateLevel

7 \ replacewith(

8 orJlong(x, y)

9 )


11 };

Listing A.28: Lemma mergeModuloIntOrJint.

1 /** @proof lemmata/ mergeModuloIntOrJint.proof ( resolution

lemmata) */

2 mergeModuloIntOrJint {

3 \find(

4 moduloInt( orJint(x, y))

5 )

6 \ sameUpdateLevel

7 \ replacewith(

8 orJint(x, y)

9 )


11 };

Listing A.29: Lemma mergeModuloLongOrJint.

1 /** @proof lemmata/ mergeModuloLongOrJint.proof ( resolution

lemmata) */


2 mergeModuloLongOrJint {

3 \find(

4 moduloLong(orJint (x, y))

5 )

6 \ sameUpdateLevel

7 \ replacewith(

8 orJint (x, y)

9 )


11 };

Listing A.30: Lemma mergeModuloLongShiftleftJlong.

1 mergeModuloLongShiftleftJlong {

2 \find(

3 moduloLong( shiftleftJlong(x, y))

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 shiftleftJlong(x, y)

8 )


10 };

Listing A.31: Lemma mergeModuloIntShiftleftJint.

1 mergeModuloIntShiftleftJint {

2 \find(

3 moduloInt( shiftleftJint(x, y))

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 shiftleftJint(x, y)

8 )


10 };

Listing A.32: Lemma mergeModuloLongShiftleftJint.

1 mergeModuloLongShiftleftJint {

2 \find(

3 moduloLong( shiftleftJint(x, y))

4 )

5 \ sameUpdateLevel

74 A Lemmata

6 \ replacewith(

7 shiftleftJint(x, y)

8 )


10 };

A.1.4 Estimation lemmata

Listing A.33: Lemma estimateOrJlongN1.

1 estimateOrJlongN1 {

2 \find(orJlong(x, y) <= -1)

3 \ sameUpdateLevel

4 \ replacewith( moduloLong(x) <= -1 | moduloLong(y) <= -1)


6 };

Listing A.34: Lemma estimateOrJintN1.

1 estimateOrJintN1 {

2 \find(orJint (x, y) <= -1)

3 \ sameUpdateLevel

4 \ replacewith( moduloInt(x) <= -1 | moduloInt(y) <= -1)


6 };

Listing A.35: Lemma estimateOrJlong256.

1 estimateOrJlong256 {

2 \find(orJlong(x, y) >= 256)

3 \ sameUpdateLevel

4 \ replacewith( moduloLong(x) >= 256 | moduloLong(y) >= 256)


6 };

Listing A.36: Lemma estimateOrJint256.

1 estimateOrJint256 {

2 \find(orJint (x, y) >= 256)

3 \ sameUpdateLevel

4 \ replacewith( moduloInt(x) >= 256 | moduloInt(y) >= 256)



6 };



2 \find( orJlong(x, y) >= 65536)

3 \ sameUpdateLevel

4 \ replacewith( moduloLong(x) >= 65536 | moduloLong(y) >=

65536)


6 };



2 \find( orJint(x, y) >= 65536)

3 \ sameUpdateLevel

4 \ replacewith( moduloInt(x) >= 65536 | moduloInt(y) >= 65536)


6 };



2 \find( orJlong(x, y) >= 16777216)

3 \ sameUpdateLevel


16777216)


6 };



2 \find( orJint(x, y) >= 16777216)

3 \ sameUpdateLevel

4 \ replacewith( moduloInt(x) >= 16777216 | moduloInt(y) >=

16777216)


6 };

76 A Lemmata



2 \find(orJlong(x, y) >= 4294967296)

3 \ sameUpdateLevel


4294967296)


6 };



2 \find(orJlong(x, y) >= 1099511627776)

3 \ sameUpdateLevel

4 \ replacewith( moduloLong(x) >= 1099511627776 | moduloLong(y)

>= 1099511627776)


6 };



2 \find(orJlong(x, y) >= 281474976710656)

3 \ sameUpdateLevel

4 \ replacewith( moduloLong(x) >= 281474976710656 | moduloLong(y

) >= 281474976710656)


6 };



2 \find(orJlong(x, y) >= 72057594037927936)

3 \ sameUpdateLevel

4 \ replacewith( moduloLong(x) >= 72057594037927936 | moduloLong

(y) >= 72057594037927936)


6 };


A.1.5 Comparison lemmata

Listing A.45: Lemma compareShortsPerByte.

1 compareShortsPerByte {

2 \find(

3 ==>

4 x = y

5 )

6 \varcond(

7 \ notFreeIn(i, x),

8 \ notFreeIn(i, y)

9 )

10 \add(

11 ( short_MIN <= x & x <= short_MAX

12 & short_MIN <= y & y <= short_MAX

13 | 0 <= x & x <= short_RANGE

14 & 0 <= y & y <= short_RANGE

15 )

16 & \ forall i; (

17 i <= -1

18 | i >= 2

19 | andJlong(x, shiftleftJlong(255 , 8 * i)) =

andJlong(y, shiftleftJlong(255 , 8 * i))

20 )

21 -> x = y

22 ==>

23 )

24 };

Listing A.46: Lemma compareIntsPerByte.

1 compareIntsPerByte {

2 \find(

3 ==>

4 x = y

5 )

6 \varcond(


8 \ notFreeIn(i, y)

9 )

10 \add(

11 ( int_MIN <= x & x <= int_MAX

12 & int_MIN <= y & y <= int_MAX

13 | 0 <= x & x <= int_RANGE

14 & 0 <= y & y <= int_RANGE

15 )

78 A Lemmata

16 & \forall i; (

17 i <= -1

18 | i >= 4



20 )

21 -> x = y

22 ==>

23 )

24 };

Listing A.47: Lemma compareLongsPerByte.

1 compareLongsPerByte {

2 \find(

3 ==>

4 x = y

5 )

6 \ varcond(


8 \ notFreeIn(i, y)

9 )

10 \add(

11 ( long_MIN <= x & x <= long_MAX

12 & long_MIN <= y & y <= long_MAX

13 | 0 <= x & x <= long_RANGE

14 & 0 <= y & y <= long_RANGE

15 )

16 & \forall i; (

17 i <= -1

18 | i >= 8



20 )

21 -> x = y

22 ==>

23 )

24 };

A.2 Resolution bit lemmata

General rule set for the resolution of bit-operations. This rule set is more efficientthan the direct expansion of bit-operations. Shift-operations—at least ilk, which have anumber as second parameter—are resolved by the rule set of “integerBitwiseRules.key”.

A.2 Resolution bit lemmata 79

The heuristics “simplify” within some of these rules should be replaced by a betterfitting heuristics (which should have a higher priority than the heuristics “userTa-clets3”).

Strategy Priority

userTaclets1 offuserTaclets2 high (direct resolution of special terms)userTaclets3 low (translation and resolution per divide and conquer)

The schema variables and functions used in this rule set are defined as follows:


2 \term int x, y, z, a, b, c, offset ;

3 \term jlong jlx , jly , jlz;

4 \term numbers m, n;

5 \term jbyte getByte1 , getByte2;

6 \term jbyte [] byteArray;

7 \ variables jint i, j;

8 \ variables int r;

9 }

10

11 \ functions {

12 int twoToThePowerOf(int);

13 int andBitwise(int , int , int);

14 int orBitwise(int , int , int);

15 int calculateLowerBitAndBitwise (int , int , int);

16 int calculateLowerBitOrBitwise (int , int , int);

17 }

A.2.1 Translation lemmata

Listing A.48: Lemma translateAndJlong_automatic.

1 translateAndJlong_automatic {

2 \find(

3 andJlong(x, Z(n))

4 )

5 \ sameUpdateLevel

6 \ replacewith(


toTwoComplJlong(Z(n)), 64))

8 )


10 };

80 A Lemmata

Listing A.49: Lemma translateAndJint_automatic.

1 translateAndJint_automatic {

2 \find(

3 andJint(x, Z(n))

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 moduloInt( andBitwise( toTwoComplJint(x), toTwoComplJint(Z

(n)), 32))

8 )


10 };

Listing A.50: Lemma translateOrJlong_automatic.

1 translateOrJlong_automatic {

2 \find(

3 orJlong(x, Z(n))

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 moduloLong(orBitwise( toTwoComplJlong(x), toTwoComplJlong

(Z(n)), 64))

8 )


10 };

Listing A.51: Lemma translateOrJint_automatic.

1 translateOrJint_automatic {

2 \find(

3 orJint(x, Z(n))

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 moduloInt( orBitwise( toTwoComplJint(x), toTwoComplJint(Z(

n)), 32))

8 )


10 };

Listing A.52: Lemma translateAndJlong.


1 translateAndJlong {

2 \find(

3 andJlong(x, y)

4 )

5 \ sameUpdateLevel

6 \ replacewith(


toTwoComplJlong(y), 64))

8 )

9 };

Listing A.53: Lemma translateAndJint.

1 translateAndJint {

2 \find(

3 andJint(x, y)

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 moduloInt( andBitwise( toTwoComplJint(x), toTwoComplJint(y

), 32))

8 )

9 };

Listing A.54: Lemma translateOrJlong.

1 translateOrJlong {

2 \find(

3 orJlong(x, y)

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 moduloLong( orBitwise( toTwoComplJlong(x), toTwoComplJlong

(y), 64))

8 )

9 };

Listing A.55: Lemma translateOrJint.

1 translateOrJint {

2 \find(

3 orJint (x, y)

4 )

5 \ sameUpdateLevel

82 A Lemmata

6 \ replacewith(

7 moduloInt( orBitwise( toTwoComplJint(x), toTwoComplJint(y)

, 32))

8 )

9 };

A.2.2 Commutation lemmata

Listing A.56: Lemma swapNumberToTheRightAnd.

1 swapNumberToTheRightAnd {

2 \find(

3 andBitwise(Z(n), y, z)

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 andBitwise(y, Z(n), z)

8 )


10 };

Listing A.57: Lemma swapNumberToTheRightOr.

1 swapNumberToTheRightOr {

2 \find(

3 orBitwise(Z(n), y, z)

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 orBitwise(y, Z(n), z)

8 )


10 };

A.2.3 Resolution lemmata AND

Listing A.58: Lemma resolveAndBitwise.

1 resolveAndBitwise {

2 \find(

3 andBitwise(x, y, Z(n))

4 )


5 \ sameUpdateLevel

6 \ replacewith(

7 \if(Z(n) % 2 = 0)

8 \then(

9 andBitwise(x / twoToThePowerOf(Z(n) / 2), y

/ twoToThePowerOf(Z(n) / 2), Z(n) / 2)

10 * twoToThePowerOf(Z(n) / 2)

11 + andBitwise(x % twoToThePowerOf(Z(n) / 2), y %

twoToThePowerOf(Z(n) / 2), Z(n) / 2)

12 )

13 \else(

14 calculateLowerBitAndBitwise (x, y, Z(n))

15 )

16 )

17 };

Listing A.59: Lemma resolveAndBitwise64.

1 resolveAndBitwise64 {

2 \find(

3 andBitwise(x, y, 64)

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 andBitwise(x / int_RANGE , y / int_RANGE , 32) *

int_RANGE

8 + andBitwise(x % int_RANGE , y % int_RANGE , 32)

9 )


11 };



2 \find(


4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 andBitwise(x / short_RANGE , y / short_RANGE , 16) *

short_RANGE

8 + andBitwise(x % short_RANGE , y % short_RANGE , 16)

9 )


11 };

84 A Lemmata



2 \find(


4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 andBitwise(x / byte_RANGE , y / byte_RANGE , 8) *

byte_RANGE

8 + andBitwise(x % byte_RANGE , y % byte_RANGE , 8)

9 )


11 };



2 \find(


4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 andBitwise(x / 16, y / 16, 4) * 16

8 + andBitwise(x % 16, y % 16, 4)

9 )


11 };



2 \find(


4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 andBitwise(x / 4, y / 4, 2) * 4

8 + andBitwise(x % 4, y % 4, 2)

9 )


11 };




2 \find(


4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 andBitwise(x / 2, y / 2, 1) * 2

8 + andBitwise(x % 2, y % 2, 1)

9 )


11 };



2 \find(


4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 x % 2 * y % 2

8 )


10 };

Listing A.66: Lemma calculateLowerBitAnd.

1 calculateLowerBitAnd {

2 \find(


4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 \if(

8 x % 2 = 0

9 | y % 2 = 0

10 )

11 \then(

12 andBitwise(x / 2, y / 2, Z(n) - 1) * 2

13 )

14 \else(

15 andBitwise(x / 2, y / 2, Z(n) - 1) * 2 + 1

16 )

17 )


86 A Lemmata

19 };

Listing A.67: Lemma andZero.

1 andZero {

2 \find( andBitwise(x, 0, z))

3 \ sameUpdateLevel

4 \ replacewith(0)


6 };

Listing A.68: Lemma andBitwise3.

1 andBitwise3 {

2 \find ( andBitwise(x, 3, 2))

3 \ replacewith (x % 4)


5 };


1 andBitwise15 {

2 \find ( andBitwise(x, 15, 4))



5 };


1 andBitwise255 {

2 \find ( andBitwise(x, 255 , 8))



5 };


1 andBitwise65535 {

2 \find ( andBitwise(x, 65535 , 16))



5 };



1 andBitwise4294967295 {

2 \find (andBitwise(x, 4294967295 , 32))

3 \ replacewith (x % 4294967296)


5 };


1 andBitwise18446744073709551615 {

2 \find (andBitwise(x, 18446744073709551615, 64))

3 \ replacewith (x % 18446744073709551616)


5 };

A.2.4 Resolution lemmata OR

Listing A.74: Lemma resolveOrBitwise.

1 resolveOrBitwise {

2 \find(

3 orBitwise(x, y, Z(n))

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 \if(Z(n) % 2 = 0)

8 \then(

9 orBitwise(x / twoToThePowerOf(Z(n) / 2), y /


10 * twoToThePowerOf(Z(n) / 2)

11 + orBitwise(x % twoToThePowerOf(Z(n) / 2), y %


12 )

13 \else(

14 calculateLowerBitOrBitwise (x, y, Z(n))

15 )

16 )

17 };

Listing A.75: Lemma resolveOrBitwise64.

1 resolveOrBitwise64 {

88 A Lemmata

2 \find(

3 orBitwise(x, y, 64)

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 orBitwise(x / int_RANGE , y / int_RANGE , 32) *

int_RANGE

8 + orBitwise(x % int_RANGE , y % int_RANGE , 32)

9 )


11 };



2 \find(


4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 orBitwise(x / short_RANGE , y / short_RANGE , 16) *

short_RANGE

8 + orBitwise(x % short_RANGE , y % short_RANGE , 16)

9 )


11 };



2 \find(


4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 orBitwise(x / byte_RANGE , y / byte_RANGE , 8) *

byte_RANGE

8 + orBitwise(x % byte_RANGE , y % byte_RANGE , 8)

9 )


11 };




2 \find(


4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 orBitwise(x / 16, y / 16, 4) * 16

8 + orBitwise(x % 16, y % 16, 4)

9 )


11 };



2 \find(


4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 orBitwise(x / 4, y / 4, 2) * 4

8 + orBitwise(x % 4, y % 4, 2)

9 )


11 };



2 \find(


4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 orBitwise(x / 2, y / 2, 1) * 2

8 + orBitwise(x % 2, y % 2, 1)

9 )


11 };



90 A Lemmata

2 \find(


4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 x % 2 + y % 2 - (x % 2) * (y % 2)

8 )


10 };

Listing A.82: Lemma calculateLowerBitOr.

1 calculateLowerBitOr {

2 \find(


4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 \if(

8 x % 2 = 0

9 & y % 2 = 0

10 )

11 \then(

12 orBitwise(x / 2, y / 2, Z(n) - 1) * 2

13 )

14 \else(

15 orBitwise(x / 2, y / 2, Z(n) - 1) * 2 + 1

16 )

17 )


19 };

Listing A.83: Lemma orZero.

1 orZero {

2 \find( orBitwise(x, 0, z))

3 \ sameUpdateLevel

4 \ replacewith(x % twoToThePowerOf(z))


6 };

Listing A.84: Lemma or2BitWith3.

1 or2BitWith3 {


2 \find (orBitwise(x, 3, 2))

3 \ replacewith (3)


5 };


1 or4BitWith15 {

2 \find (orBitwise(x, 15, 4))

3 \ replacewith (15)


5 };


1 or8BitWith255 {

2 \find (orBitwise(x, 255 , 8))



5 };


1 or16BitWith65535 {

2 \find (orBitwise(x, 65535 , 16))



5 };


1 or32BitWith4294967295 {

2 \find (orBitwise(x, 4294967295 , 32))

3 \ replacewith (4294967295)


5 };


1 or64BitWith18446744073709551615 {

92 A Lemmata

2 \find ( orBitwise(x, 18446744073709551615, 64))

3 \ replacewith (18446744073709551615)


5 };

A.2.5 Direct resolution lemmata

Listing A.90: Lemma orZeroJlong.

1 /** @proof lemmata/ orZeroJlong.proof ( resolution lemmata) */

2 orZeroJlong { andJint7

3 \find(

4 orJlong(x, 0)

5 )

6 \ sameUpdateLevel

7 \ replacewith(

8 moduloLong(x)

9 )


11 };

Listing A.91: Lemma orZeroJint.

1 /** @proof lemmata/ orZeroJlong.proof ( resolution lemmata) */

2 orZeroJint {

3 \find(

4 orJint(x, 0)

5 )

6 \ sameUpdateLevel

7 \ replacewith(

8 moduloInt(x)

9 )


11 };

Listing A.92: Lemma andJlong7.

1 /** @proof lemmata/ andJlong7.proof */

2 andJlong7 {

3 \find ( andJlong(x, 7))

4 \ replacewith ( toTwoComplJlong(x) % 8)


6 };


Listing A.93: Lemma andJint7.

1 /** @proof lemmata/ andJint7. proof */

2 andJint7 {

3 \find (andJint(x, 7))

4 \ replacewith ( toTwoComplJint(x) % 8)


6 };


1 /** @proof lemmata/ andJlong15.proof */

2 andJlong15 {

3 \find (andJlong(x, 15))



6 };


1 /** @proof lemmata/ andJint15.proof */

2 andJint15 {




6 };


1 /** @proof lemmata/ andJlong255. proof */

2 andJlong255 {

3 \find (andJlong(x, 255))



6 };


1 /** @proof lemmata/ andJint255.proof */

2 andJint255 {



94 A Lemmata


6 };


1 andJlong65535 {

2 \find ( andJlong(x, 65535) )



5 };


1 andJint65535 {

2 \find ( andJint(x, 65535) )



5 };


1 andJlong16777215 {

2 \find ( andJlong(x, 16777215))



5 };


1 andJint16777215 {

2 \find ( andJint(x, 16777215))



5 };


1 andJlong4294967295 {

2 \find ( andJlong(x, 4294967295))



5 };



1 andJint4294967295 {

2 \find (andJint(x, 4294967295))

3 \ replacewith ( moduloInt( toTwoComplJint(x) % 4294967296))


5 };


1 andJlong1099511627775 {

2 \find (andJlong(x, 1099511627775))



5 };


1 andJlong281474976710655 {

2 \find (andJlong(x, 281474976710655))



5 };


1 andJlong72057594037927935 {

2 \find (andJlong(x, 72057594037927935))



5 };


1 andJlong18446744073709551615 {

2 \find (andJlong(x, 18446744073709551615))

3 \ replacewith ( moduloLong( toTwoComplJlong(x) %

18446744073709551616))


5 };

96 A Lemmata

A.2.6 Resolution lemmata twoToThePowerOf

Listing A.108: Lemma resolve2ToThePowerOfX.

1 resolve2ToThePowerOfX {

2 \find(

3 twoToThePowerOf(Z(n))

4 )

5 \ sameUpdateLevel

6 \ replacewith(

7 \if(Z(n) % 2 = 0)

8 \then( twoToThePowerOf(Z(n) / 2) * twoToThePowerOf(Z(n) /

2))

9 \else (2 * twoToThePowerOf(Z(n) - 1))

10 )

11 };

Listing A.109: Lemma resolve2ToThePowerOf0.

1 resolve2ToThePowerOf0 {

2 \find( twoToThePowerOf(0))

3 \ sameUpdateLevel

4 \ replacewith(1)


6 };




3 \ sameUpdateLevel

4 \ replacewith(2)


6 };




3 \ sameUpdateLevel

4 \ replacewith(4)


6 };





3 \ sameUpdateLevel

4 \ replacewith(16)


6 };




3 \ sameUpdateLevel

4 \ replacewith(256)


6 };



2 \find( twoToThePowerOf (16))

3 \ sameUpdateLevel



6 };




3 \ sameUpdateLevel



6 };




3 \ sameUpdateLevel

4 \ replacewith(18446744073709551616)

98 A Lemmata


6 };

A.2.7 Misk bit lemmata

Listing A.117: Lemma forceCalculateLowerBitAnd.

1 forceCalculateLowerBitAnd {

2 \find(

3 andBitwise(x, y, Z(n))

4 )

5 \ sameUpdateLevel

6 \ replacewith(


8 )

9 };

Listing A.118: Lemma forceCalculateLowerBitOr.

1 forceCalculateLowerBitOr {

2 \find(

3 orBitwise(x, y, Z(n))

4 )

5 \ sameUpdateLevel

6 \ replacewith(


8 )

9 };

A.3 Additional bit lemmata

Listing A.119: Lemma byteEquivalenceHighLevel.

1 byteEquivalenceHighLevel {

2 \ assumes(

3 \ forall i; (

4 i <= -1

5 | i >= Z(n)

6 | shiftleftJlong(

7 moduloLong( andJint(getByte1 ,255)),

8 mulJint(8, i)

A.3 Additional bit lemmata 99

9 )

10 = andJlong( shiftleftJlong( moduloLong(255) ,

mulJint(8, i)), x)

11 ),

12 \forall j; (

13 j <= -1

14 | j >= Z(n)

15 | shiftleftJlong(

16 moduloLong( andJint(getByte2 ,255)),

17 mulJint(8, j)

18 )

19 = andJlong( shiftleftJlong( moduloLong(255) ,

mulJint(8, j)), y)

20 ) ==>

21 )

22 \varcond(

23 \ notFreeIn(j, getByte1),

24 \ notFreeIn(i, getByte2),


26 \ notFreeIn(j, x),

27 \ notFreeIn(i, y),

28 \ notFreeIn(j, y),

29 \ notFreeIn(i, n),

30 \ notFreeIn(j, n)

31 )

32 \add( ( ( 0 < Z(n) & Z(n) < 8

33 & -shiftleftJlong(1, 8 * Z(n) - 1) <= x

34 & x <= shiftleftJlong(1, (8 * Z(n))) - 1

35 & -shiftleftJlong(1, 8 * Z(n) - 1) <= y

36 & y <= shiftleftJlong(1, (8 * Z(n))) - 1)

37 | ( Z(n) = 8

38 & inLong(x)

39 & inLong(y)

40 )

41 )

42 & \ forall i; (i <= -1 | i >= Z(n) | getByte1 = {\ subst

j; i}getByte2)

43 -> x = y

44 ==>

45 )

46 };

Listing A.120: Lemma byteEquivalenceLowLevel.

1 byteEquivalenceLowLevel {

2 \assumes(

3 \forall i; (

4 i <= -1

100 A Lemmata

5 | i >= Z(n)

6 | shiftleftJlong(

7 andJint(getByte1 , 255) +

(9223372036854775808 + andJint(

getByte1 , 255))

8 / 18446744073709551616 *

-18446744073709551616,

9 i * 8 + (2147483648 + i * 8) /

4294967296 * -4294967296

10 )

11 = andJlong( shiftleftJlong(255 , i * 8 +

(2147483648 + i * 8) / 4294967296 *

-4294967296) , x)

12 ),

13 \ forall j; (

14 j <= -1

15 | j >= Z(n)

16 | shiftleftJlong(

17 andJint(getByte2 , 255) +

(9223372036854775808 + andJint(

getByte2 , 255))

18 / 18446744073709551616 *

-18446744073709551616,

19 j * 8 + (2147483648 + j * 8) /

4294967296 * -4294967296

20 )

21 = andJlong( shiftleftJlong(255 , j * 8 +

(2147483648 + j * 8) / 4294967296 *

-4294967296) , y)

22 ) ==>

23 )

24 \ varcond(

25 \ notFreeIn(j, getByte1),

26 \ notFreeIn(i, getByte2),


28 \ notFreeIn(j, x),

29 \ notFreeIn(i, y),

30 \ notFreeIn(j, y),

31 \ notFreeIn(i, n),

32 \ notFreeIn(j, n)

33 )

34 \add( ( ( 0 < Z(n) & Z(n) < 8

35 & -shiftleftJlong(1, 8 * Z(n) - 1) <= x

36 & x <= shiftleftJlong(1, (8 * Z(n))) - 1

37 & -shiftleftJlong(1, 8 * Z(n) - 1) <= y

38 & y <= shiftleftJlong(1, (8 * Z(n))) - 1)

39 | ( Z(n) = 8

40 & inLong (x)

41 & inLong (y)

A.3 Additional bit lemmata 101

42 )

43 )

44 & \ forall i; (i <= -1 | i >= Z(n) | getByte1 = {\ subst

j; i}getByte2)

45 -> x = y

46 ==>

47 )


49 };

102 A Lemmata

Bibliography

[Ahr07] Ahrendt, Wolfgang; Beckert, Bernhard; Hähnle, Reiner; Rümmer,Philipp and Schmitt, Peter H.: Verifying Object-Oriented Programs withKeY: A Tutorial,http://www.key-project.org/case_studies/ (2007) (Cited on page 14)

[Bec07] Beckert, Bernhard; Hähnle, Reiner and Schmitt, Peter H.: Verificationof Object-Oriented Software. The KeY Approach., Springer-Verlag GmbH(2007) (Cited on pages 1, 4, 7, 8, 9, 10, 14, 30, 31, and 61)

[Bur05] Burdy, Lilian; Cheon, Yoonsik; Cok, David; Ernst, Michael D.; Kiniry,Joe; Leavens, Gary T.; Leino, K. Rustan M. and Poll, Erik: An overviewof JML tools and applications. Software Tools for Technology Transfer(2005), vol. 7(3):pp. 212–232 (Cited on page 1)

[IEE06] IEEE 802.15.4 standard: IEEE Standard for Information technology—Telecommunications and information exchange between systems—Local andmetropolitan area networks—Specific requirements Part 15.4: WirelessMedium Access Control (MAC) and Physical Layer (PHY) Specifications forLow-Rate Wireless Personal Area Networks (WPANs), Institute of Electricaland Electronics Engineers (IEEE) (2006) (Cited on pages 17, 18, and 21)

[ISO96] ISO/IEC 4798-1 standard: Information technology—Open SystemsInterconnection—Basic Reference Model: The Basic Model, InternationalOrganization for Standardization (ISO) (1996) (Cited on page 17)

[Lea06] Leavens, Gary T. and Cheon, Yoonsik: Design by Contract with JML,http://www.eecs.ucf.edu/∼leavens/JML/ (2006) (Cited on pages 1, 3, 4, 7,and 8)

[Lea08] Leavens, Gary T.: JML Reference Manual,http://www.eecs.ucf.edu/∼leavens/JML/jmlrefman/jmlrefman.html♯Top(2008) (Cited on pages 1, 4, 7, 8, and 31)

[Mos07] Mostowski, Wojciech: Fully Verified JAVA CARD API Reference Imple-mentation,http://www.cs.ru.nl/∼woj/papers/download/verify2007.pdf (2007) (Citedon page 61)

104 Bibliography

[RFC89] RFC 1122 standard: Requirements for Internet Hosts—CommunicationLayers, Internet Engineering Task Force (IETF) (1989) (Cited on page 17)

[RFC07] RFC 4944 proposed standard: Transmission of IPv6 Packets over IEEE802.15.4 Networks, Internet Engineering Task Force (IETF) (2007) (Citedon pages 17 and 18)

[Sch07] Schmitt, Peter H. and Tonin, Isabel: Verifying the Mondex Case Study,http://i12www.ira.uka.de/∼pschmitt/publications/SEFM07.pdf (2007)(Cited on page 61)

[Sun08a] Sun Microsystems: Connected Limited Device Configuration (CLDC);JSR 30, JSR 139, http://java.sun.com/products/cldc/ (2008) (Cited onpage 2)

[Sun08b] Sun Microsystems: Project Sun SPOT, http://www.sunspotworld.com/(2008) (Cited on page 2)

[Sun08c] Sun Microsystems: Project Sun SPOT » Documentation » GeneralFAQ, http://www.sunspotworld.com/docs/general-faq.php (2008) (Cited onpage 1)

[Sun08d] Sun Microsystems: The Squawk Project,http://research.sun.com/projects/squawk/ (2008) (Cited on page 2)

[Uni08] University of Karlsruhe; University of Koblenz and ChalmersUniversity of Technology: The KeY Project,http://i12www.ira.uka.de/∼key/ (2008) (Cited on page 10)

List of Figures

1.1 The assembly of a Sun SPOT . . . . . . . . . . . . . . . . . . . . . . . 2

2.1 The user interface of KeY . . . . . . . . . . . . . . . . . . . . . . . . . 13

3.1 Frame structures and their relations . . . . . . . . . . . . . . . . . . . 183.2 Mesh header structure . . . . . . . . . . . . . . . . . . . . . . . . . . . 193.3 Broadcast header structure . . . . . . . . . . . . . . . . . . . . . . . . 193.4 Fragmentation header structure . . . . . . . . . . . . . . . . . . . . . . 193.5 Protocol header structure . . . . . . . . . . . . . . . . . . . . . . . . . 193.6 Sun SPOT’s network library architecture and related architectures . . 203.7 Class diagram of the classes involved into the verification process . . . 223.8 The class LowPan . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 243.9 The classes RadioPacket and LowPanPacket . . . . . . . . . . . . . . 253.10 The classes LowPanHeader and Utils . . . . . . . . . . . . . . . . . . 26

4.1 Visualization ensures-clause . . . . . . . . . . . . . . . . . . . . . . . . 424.2 Rule application strategies readLittleEndNumber(·) start . . . . . . . 434.3 Rule application strategies for general bit lemmata . . . . . . . . . . . 444.4 Rule application strategies for resolution bit lemmata . . . . . . . . . 454.5 readLittleEndNumber(·) goal 1 . . . . . . . . . . . . . . . . . . . . . 464.6 readLittleEndNumber(·) goal 2 . . . . . . . . . . . . . . . . . . . . . 474.7 readLittleEndNumber(·) goal 3 . . . . . . . . . . . . . . . . . . . . . 484.8 readLittleEndNumber(·) goal 4 . . . . . . . . . . . . . . . . . . . . . 494.9 Proof regarding getSourceAddress() before applying the update_cut 53

106 List of Figures

List of Tables

3.1 Number of methods and attributes of the classes involved into the ver-ification process . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

4.1 Distribution of the method sizes . . . . . . . . . . . . . . . . . . . . . 29

108 List of Tables

Listings

2.1 Simple example of a method contract in JML . . . . . . . . . . . . . . 52.2 Simple example of a method contract which specifies an exceptional-

_behavior . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52.3 A more complex example for a JML specification of a method . . . . . 62.4 Example of an JML specification with the keyword \old(·) . . . . . . 72.5 Example of a taclet . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 154.1 Contract application example 1 . . . . . . . . . . . . . . . . . . . . . . 334.2 Contract application example 2 . . . . . . . . . . . . . . . . . . . . . . 354.3 Method initAsBroadcast() . . . . . . . . . . . . . . . . . . . . . . . 364.4 Expansion of andJlong . . . . . . . . . . . . . . . . . . . . . . . . . . . 384.5 The method readLittleEndNumber(·) . . . . . . . . . . . . . . . . . . 414.6 Example for moving a pre-condition . . . . . . . . . . . . . . . . . . . 51A.1 Lemma andZeroJlong. . . . . . . . . . . . . . . . . . . . . . . . . . . . 63A.2 Lemma andZeroJint. . . . . . . . . . . . . . . . . . . . . . . . . . . . 64A.3 Lemma swapNumberToTheRightAndJlong. . . . . . . . . . . . . . . . . 64A.4 Lemma swapNumberToTheRightAndJint. . . . . . . . . . . . . . . . . 64A.5 Lemma swapNumberToTheRightOrJlong. . . . . . . . . . . . . . . . . 65A.6 Lemma swapNumberToTheRightOrJint. . . . . . . . . . . . . . . . . . 65A.7 Lemma swapNumberToInnerAndJlong. . . . . . . . . . . . . . . . . . . 66A.8 Lemma swapNumberToInnerAndJint. . . . . . . . . . . . . . . . . . . 66A.9 Lemma swapNumberToInnerOrJlong. . . . . . . . . . . . . . . . . . . 66A.10 Lemma swapNumberToInnerOrJint. . . . . . . . . . . . . . . . . . . . 66A.11 Lemma shiftleftAndJlong. . . . . . . . . . . . . . . . . . . . . . . . 67A.12 Lemma shiftleftOrJlong. . . . . . . . . . . . . . . . . . . . . . . . . 67A.13 Lemma shiftleftAndJint. . . . . . . . . . . . . . . . . . . . . . . . . 67A.14 Lemma shiftleftOrJint. . . . . . . . . . . . . . . . . . . . . . . . . . 68A.15 Lemma andOrJlong. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68A.16 Lemma andOrJint. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68A.17 Lemma mergeAndJlong. . . . . . . . . . . . . . . . . . . . . . . . . . . 69A.18 Lemma mergeAndJint. . . . . . . . . . . . . . . . . . . . . . . . . . . . 69A.19 Lemma mergeAndJlongAndJint. . . . . . . . . . . . . . . . . . . . . . 69A.20 Lemma mergeAndJintAndJlong. . . . . . . . . . . . . . . . . . . . . . 70A.21 Lemma mergeOrJlong. . . . . . . . . . . . . . . . . . . . . . . . . . . . 70

110 Listings

A.22 Lemma mergeOrJint. . . . . . . . . . . . . . . . . . . . . . . . . . . . 70A.23 Lemma mergeOrJintOrJlong. . . . . . . . . . . . . . . . . . . . . . . 70A.24 Lemma mergeModuloLongAndJlong. . . . . . . . . . . . . . . . . . . . 71A.25 Lemma mergeModuloIntAndJint. . . . . . . . . . . . . . . . . . . . . 71A.26 Lemma mergeModuloLongAndJint. . . . . . . . . . . . . . . . . . . . . 71A.27 Lemma mergeModuloLongOrJlong. . . . . . . . . . . . . . . . . . . . . 72A.28 Lemma mergeModuloIntOrJint. . . . . . . . . . . . . . . . . . . . . . 72A.29 Lemma mergeModuloLongOrJint. . . . . . . . . . . . . . . . . . . . . 72A.30 Lemma mergeModuloLongShiftleftJlong. . . . . . . . . . . . . . . . 73A.31 Lemma mergeModuloIntShiftleftJint. . . . . . . . . . . . . . . . . 73A.32 Lemma mergeModuloLongShiftleftJint. . . . . . . . . . . . . . . . . 73A.33 Lemma estimateOrJlongN1. . . . . . . . . . . . . . . . . . . . . . . . 74A.34 Lemma estimateOrJintN1. . . . . . . . . . . . . . . . . . . . . . . . . 74A.35 Lemma estimateOrJlong256. . . . . . . . . . . . . . . . . . . . . . . 74A.36 Lemma estimateOrJint256. . . . . . . . . . . . . . . . . . . . . . . . 74A.37 Lemma estimateOrJlong65536. . . . . . . . . . . . . . . . . . . . . . 75A.38 Lemma estimateOrJint65536. . . . . . . . . . . . . . . . . . . . . . . 75A.39 Lemma estimateOrJlong16777216. . . . . . . . . . . . . . . . . . . . 75A.40 Lemma estimateOrJint16777216. . . . . . . . . . . . . . . . . . . . . 75A.41 Lemma estimateOrJlong4294967296. . . . . . . . . . . . . . . . . . . 76A.42 Lemma estimateOrJlong1099511627776. . . . . . . . . . . . . . . . . 76A.43 Lemma estimateOrJlong281474976710656. . . . . . . . . . . . . . . 76A.44 Lemma estimateOrJlong72057594037927936. . . . . . . . . . . . . . 76A.45 Lemma compareShortsPerByte. . . . . . . . . . . . . . . . . . . . . . 77A.46 Lemma compareIntsPerByte. . . . . . . . . . . . . . . . . . . . . . . 77A.47 Lemma compareLongsPerByte. . . . . . . . . . . . . . . . . . . . . . . 78A.48 Lemma translateAndJlong_automatic. . . . . . . . . . . . . . . . . 79A.49 Lemma translateAndJint_automatic. . . . . . . . . . . . . . . . . . 80A.50 Lemma translateOrJlong_automatic. . . . . . . . . . . . . . . . . . 80A.51 Lemma translateOrJint_automatic. . . . . . . . . . . . . . . . . . . 80A.52 Lemma translateAndJlong. . . . . . . . . . . . . . . . . . . . . . . . 80A.53 Lemma translateAndJint. . . . . . . . . . . . . . . . . . . . . . . . . 81A.54 Lemma translateOrJlong. . . . . . . . . . . . . . . . . . . . . . . . . 81A.55 Lemma translateOrJint. . . . . . . . . . . . . . . . . . . . . . . . . . 81A.56 Lemma swapNumberToTheRightAnd. . . . . . . . . . . . . . . . . . . . 82A.57 Lemma swapNumberToTheRightOr. . . . . . . . . . . . . . . . . . . . . 82A.58 Lemma resolveAndBitwise. . . . . . . . . . . . . . . . . . . . . . . . 82A.59 Lemma resolveAndBitwise64. . . . . . . . . . . . . . . . . . . . . . . 83A.60 Lemma resolveAndBitwise32. . . . . . . . . . . . . . . . . . . . . . . 83A.61 Lemma resolveAndBitwise16. . . . . . . . . . . . . . . . . . . . . . . 84A.62 Lemma resolveAndBitwise8. . . . . . . . . . . . . . . . . . . . . . . 84A.63 Lemma resolveAndBitwise4. . . . . . . . . . . . . . . . . . . . . . . 84A.64 Lemma resolveAndBitwise2. . . . . . . . . . . . . . . . . . . . . . . 84A.65 Lemma resolveAndBitwise1. . . . . . . . . . . . . . . . . . . . . . . 85

Listings 111

A.66 Lemma calculateLowerBitAnd. . . . . . . . . . . . . . . . . . . . . . 85A.67 Lemma andZero. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86A.68 Lemma andBitwise3. . . . . . . . . . . . . . . . . . . . . . . . . . . . 86A.69 Lemma andBitwise15. . . . . . . . . . . . . . . . . . . . . . . . . . . . 86A.70 Lemma andBitwise255. . . . . . . . . . . . . . . . . . . . . . . . . . . 86A.71 Lemma andBitwise65535. . . . . . . . . . . . . . . . . . . . . . . . . . 86A.72 Lemma andBitwise4294967295. . . . . . . . . . . . . . . . . . . . . . 87A.73 Lemma andBitwise18446744073709551615. . . . . . . . . . . . . . . 87A.74 Lemma resolveOrBitwise. . . . . . . . . . . . . . . . . . . . . . . . . 87A.75 Lemma resolveOrBitwise64. . . . . . . . . . . . . . . . . . . . . . . 87A.76 Lemma resolveOrBitwise32. . . . . . . . . . . . . . . . . . . . . . . 88A.77 Lemma resolveOrBitwise16. . . . . . . . . . . . . . . . . . . . . . . 88A.78 Lemma resolveOrBitwise8. . . . . . . . . . . . . . . . . . . . . . . . 88A.79 Lemma resolveOrBitwise4. . . . . . . . . . . . . . . . . . . . . . . . 89A.80 Lemma resolveOrBitwise2. . . . . . . . . . . . . . . . . . . . . . . . 89A.81 Lemma resolveOrBitwise1. . . . . . . . . . . . . . . . . . . . . . . . 89A.82 Lemma calculateLowerBitOr. . . . . . . . . . . . . . . . . . . . . . . 90A.83 Lemma orZero. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90A.84 Lemma or2BitWith3. . . . . . . . . . . . . . . . . . . . . . . . . . . . 90A.85 Lemma or4BitWith15. . . . . . . . . . . . . . . . . . . . . . . . . . . . 91A.86 Lemma or8BitWith255. . . . . . . . . . . . . . . . . . . . . . . . . . . 91A.87 Lemma or16BitWith65535. . . . . . . . . . . . . . . . . . . . . . . . . 91A.88 Lemma or32BitWith4294967295. . . . . . . . . . . . . . . . . . . . . 91A.89 Lemma or64BitWith18446744073709551615. . . . . . . . . . . . . . . 91A.90 Lemma orZeroJlong. . . . . . . . . . . . . . . . . . . . . . . . . . . . 92A.91 Lemma orZeroJint. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92A.92 Lemma andJlong7. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92A.93 Lemma andJint7. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93A.94 Lemma andJlong15. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93A.95 Lemma andJint15. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93A.96 Lemma andJlong255. . . . . . . . . . . . . . . . . . . . . . . . . . . . 93A.97 Lemma andJint255. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93A.98 Lemma andJlong65535. . . . . . . . . . . . . . . . . . . . . . . . . . . 94A.99 Lemma andJint65535. . . . . . . . . . . . . . . . . . . . . . . . . . . . 94A.100Lemma andJlong16777215. . . . . . . . . . . . . . . . . . . . . . . . . 94A.101Lemma andJint16777215. . . . . . . . . . . . . . . . . . . . . . . . . . 94A.102Lemma andJlong4294967295. . . . . . . . . . . . . . . . . . . . . . . 94A.103Lemma andJint4294967295. . . . . . . . . . . . . . . . . . . . . . . . 95A.104Lemma andJlong1099511627775. . . . . . . . . . . . . . . . . . . . . 95A.105Lemma andJlong281474976710655. . . . . . . . . . . . . . . . . . . . 95A.106Lemma andJlong72057594037927935. . . . . . . . . . . . . . . . . . . 95A.107Lemma andJlong18446744073709551615. . . . . . . . . . . . . . . . . 95A.108Lemma resolve2ToThePowerOfX. . . . . . . . . . . . . . . . . . . . . 96A.109Lemma resolve2ToThePowerOf0. . . . . . . . . . . . . . . . . . . . . 96

112 Listings

A.110Lemma resolve2ToThePowerOf1. . . . . . . . . . . . . . . . . . . . . 96A.111Lemma resolve2ToThePowerOf2. . . . . . . . . . . . . . . . . . . . . 96A.112Lemma resolve2ToThePowerOf4. . . . . . . . . . . . . . . . . . . . . 97A.113Lemma resolve2ToThePowerOf8. . . . . . . . . . . . . . . . . . . . . 97A.114Lemma resolve2ToThePowerOf16. . . . . . . . . . . . . . . . . . . . . 97A.115Lemma resolve2ToThePowerOf32. . . . . . . . . . . . . . . . . . . . . 97A.116Lemma resolve2ToThePowerOf64. . . . . . . . . . . . . . . . . . . . . 97A.117Lemma forceCalculateLowerBitAnd. . . . . . . . . . . . . . . . . . . 98A.118Lemma forceCalculateLowerBitOr. . . . . . . . . . . . . . . . . . . 98A.119Lemma byteEquivalenceHighLevel. . . . . . . . . . . . . . . . . . . 98A.120Lemma byteEquivalenceLowLevel. . . . . . . . . . . . . . . . . . . . 99

Index

A

Application Layer . . . . . . . . . . . . . . . . . . . . . . . 17Assumed-Selection . . . . . . . . . . . . . . . 32, 34, 35

C

Connected Limited Device Configuration(CLDC). . . . . . . . . . . . . . . . . .2, 27, 28

Contract assumption . . . . . . . . . . . . . 32, 34, 36

D

Data Link Layer . . . . . . . . . . . . . . . . . . . . . . . . .17design by contract (DBC) . . . . . . . . . . . . . . . . 4

E

Ensured-Selection . . . . . . . . . . . . . . . . 32, 34–36

I

Invariant . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4, 7, 9

J

Java . . . . . . . . . . . 1–4, 7, 10, 13, 28, 29, 58, 61Java Dynamic Logic (JavaDL)10–13, 57, 60,

61Java Modeling Language (JML) . . . . . 1, 3–9,

11–13, 28, 30, 32, 33, 51, 52, 54, 57,59, 61

K

KeY . . . . 1–3, 8–14, 27–37, 39, 43, 50–52, 54,57–61

L

Low-Rate Wireless Personal Area Network(LoWPAN). . . . . . . . . . . . . . . . . . . . .17

LoWPAN Adaption Layer 17, 18, 21–23, 28,61

LoWPAN encapsulation frame . . . 18, 21, 23

M

MAC data service . . . . . . . . . . . . . . . . 17, 18, 21MAC Sublayer . . . . . . . . . . . . . . . . . . . 17, 21, 23Method contract . . . . . . . . . . . . . . . . . . . . .4, 5, 9MPD unit . . . . . . . . . . . . . . . . . . . . 17, 18, 21, 23

N

Network Access Layer . . . . . . . . . . . . . . . . . . . 17Network Layer. . . . . . . . . . . . . . . . . . . . . . . . . . .17

O

Observed state correctness . . . . . 9, 27, 29–32Open Systems Interconnection (OSI) Model

17, 18

P

PHY data service . . . . . . . . . . . . . . . . . . . . . . . .17Physical Layer . . . . . . . . . . . . . . . . . . . . . . . . . . .17Post-condition. . . . . . . . . . . . . . . .4, 7, 9, 50, 52Pre-condition . . . . . . . . . . . . . . . 4, 9, 50, 51, 59Program state . . . . . . . . . . . . . . . . . . . . . . . . . . . 30Proof assumption . . . . . . . . . . . . . . . . . . . . 32–36

S

Squawk . . . . . . . . . . . . . . . . . . . . . . . . . . . 2, 28, 61Sun SPOT. . . . . . . . . . .1, 2, 17, 20, 27, 28, 61

T

TCP/ IP Model . . . . . . . . . . . . . . . . . . . . . . 17, 18Transport Layer . . . . . . . . . . . . . . . . . . . . . . . . . 17

Diploma Thesis - KITlfm.iti.kit.edu/download/DAScheben.pdf · Diploma Thesis Veriﬁcation of Sun...

Documents

Transcript of Diploma Thesis - KITlfm.iti.kit.edu/download/DAScheben.pdf · Diploma Thesis Veriﬁcation of Sun...