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

[David MENTRE]

Dear Prof. Ladkin,

Le 26/02/2016 12:54, Peter Bernard Ladkin a écrit :
> I agree with much of what you say, but I am not sure about SDL.

I'm not sure neither. But apparently some work has been done. I won't 
say anything about its coverage.

Nonetheless, you'll find in ITU Z.100 :
"""
Appendix I
Status of ITU-T Z.100, related documents and Recommendations
[...]
– Annex F [Formal specification of SDL] to Recommendation ITU-T Z.100 
(approved by ITU-T Study Group 10 on 24
November 2000). This document was for SDL-2000 and consistency with 
SDL-2010 is
subject to further study. Not part of the ITU-T Z.100 series for SDL-2010.
Tools for the formal semantics reference model of SDL-2000 (ITU-T 
Specification and
Description Language) are found at http://sourceforge.net/projects/sdlc 
(the files themselves
are accessible either through CVS, or through the CVS web front end, at
http://sdlc.cvs.sourceforge.net/viewvc/sdlc/).
"""

> It was not true that SDL had an adequate formal semantics in the sense in
> which computer scientists use that term; neither was it true that SDL was unambiguous.

Honestly, I don't know. I would conjecture that it is better than 
UML/SysML. Maybe not at the level of SCADE.


> Lustre and Esterel certainly. I don't know about Signal. There is the further question of whether
> the SCADE tools respect the semantics of Lustre and Esterel (and Signal). That was always the
> intent, and my colleagues at Esterel do claim it, but I am not sure to what extent it has ever been
> independently assessed (apart from what TüV Süd says).

 From my understanding SCADE has its own semantics, but at least it is 
formally defined (in the mathematical sense of it).

>> It is both a
>> graphical and textual language. It is an international standard (ITU Z.100 to Z.109,
>> http://www.itu.int/rec/T-REC-z) and is apparently freely available.
>
> The ITU charges for its documents.

Not always. For example you can freely download the PDF of Z.100:
   http://www.itu.int/rec/T-REC-Z.100-201112-I/en

And also annexes F1 to F3, were formal semantics of SDL is defined.

>> >For me, a graphical representation is unambiguous if, for each graphical construction or combination
>> >of constructions, its semantics (i.e. its meaning) is described, in an exhaustive way.
> 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.

Well spotted! I won't have time to try to propose a more complete 
definition but I fully agree with you.


>> >Because you can read the formal description and make tools from it.
> People do that with C!

Yes. Once again, my definition was too loose.

Best regards,
david