[SystemSafety] Bursting the anti formal methods bubble

Derek M Jones derek at knosof.co.uk
Mon Oct 30 23:40:29 CET 2017


Peter,

> 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

No.  The whole point of this discussion is that it cannot be used for
assuring correct implementation of functionality, only x%, where x < 100
I assume you mean 100% correctness; thanks for supplying an example to
save me having to cut-paste a link to reply to clayton's query.


> 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
>>
>>   
>>
> 

-- 
Derek M. Jones           Software analysis
tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com


More information about the systemsafety mailing list