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

[Derek M Jones]

David,

>>> >Some people have even formally defined the semantics of Simulink or
>>> a subset of it:

Yes a subset.
 From the abstract of: An Operational Semantics for Stateflow
"Stateflow has many tricky features but our operational treatment yields
a surprisingly simple semantics for the subset that is generally
recommended for industrial applications."

> from the Matlab simulator. We have done this and systematically examined
> many examples; for all these examples, the traces obtained by the two
> tools were the same.

How many is "many" and to what extent did they exercise all the features
of the subset handled?

>> It's laudable, but it's a long way from what "formally defined the
>> semantics of Simulink" would mean
>> to practicing engineers. That would further entail that (a) one of

Yes, what use is a formal specification of a language?

In theory it might be used to find inconsistencies in how
the language interprets constructs.  There have been various
projects intending to do this sort of thing, but the ones I am
aware of have had their hands full just completing the formal
specification.  Does anybody know of success stories here?

Are there other uses?

There is a class of people who are mightily impressed by
the existence of a formal specification for whatever.  So there
is a marketing use.

-- 
Derek M. Jones           Software analysis
tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com