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

From: Steve Tockey < >
Date: Sat, 27 Feb 2016 08:47:47 +0000

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

-----Original Message-----
Date: Friday, February 26, 2016 11:15 PM To: "systemsafety_at_xxxxxx <systemsafety_at_xxxxxx 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



The System Safety Mailing List
systemsafety_at_xxxxxx Received on Sat Feb 27 2016 - 09:48:00 CET

This archive was generated by hypermail 2.3.0 : Tue Jun 04 2019 - 21:17:07 CEST