[SystemSafety] "Suggestions about processes / tools that may help organisations to become 'more formal'"

Daniel Kästner kaestner at absint.com
Wed Nov 8 08:59:00 CET 2017


Dear David,

that is a very nice survey which in my opinion sums up many different 
aspects quite nicely.

Just one addendum regarding sound code analysis: with Astrée our customers 
routinely analyze C code bases of 2MLOC and beyond these days (cf. paper 
below for one example), so it scales to contemporary software sizes.

Cheers,
  Daniel.

Reference:
D. Kästner, A. Miné, L. Mauborgne, X. Rival, J. Feret, P. Cousot, A. 
Schmidt, H. Hille, S. Wilhelm, C. Ferdinand. Finding All Potential Runtime 
Errors and Data Races in Automotive Software. SAE Technical Paper 
2017-01-0054, SAE World Congress 2017, Detroit, April 2017. 
doi:10.4271/2017-01-0054. Available from: 
http://papers.sae.org/2017-01-0054/

---
Dr.-Ing. Daniel Kaestner ----------------------------------------------
AbsInt Angewandte Informatik GmbH      Email: kaestner at AbsInt.com
Science Park 1                         Tel:   +49-681-3836028
66123 Saarbruecken                     Fax:   +49-681-3836020
GERMANY                                WWW:   http://www.AbsInt.com
----------------------------------------------------------------------
Geschaeftsfuehrung: Dr.-Ing. Christian Ferdinand
Eingetragen im Handelsregister des Amtsgerichts Saarbruecken, HRB 11234

> -----Ursprüngliche Nachricht-----
> Von: systemsafety 
> [mailto:systemsafety-bounces at lists.techfak.uni-bielefeld.de] Im Auftrag 
> von David MENTRÉ
> Gesendet: Dienstag, 7. November 2017 22:42
> An: systemsafety at lists.techfak.uni-bielefeld.de
> Betreff: [SystemSafety] "Suggestions about processes / tools that may help 
> organisations to become 'more formal'"
>
> Dear Mr Pont,
>
> Le 2017-10-26 à 11:21, Michael J. Pont a écrit :
> > There are people on this list who are formal-method 'fans' (some would 
> > say 'fundamentalists').
>
> I would probably be classified as one of those formal methods 'fans': I
> am part of corporate research of a big industrial group and do research
> on formal methods and their application to industrial developments.
>
> Nonetheless, I also apply by myself formal methods (FM) to real
> industrial software (railway, automotive, factory automation, ...,
> 80-100 Kloc range) so hopefully I keep a critical view on the limits of
> the tools and their applicability to industrial developments with 'real'
> people.
>
>
> > In some cases, I think such FM people 'need to get out more' - and spend 
> > time with the development teams in real (often fairly
> small) organisations that are struggling to create safety-related systems. 
> Such teams usually have very limited time and resources
> available: this does not mean that they are populated by 'bad people' who 
> want to create poor-quality systems.
>
> As other people said, even in big groups people are struggling with
> limited time and resources.
>
> > Shouting at people because they are not using formal methods doesn't 
> > really help ...
>
> I can only agree.
>
> >  Offering suggestions about processes / tools that may help 
> > organisations to become 'more formal' would - in my view - be more
> productive.
>
> As Peter said, your question is far to broad to give a precise answer. I
> nonetheless try to give below some suggestions, hopefully in a
> constructive manner. I'll give names of companies and products. I'm not
> affiliated to any of them, it is just to show that supporting tools and
> companies do exist. Most of those tools also exist as Free Software or
> at least at no cost, so you can do some experiments. Some of them are
> even available online, so you don't even need to install them.
>
> Subjectively from the easiest to the most difficult, not in successive
> step (i.e. this is not a process):
>
>  0. Apply Good-Old-Software-Engineering principles. My short recommended
> reading list is "Better Embedded System Software", P. Koopman
> (http://koopman.us/) and "The Pragmatic Programmer", A. Hunt and D. 
> Thomas.
>
> Often they are a first steps towards the use of formal methods. For
> example, Better Embedded System Software book recommends simple and
> predictable software with minimal complexity, a prerequisite for
> successful application of formal methods. As another example, The
> Pragmatic Programmer recommends Design-by-Contract which is the first
> step towards application of Deductive Verification (aka Hoare-logic
> verification).
>
>  1. Re-use existing kits already proven with formal methods. You have C
> Compiler (AbsInt's CompCert), Operating Systems (seL4, Prove&Run's
> Provencore, ...), ... No need to change your process or learn "Formal
> Methods", you just use it as you would use other software components.
> They can nonetheless give you strong guaranties, e.g. faithful C code
> translation to assembler for CompCert or strong guarantees on process
> isolation for Provencore.
>
>  2. Use a language with strong typing. For example, for low level
> programming, you can use Ada instead of C. You'll structurally avoid a
> bunch of errors. If you are using Ada, you can even restrict yourself to
> the SPARK formal subset. Even without proof, you'll gain a deterministic
> language. Companies like AdaCore can help you.
>
> This can be very easy or very difficult, depending on your corporate
> culture. To my despair in my company this is nearly impossible.
>
> New languages like Rust have very interesting properties through their
> advanced type system (e.g. guarantee statically absence of memory
> allocation issue or concurrency issue) but applicability to regular
> programmers remains to be checked.
>
>  3. Use (sometimes FM) tools to automatically generate test cases. You
> do not modify your existing process, just automate part of it, making it
> less costly and free of some human errors. Look at tools like
> VectorCast, PathCrawler (https://frama-c.com/pathcrawler.html) or CBMC.
>
> You can also use Design-by-Contract, i.e. pre-/post-conditions on
> routines, to have more thorough dynamic check with tests. In Ada
> contracts can be compiled to dynamic assertions by default. In C you can
> use Frama-C / E-ACSL. Once your programmer are at ease with
> Design-by-Contract, they'll be ready to do proof of those contracts.
>
> You can also apply sound static analysers (see 4. below) on your
> existing tests. If the tool triggers an error, it is a real alarm. No
> false alarm. TrustInSoft's tisinterpreter
> (https://trust-in-soft.com/tis-interpreter/) is such a tool.
>
>  4. Apply sound (i.e. based on formal methods) static analysers like
> TrustInSoft Analyzer, Frama-C / Value Analysis, AbsInt's Astrée,
> MathWorks' Polyspace. They guarantee absence of run time error
> (out-of-bound array access, division by zero, ...). Their are applicable
> on existing C or Ada code to relatively big code size (100-200 Kloc)
> with low to medium effort.
>
> If you are using Ada, you can use SPARK tools to prove absence of
> runtime errors.
>
>  5. Design models using formally defined languages like SCADE and
> automatically generate code from it. You need to change your programming
> language. Depending on your programmers' background, it might be very
> easy to very difficult. You can also do the same thing using MathWorks
> Simulink (easy if you are in automotive industry), but be aware that
> Simulink is far from being a formally defined language (but you can
> always restrict yourself to a well defined subset of it).
>
>  6. Apply Model Checker or SAT/SMT solvers to models of your system or
> your target code. Tools like SPIN or CBMC come to mind. Such tools can
> be quite easy to use (CBMC) to more involved (SPIN), especially when you
> need to define the key properties to verify. Model Checker can be
> particularly useful to check concurrent systems. However they suffer
> from the state explosion problem, so models need to be designed
> carefully, i.e. use of formal methods becomes more involved. For example
> SCADE has a Model Checker tool but I know no industrial use of it
> (except in a Korean Nuclear very simple shutdown system). On the
> contrary, companies like SafeRiver have successfully developed and
> proved correctness of railway signalling system with MathWorks tools.
>
>  7. Apply Deductive Verification to prove key properties, routine by
> routine. There are two main issues: (i) write the formal properties
> corresponding to your key safety and security properties and (ii) prove
> them using the tools. For (i), this can be very easy to very difficult,
> depending on properties. For (ii), it depends on your code. If you have
> control dominated code without any loops, tools will prove your
> contracts automatically in a glimpse (I have seen industrial code having
> such form). If you have floating point code and you want to prove
> algorithm correctness, be prepared to a strong effort.
>
> For Ada you have SPARK, for C you have Frama-C / WP, for Java you can
> use openjml, etc.
>
>  8. Apply the formal method to the complete development process, from
> specification to implementation, typically using B Method and its formal
> refinement process. You need to completely change your development
> process and invest in strong training of your team. You'll gain very
> strong guarantees (e.g. 0 to 4 errors for 200 Kloc) on the resulting
> software. People (i.e. Siemens and Alstom) have done it for CBTC
> (Communication Based Train Control) safety critical software and railway
> signalling systems for 20 years, up to ~200 Kloc software. Companies
> like ClearSy or Systerel can help you.
>
>  9. Develop certified tools like CompCert or seL4 by yourself using
> proof assistant like Coq or Isabelle. Be prepared to invest years of
> training and learning, or hire a PhD having done his/her PhD with such
> tools. You can do whatever tools with whatever guarantees you want. Only
> cost would limit you. CompCert cost is about 20-30 man.year with very
> talented people. If I remember correctly seL4 cost is in the same range.
> But tools are improving, proof techniques are improving, knowledge is
> spreading in the formal method community.
>
> Above classification is my own view but you'll see similar
> classification by other people, e.g. Stone, Bronze, Silver, Gold levels
> of AdaCore and Thales:
>   https://www.adacore.com/books/implementation-guidance-spark
>
>
> I hope I have given enough food for thought while being realistic. Do
> not hesitate to ask questions if needed, on this list or privately.
>
> Sincerely yours,
> D. Mentré
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE


More information about the systemsafety mailing list