[SystemSafety] Safety Culture redux

Mon Feb 26 23:01:10 CET 2018

Dear Steve, David,

well, the word "static" in static checking is a bit ambiguous (imho),
because it is not a yes/no thing. There are many grey levels.

When referring to state-of-the-art static analysis, people often not
only refer to code style checkers, syntax or idiom checkers (available
for Java, C, C++), bug pattern tools, and the like showing you more or
less helpful defect metrics and disclosing a couple of known
anti-patterns or "worst practices, no gos".

However, there are several certainly academically-inspired tools which
attach some operational semantics to the checked code (Les, I wouldn't
speak of "ontologies" right here but at some point). Some people still
like to call them static analysis tools because these tools do not
literally execute the code on the given platform but instead reason
within a mathematical model they incorporate when doing the analysis.

There are very tight limits on the extent to which one can do this,
particulary, when talking about parallel programming. However, in
increasingly many practical cases, those approaches turn out to be quite
helpful when applied with expert care.

Anyway, tools of the latter kind might, e.g. use an implementation of
Hoare style assertions, like it was mentioned by David, or others might
use data flow approximations, there is a French/German product, as far
as I can remember. You might know it.

AND:
I personally like the term "defect", had quite a tough time in sorting
out such terminology when writing my thesis :) To be honest, once you
know what you are looking for in the code, it is not that important how
you call it, it is more important how you identify the real cause and
how you can get rid of it without introducing further defects.

Best,
Mario

On 26.02.2018 19:04, David Crocker wrote:
> 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
> 
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5053 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20180226/64c7359f/attachment-0001.bin>