[SystemSafety] Modelling and coding guidelines: "Unambiguous Graphical Representation"

[Peter Bernard Ladkin]

On 2016-02-27 06:41 , Steve Tockey wrote:
> To me it means "single interpretation". The model has exactly one meaning. Regardless of how the
> model was turned into code (either by a human or by a tool) the code behaves identically for all
> correct implementations.

I take "unambiguous" to mean "has a single meaning" also. Indeed, like most English speakers I take
the two phrases as synonymous. But that just pushes the difficulty further. I am not sure people
have taken on board what I suggested yesterday:

> Let X be a syntactic object specifying behavior. Let A, B and C be pairwise incompatible statements
> of a semantics.
> 
> "X means A, or B, or C" is an exhaustive description of a semantics of X. It is patently not
> unambiguous. Indeed, X can have any one of three mutually incompatible meanings.
> 
> You can, of course, say that "A or B or C" is unambiguous, and in logic it is. But in terms of
> understanding what X does, it is not.
> 
> So, as we see, the term "unambiguous" is ambiguous.

Maybe it was too abstractly expressed. Let me make the point more concretely.

A = "the executing program X returns a "0" and terminates normally"
B = "the executing program X returns "100" and terminates normally"
C = "the executing program X terminates abnormally"

Assumption (*): Let us agree that A and B and C are all "unambiguous meanings". (There is a caveat
below.)

I can assign X an unambiguous operational meaning: Meaning(X) = (A or B or C). This meaning is
calculated by applying the truth table for "or" to the meanings of A, B, C. Since the truth table is
functional on its components (namely, the meanings of A, B and C), and a function only has one value
for given values of its arguments, the meaning of X is unambiguous. QED.

However, it does not follow that X behaves identically for all correct = (semantically conformant)
implementations. Indeed, any of (at least) three incompatible behaviors is correct.

So the criterion that the code behaves identically in all executions is stronger than the literal
English meaning of "unambiguous" as having one meaning. So Steve gives two meanings to
"unambiguous". :-)

Now, we can have a go at what it means for the "code [to] behave identically". Exercise for the
reader, but here's a hint: it's not as easy as you might think it looks.

For example: What if there is a hidden register in the CPU that is incremented when code X is run,
and every so often raises an interrupt on its value? Code X doesn't behave the same: it used to do
"A" but now terminates abnormally on the interrupt (i.e., C). But, you might say, it's not program X
that generates the behavior, it's some other stuff that doesn't belong to X. OK, so now you've
allowed the possibility that program X running on a sequential CPU can exhibit two different real
I/O behaviors (A, or C) while only "really" exhibiting one (namely A), because something "hidden"
manifests itself. So how do you tell which I/O behavior "belongs" to the program X and which is
"extraneous"? You can't do it just by looking, obviously.

And so on.

Concerning the ambiguity of certain constructs in Statecharts, Steve refers to

> M. von der Beek. A Comparision of Statechart Variants. In W.-P. de Roever
> H. Langmaack and J. Vytopil, editors, Formal Techniques in Real-Time and
> Fault-Tolerant Systems , number 863 in Lecture Notes in Computer Science,
> pages 128­148. Springer Verlag, September 1994.
> 
> The article talks about something like 17 different dimensions of
> ambiguity in state charts.

Willem de Roever is the source of my observations on ambiguous constructs in Statecharts. To put it
in technical terminology, the semantics of Statecharts were not compositional (although useful
subsets are), but see below.

(Suppose L is a language whose syntax is defined inductively. A compositional semantics for L is a
semantics in which the meaning of a whole statement is functional on the meaning of its parts
(substatements). A decent compositional semantics is one where you know the functions involved. A
practical compositional semantics is one where not only do you know the functions, but they are
simple.....)

The author's name is spelt wrongly above, I think. It's Michael van der Beeck with a "c". There is
an ICASE report from 2000 by Gerald Lüttgen (now at Bamberg), van der Beeck, and Rance Cleaveland on
how to get a compositional semantics for Statecharts, followed by a paper in the ACM Sigsoft
International Symposium on the Foundations of Software Engineering (FSE):

>  [Statechart-like constructs are] used in many popular software design notations. A large part of the appeal of 
> Statecharts derives from its [sic] basis in state machines with their intuitive operational interpretation. The 
> traditional semantics of Statecharts howeversuffers from a serious defect: it is not compositional, meaning that 
> the behavior of system descriptions cannot be inferred from the behavior of their subsystems. Compositionality is a 
> prerequisite for exploiting the modular structure of Statecharts for simulation, verification, and code generation .... 
> This paper suggests a new compositional approach to formalizing Statecharts semantics ........

The ICASE report is at http://www4.informatik.tu-muenchen.de/publ/papers/LueBeeCle00.pdf and the FSE
paper at http://www.swt-bamberg.de/luettgen/publications/pdf/FSE2000.pdf

I tried to find out where Michael van der Beeck now is. He was at TUM when the paper was published.
I found a contract annex still on line at the Uni Paderborn for the SegraVis project, where he was
listed as affiliated with BMW as an "external". That document dates from sometime before 2003. So I
would imagine he went from TUM to BMW.  Willem, Gerald or Rance are probably the people to ask about
further developments with the semantics of Statecharts.

PBL

Prof. Peter Bernard Ladkin, Faculty of Technology, University of Bielefeld, 33594 Bielefeld, Germany
Je suis Charlie
Tel+msg +49 (0)521 880 7319  www.rvs.uni-bielefeld.de





-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 455 bytes
Desc: OpenPGP digital signature
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20160227/20a16ef5/attachment.pgp>