[SystemSafety] Bursting the anti formal methods bubble

[Peter Bishop]

I think the discussion in this list illustrates the fact that FM (as
normally defined) is not a panacea.
It can be used for assuring correct implementation of functionality, but
is not so good for other key features of real time embedded systems, e.g.

- meeting timing requirements
- meeting other resource constraints (like stack limits)
- correctness of data

Imagine for example, we had an AI system where the AI learning algorithm
was formally specified and proved.
- How do we show its real-time response is fast enough?
- Can we be sure that that it won't hit some implementation resource limit?
- Can we trust the data derived by the AI learning algorithm will ensure
a safe response on all circumstances?

Peter Bishop


On 28/10/2017 09:44, Michael J. Pont wrote:
> Steve,
> 
> Thanks for your reply.
> 
> I agree with your comments.
> 
> Some people on this list are already aware of my background (I’ve been
> helping organisations to build ‘Time Triggered’ systems for 20+ years). 
> The process involved allows precise modelling of timing behaviour (at
> design time) and monitoring of this behaviour (at run time).  This is a
> ‘semi formal’ process.  It's not the right approach for every system but
> – when it is a good match – it’s very effective (in my experience). 
>  I’ve helped to develop numerous safety-related TT systems.
> 
> What I have been wondering (over a period of several years, as a
> background activity) is whether the addition of some FMs would provide a
> means of improving confidence in the safety of some ‘high end’ TT
> systems.  The potential match is obvious: we use the TT design process
> to increase confidence that the timing behaviour will match the spec; we
> use the FM to increase confidence that the functional behaviour
> (particularly the task behaviour) will match the spec.
> 
> I’ve been motivated to look more closely at the FM issue by the
> discussions that I’ve had over the last 12 months or so with developers
> of autonomous vehicles, and developers of components for use in such
> vehicles.   These systems (at SAE Level 3 and above) provide enormous
> technical challenges.  In my view, we (as a planet) are going to need
> all the help we can get if these systems are to operate safely and
> reliably, and it seems to me that FMs may have a role to play here.
> 
> The various comments that I’ve received on this list (and in private
> emails off list) in the last few days have provided much food for
> thought.   I now need to do a little more research.
> 
> Michael.
> 
> *From:*Steve Tockey [mailto:Steve.Tockey at construx.com]
> *Sent:* 27 October 2017 19:35
> *To:* M.Pont at SafeTTy.net; systemsafety at lists.techfak.uni-bielefeld.de
> *Subject:* Re: [SystemSafety] Bursting the anti formal methods bubble
> 
> Michael J. Pont wrote:
> 
> “Will FMs help such small automotive teams?”
> 
> I would argue that some amount of at least semi-formal methods will
> help. However, no change in common practice will happen unless it can be
> shown that there is a business benefit to an increase in formality, like:
> 
> *) a reduction in development project cost and/or schedule
> *) a reduction in defects delivered (e.g., ability to reduce or avoid
> product recall)
> *) a reduction in product lifetime maintenance costs
> 
> Without a demonstration of benefit to the business, you’re unlikely to
> get organization to adopt whatever you are selling.
> 
> “If the development process for such teams is to become more formal, how
> should they get started?”
> 
> I would argue that there are two very powerful first steps:
> 
> *) Adopt semi-formal modeling of requirements and design, like using UML
> state charts
> 
> *) Adopt Design-by-Contract as a part of standard practice
> 
> 
> “How much ‘FM’ is enough to protect the company if the product goes
> wrong and they end up in court (a risk that you raised in a recent post)?”
> 
> I’m not a lawyer however I have been involved in some expert witness
> work in a couple of software cases. At least in the US, companies can
> avoid or reduce their legal liability as long as they can show that they
> used “generally accepted professional practices”. Being able to show
> that you did more than just generally accepted practice—by using FM—can
> only help your case.
> 
> — steve
> 
>  
> 

-- 

Peter Bishop
Chief Scientist
Adelard LLP
24 Waterside, 44-48 Wharf Rd, London N1 7UX
http://www.adelard.com
Recep:  +44-(0)20-7832 5850
Direct: +44-(0)20-7832 5855

Registered office: Stourside Place, Station Road, Ashford, Kent TN12 1PP
Registered in England & Wales no. OC 304551. VAT no. 454 489808

This e-mail, and any attachments, is confidential and for the use of
the addressee only. If you are not the intended recipient, please
telephone 020 7832 5850. We do not accept legal responsibility for
this e-mail or any viruses.