Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.arch.embedded > #30635

Re: (Semi-) formal methods

Show all headers | View raw

On 5/15/2021 3:54 AM, Clifford Heath wrote:
> On 15/5/21 7:10 pm, Don Y wrote:
>> Unfortunately, use in such a document is not suited for "general audiences"
> 
> The goal of CQL is to make the formal model suitable for (and expressed in the 
> language of) anyone generally familiar with the domain being modelled.

I opted for OCL as my system is object-based, UML is relatively easy to
understand and the way things would be expressed closely mimics the
way those constraints would be imposed in the code.  Any "translation"
effort would introduce other opportunities for errors to creep in.

>> because it lacks rationale for each item in the specification.
> 
> Actually rationale is seldom needed. What is needed is an example of the 
> scenario that is allowed or disallowed by each definition. The example is 
> almost always an adequate rationalisation.

I disagree.  I find many cases where I need to resort to prose to
explain why THIS implementation choice is better than THAT.  Just
*stating* (or implying) that it is leaves too much to the Reader,
as an "exercise" ("Now WHY, exactly, would this be a better approach?")

For example, I had to make a decision, early on, as to whether or
not "communications" would be synchronous or asynchronous.  There
are advantages and drawbacks to each approach.  From a performance
standpoint, one can argue that async wins.  But, from a cognitive
standpoint, sync is considerably easier for "users" (developers)
to "get right"; message and reply are temporally bound together
so the user doesn't have to, *later*, sort out which message a
subsequent reply correlates with (icky sentence structure but it's
early in the morning  :< )

The fact that comms then become blocking operations means any
desire for concurrency has to be addressed with other mechanisms
(e.g., set up a thread to do the comms so the "main" thread can
keep working and make the coordination between these two -- which
now appear asynchronous -- to be more visible.)

Or, trying to explain the many ways a particular comm can fail
(e.g., what if the party on the other end never listens?
Or, *can't* listen?  Or, the processor hosting it powers down?
Or...) and how the response/detection of that failure can
vary based on where in the "failure" it occurs.

>> The alternative is: an /ad hoc/ specification (with some likely incompletely
>> specified set of loose rules) *or* an *absent* specification.  Each of these 
>> leave gaping holes in the design that (supposedly) follows.
> 
> That's precisely true. That's why analytic (formal) models are needed.

I'm not sure the models need to be mechanically verifiable.  What *needs*
to happen is they need to be unambiguous and comprehensive.  You should
be able to look at one (before or after the code is written) and convince
yourself that it addresses every contingency -- as well as HOW it does so
(to the appearance of other actors)

>> Again, why the resistance to adopting such a "codified" approach?
> 
> Hubris, mostly. People genuinely don't see the need until enough experience has 
> humbled them, and by then, their accumulated caution and tentativeness mean 
> their industry sees them as dinosaurs.

"Hubris" suggests overconfidence (in their abilities).  I'm not sure
that's the case.

I started looking for a "common ground" in which I could express my current
design when I "discovered" that, not only is there no such thing, but that
there isn't even a common approach (methodology) to design.  It's not
a question of whether method A or method B is the more common (and, thus,
more readily recognizable to adopt in my presentation) but, that NONE OF
THE ABOVE is the clear winner!

[I couldn't even get a concensus on how to *diagram* relationships
between actors/objects just for illustrative purposes!]

This prompted the question, here.

I've been looking back over the past experiences I've had with getting
folks to "move forward" to try to see if I can identify the issue that
leads to this resistance.

Early on, I can argue that a lack of understanding for the (software)
design process led some employers to skimp in ways that they might
not have realized.  E.g., when a development seat cost many thousands of
1975 dollars, you could see how an employer, new to using MPUs *in*
their products, could decide to "share" a single seat among several
developers.

Similarly, when ICEs came on the scene.

And, HLLs.

But, those issues are largely behind us as there are many "free"/cheap
tools that can make these sorts of decisions "no brainers".

I can also see how scheduling pressures could lead to a resistance
to adopt new methods that *claim* to improve productivity.  I've
never been in an environment where time was allotted to explore
and learn new tools and techniques; there's another product that's
anxious to make its way to manufacturing (and YOU don't want to
be the one responsible for stalling the production line!)

I can see how fear/uncertainty can lead individuals (and organizations
as organizations are, at their heart, just individuals) to resist
change; the process you know (regardless of how bad it might be) is
safer than the process yet to BE known!

For things like specification and modeling, I can see a preception of
it as being a duplication of effort -- esp the more formally those
are expressed.

And, for some, I think an amazing lack of curiosity can explain their
clinging to The Way We Always Did It.  Or, the lack of "compensation"
for the "risk" they may be taking ("Heads, you win; tails, I lose!")

*Most* of these arguments can be rationalized by "employees" -- the
excuse that THEY (personally) don't have any control over THEIR
work environment.  OK, I'll avoid getting into *that* argument...

But, for folks working in more permissive environments (e.g.,
independent contractors), most of the arguments crumble.  YOU can
make the time to learn a technique/tool; YOU can buy the tool;
YOU can gauge its impact on YOUR productivity; etc.

I have a lot of respect for my colleagues -- they've all got
proven track records with significant projects.  Yet, they still
fall into this pattern of behavior -- clinging to past processes
instead of exploring new.  To their credit, they will make an
effort to understand the approaches and technologies that *I*
pursue -- but, that's more the result of a personal relationship
(than a BUSINESS one).  Yet, I never hear any epiphanies where
they exclaim "this is SO COOL"...  is the pull of the familiar SO
overwhelming?

[I left the 9-to-5 world primarily so I could dabble in other
fields, techniques, etc.  I have no desire to make "model 2",
especially if it will follow "process 1"!]

Back to comp.arch.embedded | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread

Thread

(Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-11 18:25 -0700
  Re: (Semi-) formal methods Theo <theom+news@chiark.greenend.org.uk> - 2021-05-13 15:25 +0100
    Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-13 11:57 -0700
      Re: (Semi-) formal methods Theo <theom+news@chiark.greenend.org.uk> - 2021-05-14 10:43 +0100
        Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-14 12:37 -0700
          Re: (Semi-) formal methods HT-Lab <hans64@htminuslab.com> - 2021-05-15 08:44 +0100
            Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-15 02:48 -0700
          Re: (Semi-) formal methods Theo <theom+news@chiark.greenend.org.uk> - 2021-05-15 12:02 +0100
            Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-15 15:07 -0700
  Re: (Semi-) formal methods Dave Nadler <drn@nadler.com> - 2021-05-13 19:32 -0400
    Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-13 16:57 -0700
    Re: (Semi-) formal methods Paul Rubin <no.email@nospam.invalid> - 2021-05-14 12:22 -0700
  Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-14 21:55 -0700
  Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-14 21:52 -0700
    Re: (Semi-) formal methods Clifford Heath <no.spam@please.net> - 2021-05-15 18:14 +1000
      Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-15 02:10 -0700
        Re: (Semi-) formal methods Clifford Heath <no.spam@please.net> - 2021-05-15 20:54 +1000
          Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-15 12:26 -0700
            Re: (Semi-) formal methods Clifford Heath <no.spam@please.net> - 2021-05-16 11:41 +1000
              Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-05-16 00:35 -0700
                Re: (Semi-) formal methods Clifford Heath <no.spam@please.net> - 2021-06-02 12:03 +1000
                Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-06-01 22:23 -0700
                Re: (Semi-) formal methods Clifford Heath <no.spam@please.net> - 2021-06-02 22:39 +1000
                Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-06-02 09:01 -0700
                Re: (Semi-) formal methods Clifford Heath <no.spam@please.net> - 2021-06-03 11:54 +1000
                Re: (Semi-) formal methods Don Y <blockedofcourse@foo.invalid> - 2021-06-03 01:56 -0700
  Re: (Semi-) formal methods Clifford Heath <no.spam@please.net> - 2021-05-15 14:15 +1000

csiph-web