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

From: Derek M Jones < >
Date: Fri, 26 Feb 2016 16:36:51 +0000


>>> >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
The System Safety Mailing List
Received on Fri Feb 26 2016 - 17:37:21 CET

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