Re: [SystemSafety] Logic

From: Peter Bernard Ladkin < >
Date: Fri, 21 Feb 2014 09:46:49 +0100

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

The System Safety Mailing List
systemsafety_at_xxxxxx Received on Fri Feb 21 2014 - 09:47:01 CET

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