[SystemSafety] The Fosse of Babel

[Grazebrook, Alvery AN]

a)      I agree with your basic position – about capturing information at the right level of abstraction, and refining it in the same language framework down to implementation.

b)      I don’t agree that no-one is doing anything about it. What about SCADE? What about Event-B?
Of course, more could be done.

Cheers,
                Alvery
** these are my own opinions, not necessarily those of my employer.

From: systemsafety [mailto:systemsafety-bounces at lists.techfak.uni-bielefeld.de] On Behalf Of Olwen Morgan
Sent: 21 September 2018 3:25 PM
To: systemsafety at lists.techfak.uni-bielefeld.de
Subject: [SystemSafety] The Fosse of Babel



" ...  let us go down, and there confound their language, that they may not understand one another's speech. So the Lord scattered them abroad from thence upon the face of all the earth ..."

Genesis 11:7-8



(No, by quoting part of the Tower of Babel story I've not suddenly gone all god-bothering - I'm more of a Buddhist than anything else). But this serves to introduce an idea:



Ask around and I expect you'd find a reasonable consensus that mathematics is the hardest thing in the sciences and translation is the hardest thing in the humanities. (As an occasional translator, FR-EN and DE-EN, I can certainly vouch for this as regards translation.)



Now, by the standards of hard mathematics, the kind of mathematics that you need to do software engineering rigorously isn't particularly hard. On the other hand something that is done in every software process I've seen is translation. We start with requirements in natural language, we do design in another formalism, programming in another and testing using yet further formalisms. Much of the use of mathematics in software engineering is to provide a lingua-franca that allows us to reason about whether a description of something in one kind of formalism is actually consistent with its description in a different formalism.



This makes pertinent the question of WHY the software engineering process is one of successive translations between different formalisms. Are we not asking for trouble if we have to use the most difficult thing in the sciences to keep us afloat because we're doing the most difficult thing in the humanities?



I posit that, if we ever get a firm grip on software quality, it will be because we have developed what I call, "end-to-end" languages - call them EELs for short. An EEL is a language into which we translate natural language requirements such that thereafter, all tasks in the software lifecycle can be supported directly by the EEL.

That means that an EEL must support:

1.    Statements of requirements

2.    Description of designs

3.    Low-level processing

4.    Unit and integration testing

5.    System testing

6.    Proof of correctness conditions at all life cycle stages

7.    Identification of configuration items (COBOL's Identification Division was prescient here - three cheers for Auntie Grace)

... and generally any other task in the life cycle related to product quality.



An obvious thing to do is to start designing languages that include annotations for; proofs, testing, configuration control, etc. Proof annotation are well established in SPARK Ada and within the Frama C project. It would be no great task to include proof annotations in a language itself. Proof annotations could also support automatic test generation.



Yet, looking at current programming languages, it's quite clear that we're NOT EVEN TRYING to design EELs - when the state of knowledge in computer science is almost certainly capable of giving an EEL suitable semantics and making compilers for it. What software engineering needs more than anything else is not new research but better application of what we already know.



O




This email and its attachments may contain confidential and/or privileged information.  If you have received them in error you must not use, copy or disclose their content to any person.  Please notify the sender immediately and then delete this email from your system.  This e-mail has been scanned for viruses, but it is the responsibility of the recipient to conduct their own security measures. Airbus Operations Limited is not liable for any loss or damage arising from the receipt or use of this e-mail.

Airbus Operations Limited, a company registered in England and Wales, registration number, 3468788.  Registered office:  Pegasus House, Aerospace Avenue, Filton, Bristol, BS34 7PA, UK.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20180921/49d76637/attachment-0001.html>