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

[Steve Tockey]

"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."

I would propose that there's a difference between ambiguity and
determinism. Your model is unambiguous in specification--it does have one
and only one meaning. The issue is that it appears to be non-deterministic
in execution.

An ambiguous model can be interpreted to mean different things. If that
model is deterministically ambiguous then any one of those interpretations
will always behave only one way.

An unambiguous model can be non-deterministic (as is your example). It has
only one meaning, but will possibly yield different results under any
given execution. There are cases where unambiguous, non-deterministic
models can be useful: Monte Carlo simulation, for example.

In safety critical systems, we should strive for specifications that are
both unambiguous and deterministic, so that relevant safety properties can
be examined. As well, if an unambiguous and deterministic specification is
faithfully implemented then the code will always behave one and only one
way--the way it was specified--in any execution.


-- steve



-----Original Message-----
From: systemsafety <systemsafety-bounces at lists.techfak.uni-bielefeld.de>
on behalf of Peter Bernard Ladkin <ladkin at rvs.uni-bielefeld.de>
Date: Friday, February 26, 2016 11:15 PM
To: "systemsafety at lists.techfak.uni-bielefeld.de"
<systemsafety at lists.techfak.uni-bielefeld.de>
Subject: Re: [SystemSafety] Modelling and coding guidelines: "Unambiguous
Graphical Representation"

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