Lösungsvorschlag Software Architecture And Engineering FS14

Aus VISki
Wechseln zu: Navigation, Suche

Achtung, dies ist nur ein von Studenten erstellter Lösungsvorschlag, keine offizielle Lösung.

Task 1 - Modeling

A. Modeling using UML and Alloy

(a)

  1. R1, R2 & R3
  2. Uml diagram SAE Ex SS2014.png

(b)

sig ID{}
sig Client{}
sig Account{
 id: one ID,
 owner: one Client
}
sig Checking, Savings, CreditCard extends Account{}

fact atMostFiveAccounts {
 //gibt sicher bessere Lösungen
 all c:Client | all disj a1,a2,a3,a4,a5,a6 :Account | a1.owner = c && a2.owner = c && a3.owner = c && a4.owner = c && a5.owner = c implies a6.owner != c
 // bessere Lösung:
 all c:Client | #{a:Account | a.owner = c} <= 5
 // noch kürzer:
 all c: Client| # owner.c <= 5
 // oder äquivalent:
 all c: Client| #c.~owner <= 5
}

fact uniqueIDs {
 all disj a1,a2: Account | a1.id != a2.id
 // kürzer:
 all i: ID | one id.i
}

fact noCreditCardIfNoChecking {
 all cc: CreditCard | some c:Checking | cc.owner = c.owner
 // different approach (not better, just different, may be useful to illustrate some operators)
 all c: Client | no Checking <: (owner.c) => no CreditCard <: (owner.c)
 // yet another approach
 all a1: CreditCard | some a2: Checking | a2.owner = a1.owner
}

(c)

sig Account {
 balance: Int
}

pred init[s: Account] {
 s.balance = 0
}

pred deposit[s, s': Account, amount: Int] {
 (amount >= 0) =>
  s'.balance = plus[s.balance, amount]
 else
  s'.balance = s.balance
}

pred withdraw[s, s': Account, amount: Int] {
 (amount >= 0 && s.balance >= amount) =>
  s'.balance = minus[s.balance, amount]
 else
  s'.balance = s.balance
}

pred inv[s: Account] {
 s.balance >= 0
}

assert neverNegative {
 // (1)
 all s:Account | init[s] => inv[s]
 // (2)
 all s1, s2:Account, a:int | (inv[s1] and deposit[s1,s2,a]) => inv[s2]
 all s1, s2:Account, a:int | (inv[s1] and withdraw[s1,s2,a]) => inv[s2]
}
// alternatively:
assert neverNegative {
 all s: Account | init[s] => inv[s]
 all s, s': Account, a: int | inv[s] => (deposit[s, s', a] or withdraw[s,s',a]) => inv[s']
}

B. Alloy Semantics

(a)

(b)

(1): Es hält, da next für beide Nodes weder die leere Menge sein darf, noch sich selbst beinhalten, kann sie zwingendermassen nur die Menge mit nur der anderen Node drin sein. Somit kommt man mit 2 mal next immer wieder zurück auf sich selbst.

(2): Hier hält sie nicht mehr:
Node = {n0,n1,n2}
next = {(n0,n1),(n1,n0),(n2,n0)}
n2.next.next = n0.next = n1 != n2

Task 2 - Testing

A. control flow graph

                                    +---------+
                                    | b#start |
                                    +---------+
                                         |
                                         |
                                         ↓
                       +-----+----------------------------+
                       | b#0 | int d = days; int y = 1980 |
                       +-----+----------------------------+
                                         |
                                         |
                                         ↓
                                +-----+--------------+           false
  + ---------------------------→| c#0 | c0 = 365 < d |----------------------------------------+
  |                             +-----+--------------+                                        |
  |                               |            ↑   ↑                                          |
  |                          true |            |   |                                          |
  |                               ↓            |   +----------+                               ↓
  |         +-----+--------------------+       |              |        +-----+-----------------------------------------------+
  |         | c#1 | c1 = isLeapYear(y) |       |              |        | b#4 | System.out.printf("year: %d, day: %d", y, d); |
  |         +-----+--------------------+       |              |        +-----+-----------------------------------------------+
  |             |                     |        | false        |                               |
  |       false |                     | true   |              |                               |
  |             ↓                     ↓        |              |                               ↓
+-----+-------------------------+  +-----+--------------+     |                           +-------+
| b#2 | d = d - 365; y = y + 1; |  | c#2 | c2 = 366 < d |     |                           | b#end |
+-----+-------------------------+  +-----+--------------+     |                           +-------+
                                              |               |
                                              | true          |
                                              ↓               |  
                                +-----+-------------------------+
                                | b#3 | d = d - 366; y = y + 1; |
                                +-----+-------------------------+

B. Coverage

(a) Block coverage: 1 = 100%

(b) Branch coverage: 5/6, da der false-Branch von c#2 nie genommen wird.

C. smallest additional test input

Wie in B. berechnet, reicht der Test-Input 732 nicht um 100% Branch coverage zu erreichen. Wenn wir noch 366 dazu nehmen, reicht dies aber bereits, da 366 > 365 ist c#0 wahr, da 1980 % 4 = 0 und 1980 % 100 != 0, ist c#1 ebenfalls wahr, und da 366 nicht < 366 ist c#2 falsch und somit haben wir den letzten Branch auch noch genommen.

D. Single Test with 100% Coverage

Nein, es gibt keinen einzelnen Input, der 100% Block Coverage & Branch Coverige erreichen kann. Denn um 100% Branch Coverage zu erreichen, müssen wir auch den false-Branch von c#2 nehmen. Um diesen zu nehmen brauchen wir irgendwann im Programmverlauf d = 366 und y = Schaltjahr. Wenn wir diesen Status aber haben, sind wir in einer Endlosschleife gefangen, da d immer grösser 365 ist, also c#0 immer wahr, y immer ein Schaltjahr ist, also c#1 ebenfalls immer wahr und d nie grösser als 366 ist ist c#2 immer falsch. Wenn wir also 100% Branch Coverage anstreben, können wir b#4 nie erreichen und 100% Block Coverage ist ausgeschlossen.

E. Block Coverage -> Branch Coverage

Nein, wie in Task B zu sehen.

static void convert(int days) {
 int d = days; int y = 1980;
 while (365 < d) {
  if (isLeapYear(y)) {
   if (366 < d) {
    d = d -366; y = y + 1;
   }
   // Beginn neuer Teil
   else {
    skip;
   }
   // Ende neuer Teil
  } else {
   d = d -365; y = y + 1;
  }
 }
 System.out.printf("year: %d, day: %d", y, d);
}

F. terminating

convert terminiert für alle Inputs bis auf . von 1 bis 10'000 sind dies: 366, 1827, 3288, 4749, 6210, 7671 und 9132. Also 7 von 10'000 Zahlen, somit liegt die Wahrscheinlichkeit, dass convert nicht terminiert bei

Task 3 - Static analysis

A. complete lattice

P und Q sind complete lattices.

B. monotone

f ist nicht monoton, da nicht gilt.

g ist monoton.

C. abstract domain

when

Task 4 - Interval analysis

A.

Work in progress.png

Diese Aufgabe wurde noch von niemandem gelöst und wartet noch immer auf einen Musterlöser.
Hast du dieses Fach bereits besucht? Hilf mit, die Qualität dieser Seite zu verbessern, indem du eine plausible Lösung für diese Frage notierst!

B.

C.

Dass so ein Pfad existiert, bedeutet, dass die Funktion über-approximiert wird.

D.

i = 0;
while (i < 16)
{ skip;
 i = i + 1;
}

Mit der Interval-Analysis erweitern wir nach 4 Schritten, so dass wir am Ende erhalten, während wir mit der Domain erhalten, da wir nie erweitern müssen, da wir beim zweiten Schritt schon bei angelangen.

Task 5 - Pointer Analysis and Symbolic Execution

A. flow-insensitive Pointer Analysis

, , , , , , ,

B. flow-sensitive Pointer Analysis

, , , , , , ,

C. Symbolic Execution

D. pct decidable

The path constraint is important because it tells us under what conditions we can reach a certain program point. If this is not decidable, we do not gain anything out of the analysis because we don't know if and how to reach a certain program point.

E. simplify pct

  • Use rules of boolean algebra (e.g. can be simplified to )
  • Use rules of integer arithmetics (e.g. we can simplify that to )
  • Concolic execution can be used to work around unsolvable path constraints through replacing variables with values from a concrete execution.
  • maybe more ;-)