--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on November 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] I wrote a blog post about my experiences with Frama-C so far



sön 2018-11-25 klockan 20:17 +0100 skrev David MENTRÉ:
> Hello,
> 
> Le 22/11/2018 à 14:07, Tomas Härdin a écrit :
> > This is actually a topic I have planned for a future post.
> > Comparing
> > the CPU time and developer time vs benefit of some common software
> > QA
> > methods.
> 
> I would be interested in such a post, especially if you have some
> figures.

Figures might be hard, but rough estimates and sort of ranking the
different methods against eachother should be possible.

> >  Verification can replace unit testing outright, in my opinion.
> 
> :-) In fact, this has already be done 20 years ago (1998 for Paris
> Metro line 14), for example for fully-automatic train control
> software developed using the B Method. No unit test, no integration
> test. And of course functional tests were kept.

Nothing new under the sun, eh?

> By the way, you say in your post:
> > Frama-C is not a panacea, since it says nothing about how long a
> > program might take to execute.
>  In fact, some research work has been done on that topic:
>  Certifying and Reasoning on Cost Annotations in C Programs 
>  https://link.springer.com/chapter/10.1007%2F978-3-642-32469-7_3

Neat. Can't access the paper, sadly.

/Tomas