[SystemSafety] Bursting the anti formal methods bubble

[Michael J. Pont]

Martyn,

 

This is a very helpful reply – thank you.

 

I will investigate further.

 

Michael.

 

From: systemsafety [mailto:systemsafety-bounces at lists.techfak.uni-bielefeld.de] On Behalf Of Martyn Thomas
Sent: 27 October 2017 12:05
To: systemsafety at lists.techfak.uni-bielefeld.de
Subject: Re: [SystemSafety] Bursting the anti formal methods bubble

 

Michael

A few responses are embedded below.

 

On 27/10/2017 08:01, Michael J. Pont wrote:

Martyn,

 

Thank you for your reply.

 

I am happy to accept that cybersecurity represents a significant challenge for developers of a wide range of modern embedded systems.

 

I see another key challenge (it is not unrelated).

 

In my experience, key parts of the automotive supply chain involve companies much smaller than Bosch or Siemens.  The team developing such embedded systems may involve 10 people or less (covering both hardware and software).  Companies with teams of this size are building safety-critical components (such as sensors) that will be used in highly-autonomous vehicles in the next few years.

Such organisations typically work in ‘C’ and target small microcontrollers (something like a ‘Cortex M4’ would be typical).  They will often (in my experience) struggle to get to grips with ISO 26262.  They have a lot of work to do, and often produce products with small profit margins (around 2% is typical for high-volume automotive components).  

The teams in Bosch, Siemens, SSF and SAP that were part of the DEPLOY project that I mentioned were small groups. Even in a big company, the team responsible for a component may be quite small.



Will FMs help such small automotive teams?  

I believe so, but you remind me of another barrier to adopting FMs that I failed to mention before. Companies that are able to bid accurately often price their bids higher than competitors who price their bids by deciding what the winning price will be, bidding that price and relying on the client having to make changes to their informal requirements statement and therefore haveing to pay for contract changes. It is infuriating to lose a bid to a competitor and to find out later that after a string of contract changes, the customer has had to pay more than the losing bid that we put in. So we had to find a way to convince the customer that our higher bid was good value and we did this by offering long, free warranties against defects found after the client had signed off our formal specification. 

So one issue that I would like to overcome is the customers' unwillingness to purchase software the way that they purchase new buildings – with an initial contract placed with a system architect, to establish and formalise the requirement specification in detail, followed by a development contract let competitively against that detailed specification.



 

If the development process for such teams is to become more formal, how should they get started?  

In my opinion, in small steps. I would start by introducing formal specifications - maybe not for a whole system or even a subsystem but for the tricky algorithms or the most obscure requirements. It is strtling how many questions this can reveal and how much benefit you get from finding these questions and answering them early in the project. 

The specification langiage Z might me a good place to start. Praxis's internal Z course was 5 days: one day of maths and notations and four days of Z. By the end, staff could read a Z specification and work from it successfully, learning to write a good specification took longer and was best done on a real project with support from an expert.

I would expect to recover this up front investment in training in the first project. 



 

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

That depends on the project and the circumstances - and on the expertise of the prosecution and defence experts. But even using a strongly-typed language might avoid the defects that could lead you to be in court in the first place. I wouldn't advocate using better methods to create a courtroom defence, but as a professional approach that should greatly reduce the risk of ever having to appear in court!




 

In my view, this isn’t just an automotive problem.  For example, I also work with small teams (often at the heart of organisations with several hundred employees) developing safety-critical industrial systems in compliance with IEC 61508.   The challenges here are very similar.

Yes. See above.



 

Overall if – as I believe you have argued – FMs represent ‘state of the art’, then we either need to provide FM tools and clearly-defined processes that can be shown to work effectively with very small teams, or we will need to re-structure the automotive supply chain (and probably the supply chain in other safety-related sectors too) …

Look at the tools and methods that the very small Praxis team used on Tokeneer, 20 years ago. The Tokeneer project taught these methods to a couple of bright NSA interns in a couple of weeks plus email support, and the interns used them successfully to enhance the system significantly. The tools and methods and documentation are even better now.

Martyn

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20171027/b50cfa25/attachment-0001.html>