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

From: David MENTRE < >
Date: Fri, 26 Feb 2016 17:09:30 +0100

Dear Prof. Ladkin,

Le 26/02/2016 12:34, Peter Bernard Ladkin a écrit :
> On 2016-02-26 10:33 , David MENTRE wrote:
>> >Le 26/02/2016 09:43, Peter Bernard Ladkin a écrit :
>>> >>Another reason is the prevelance of MathLab/Simulink in this domain. Simulink is now an executable
>>> >>specification language. Since there is one supplier, it is de facto unambiguous (there is just one
>>> >>simulator, so the single meaning of a Simulink spec is precisely what that simulator does with the
>>> >>spec).
>> >
>> >Some people have even formally defined the semantics of Simulink or a subset of it:
> I think what this says is that some people have interpreted in a formal way what they think Simulink
> diagrams should ideally mean. Whether they do mean that or not is another question.

No, at least for some of those works, they have compared their formalisation to actual execution with Matlab/Simulink.

For example:
Presented at Fundamental Approaches to Software Engineering (FASE) Barcelona, Spain, March 2004. Springer Verlag LNCS 2984, pp. 229–243. 
An Operational Semantics for Stateflow
Grégoire Hamon and John Rushby


However, our SOS semantics is directly executable and can easily be used to define a Stateflow interpretor whose outputs can be compared to those 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.

I agree that such comparisons are more tests of the semantics than a real proof of adequacy.

> 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 those semantics had been
> independently assessed as adequate, (b) MathWorks had accepted it, and (c) MathWorks had
> demonstrated that their simulator (the execution engine for Simulink) conformed to the semantics.

Or on the reverse, one could probably demonstrate through enough testing that one of above semantics matches a subset of Matlab/Simulink with the actual tool. Such work would be very close to work done on testing compilers for aeronautics certification for example. However I'm not sure anybody would interested in investing enough time and money to do it. :-)

Sincerely yours,
D. Mentré

The System Safety Mailing List
systemsafety_at_xxxxxx Received on Fri Feb 26 2016 - 17:09:38 CET

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