[SystemSafety] Logic

[Peter Bernard Ladkin]

The bit I take away from Steve's engaging tale (thank you, Steve!) is that

1. A lot of attention was paid to the requirements and general design engineering before code was
written. And that seems to have been where most (in terms of effort) of the difficulties and
potential slip-ups were resolved.

2. The specification languages used were formal (class diagrams, state charts) and the semantics was
unambiguous. That is what I suggested needed to be learnt in my Logic White Paper.

I would call point 2 use of a formal method. Steve suggests it's not "in the sense ..... hotly
debated here." If not, how about a suggestion of a term for "use of formal description language with
an unambiguous semantics" that I and others can use?

On 2014-02-21 01:20 , Steve Tockey wrote:
>> I should add that what was done on these projects was not strictly "formal
>> methods" in the sense that's being hotly debated here. We didn't use Z,
>> VDM, or any of those formal languages. We didn't use theorem provers
>> either. We used UML (and pre-UML because of project timing) class diagrams
>> and state charts mostly, but we had a carefully defined and enforced (via
>> the model inspections) single interpretation of that modeling language.

The bit I take away from Les's tale (thank you, also, Les!) is

1. Same as above

2. Use of cooperating FSMs as a paradigm.

On 2014-02-21 02:52 , Les Chambers wrote:
> .... All
>> projects started with something we called "English language", a clear
>> statement of the operating discipline structured such that it could be
>> easily transformed into a design models - something similar to what is now
>> called Requirements State Machine Language. 

Could you call it a version of Controlled English? Was it ambiguous or was it unambiguous?

>> .......
>> .....You could write any program you liked as long
>> as it implemented the plant control system as a set of cooperating finite
>> state engines. 

A major engineering company which produces some of the most sophisticated and expensive engineering
artefacts around uses either Lustre or Statecharts for most of its SW projects and builds very
successful, comparatively highly reliable SW. Both Lustre and Statecharts are based on the paradigm
of communicating FSMs. With an underlying formal language expressing states and transitions. (I
already knew some of this but thank you, anonymous, for expanding on it!)

PBL

Prof. Peter Bernard Ladkin, Faculty of Technology, University of Bielefeld, 33594 Bielefeld, Germany
Tel+msg +49 (0)521 880 7319  www.rvs.uni-bielefeld.de