Live Sequence Diagrams

Question 1

What is the definition of well-formedness?

Answer 1

For each location l, if l is the location of a condition or a local invariant, then there is a location l’ simultaneous to l, which is the location of an instance head or a message

Question 2

What are all the parts of the abstract syntax?

Answer 2

1. set of locations with partial order and simultaneity
2. the set of instance lines (a partition of the set of locations)
3. set of messages
4. set of conditions
5. set of local invariants
6. assignment of temperature to each location/element

Question 3

Are cyclic LSDs allowed?

Answer 3

No, they do not have an abstract syntax

Question 4

Relationship between abstract and concrete syntax?

Answer 4

multiple concrete syntaxes for one abstract syntax

Question 5

What is the definition of a cut?

Answer 5

A nonempty set of locations which is:

1. downward-closed (if b is in the cut and a<b></b>

Question 6

What is the temperature of a cut?

Answer 6

C is hot if and only if at least one of its maximal elements (latest in cut) is hot

Question 7

What are always the first and last cuts?

Answer 7

first cut = all instance heads

last cut = entire diagram (all locations)

Question 8

What is a fired set F of a cut C?

Answer 8

“difference between one cut and the following cut” denoted by squiggly line between cuts

1. C and F are disjoint
2. union of C and F is a cut
3. all locations of F are “direct successors” of locations in C (no location between location in C and location in F)
4. locations in F that are on the same instance line are pairwise unordered
5. for each asynchronous message reception in F, the corresponding sending is already in C

Question 9

What are the 3 syntaxes of LSDs?

Answer 9

abstract, concrete (diagram), semantics (automat)

Question 10

What is the TBA construction principle?

Answer 10

The TBA B(L) of LSC L is (C, Q, q_ini, –>, Q_F) where:
Q = set of cuts,
q_ini = instance heads cut,
C_B = union of C and E!?,
–> consists of loops, progress conditions (fired set), and legal exits (cold cond or local invariant),
F is the set of cold cuts

Question 11

List the components of a full LSC

Answer 11

pre-chart (possibly empty), main chart (non-empty), activation condition (condition/location invariant), strictness flag (strict or permissive), activation mode (initial or invariant), chart mode (existential (cold) or universal (hot)), strictness flag

Question 12

When is a “universal” LSC satisfied by software? (hot)

Answer 12

A universal LSC is satisfied by a software

S if and only if all words induced by the computation paths of S are accepted by the LSC’s TBA

Question 13

When is a “existential” LSC satisfied by software? (cold)

Answer 13

An existential LSC is satisfied by a software
S if and only if there is a word induced by a computation path of S which is accepted by the LSC’s TBA. Prove by demonstrating the computation path.

Question 14

What is the purpose of precharts?

Answer 14

allow us to specify anti-scenarios (“this must not happen”) and activation interactions

Question 15

invariant v. initial?

Answer 15

invariant: software can satisfy the LSC starting at any state
initial: software must satisfy the LSC starting at the first state

Question 16

relationship between word and computation path of software?

Answer 16

word = sequence of (state disjunction next action)

Question 17

When is software compatible with LSC?

Answer 17

states are valuations of the conditions, events are of the form E?, E!