[SystemSafety] "Suggestions about processes / tools that may help organisations to become 'more formal'"
David MENTRÉ
David.MENTRE at bentobako.org
Tue Nov 7 22:42:01 CET 2017
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é
More information about the systemsafety
mailing list