[SystemSafety] Safety Culture redux

[David Crocker]

Steve, there are annotated static analysis techniques such as Escher
C/C++ Verifier (disclosure - a product from my company) and SPARK that
can do exactly that kind of semantic analysis, i.e. verify that each
function satisfies its contract - and that all callers to that function
satisfy their side of the contract too.

David Crocker, Escher Technologies Ltd.
http://www.eschertech.com
Tel. +44 (0)20 8144 3265 or +44 (0)7977 211486

On 26/02/2018 18:43, Steve Tockey wrote:
> Mario,
> You wrote:
>
> ³As far as I can see, the issue with static analysis is that
> there is a wide bandwidth of approaches available under this name. Some
> are good, some are outdated, some are inappropriate. The good ones that
> we desire to use, I believe, rarely come at low cost. On the contrary,
> these, even if sold as tools, require high skills and a lot of
> experience to be effective.²
>
> My concern is that these static analysis tools are only able to do
> structural (aka syntactic) analysis of the code. They are completely
> unable to do any significant semantic analysis of the code. As a simple
> example, the declared contract of a function might be that it requires X
> and guarantees Y but the analyzer is unable to tell me that the method
> code is consistent (or not) with that declared contract.
>
> Said a slightly different way, ³They call them bugs. We are trying to get
> everyone to call them defects (or, errors). But they really are just
> semantic inconsistencies². In order to be capable of finding the kinds of
> problems I care about, the tools need to be able to do semantic analysis
> of the code and that¹s orders of magnitude more difficult.
>
>
> Cheers,
>
> ‹ steve
>
>
>
> -----Original Message-----
> From: systemsafety <systemsafety-bounces at lists.techfak.uni-bielefeld.de>
> on behalf of Mario Gleirscher <mario.gleirscher at tum.de>
> Organization: Technical University of Munich
> Date: Saturday, February 24, 2018 at 6:39 AM
> To: "systemsafety at lists.techfak.uni-bielefeld.de"
> <systemsafety at lists.techfak.uni-bielefeld.de>
> Subject: Re: [SystemSafety] Safety Culture redux
>
> Dear Peter,
> dear all,
>
> Thanks for indirectly bringing up one of the many reasons why we started
> our survey on finding out the use of techniques known as formal methods
> (and, hence, many don't like them because of just the name which I think
> is sooooo sad) in various realms of software engineering practice. Last
> time I unintentionally triggered quite a discussion and would like to
> apologize for my insistence.
>
> Because Steve pointed at a classic (https://doi.org/10.1109/TDSC.2004.2)
> terminology issue "bug vs. error vs. defect", I'd like to remind those
> who haven't participated of our survey and kindly ask all of you to
> forward the link below to software practitioners who might be eligible
> to participate:
>
> https://docs.google.com/forms/d/e/1FAIpQLScMbKk3SDY62fzBujtJA-i8XKREZP40MjX
> jIZvluZSVO9-QXA/viewform
>
> Accompanying a mindset change through good terminology, we also need
> empirical studies on finding out causes of the actual social phenomena
> we are discussing. We have gained almost 100 responses, however, this is
> by far not enough.
>
> Systems are eating the world and there is no time at all to stick around
> and rely on anecdotal evidence on "best practices."
>
> @Steve: As far as I can see, the issue with static analysis is that
> there is a wide bandwidth of approaches available under this name. Some
> are good, some are outdated, some are inappropriate. The good ones that
> we desire to use, I believe, rarely come at low cost. On the contrary,
> these, even if sold as tools, require high skills and a lot of
> experience to be effective.
>
> Thank you and have a nice weekend,
> Mario
>
> On 23.02.2018 12:00, Peter Bernard Ladkin wrote:
>> It is not just schools. I had a recent experience.
>>
>> Recent graduate in math with minor in informatics, now working at a
>> company in which programs and
>> sells WWW-based services. They are using Scala, which has some
>> functional programming facility. He
>> thinks of using type theory (that is, mathematical type theory, not data
>> typing) to improve the
>> "correctness" (his word) of the programs. Are we interested?
>>
>> Here is a simplified dialog:
>>
>> Me: "Is there a requirements specification of the program you are
>> interested in?"
>> Him: "What's that?"
>> Me: "It is a description of what you (or someone) wants the program to
>> do"
>> Him: "Oh, I don't think so"
>> Me: "You used the term <correctness>. If there is no description of what
>> you want the program to do,
>> what did you mean by <correctness>?"
>> Him: "It means the program is working the way we want it to work"
>> Me: "But didn't you just tell me there was no description of that?"
>> Him: "Huh?"
>>
>> And this from someone who is, as far as I know, quite smart and quite
>> capable. In any case, I did
>> have the impression he was less interested in this aspect of things than
>> in the prospect of playing
>> around a bit with type theory. That's fine. (But it's not what I do any
>> more.)
>>
>> I have had such experiences regularly over thirty years of teaching.
>>
>> PBL
>>
>> Prof. Peter Bernard Ladkin, Bielefeld, Germany
>> MoreInCommon
>> Je suis Charlie
>> Tel+msg +49 (0)521 880 7319  www.rvs-bi.de
>>
>
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE