"Stuart" <stuart@[EMAIL PROTECTED]
> wrote in message
news:483d26f5$1_1@[EMAIL PROTECTED]
> "Michael" <Michael@[EMAIL PROTECTED]
> wrote in message
> news:ZCY_j.169009$rd2.39062@[EMAIL PROTECTED]
>
> must do better!
> Stuart
Right Stuart you had the point: you extended the safety view, but stuck on
details and get mixed up.
From that view, you could almost tell that the Praxis Correctness by
Construction formal methods are incompatible with a software-intensive
safety-critical large-scale system like NERC.
(Please, don't confound with the formal methods, (from engineering control
theory); which provide mathematical guarantee of the modeled system's
behaviour in the presence of state and input constraints. e.g.: design of
multi-objective control laws that by construction will guarantee
stability,
and prevent input saturation.)
Praxis CbC formal methods are mathematical abstractions transposed within
the software development domain (i.e.: Z, SPARK). The intents are to
enhance reliability by verifying coherence of specifications, code
semantic
correctness and resilience to dataflow defects.
Such CbC set of principles, distilled from formal methods, (like he said),
should have been diluted within some engineering crystal-clear water.
That
would have prevented Praxis-HIS to drive iFACTS crazy - as well as most of
his engineers - quite probably.
NATS's NERC was developed by Lockheed Martin, in Rockville, MD. After
some
adaptations in the UK (e.g.: problems with 0 degrees longitude, and so on
....) NERC went solid like a rock - finally.
iFACTS is almost plug and play (Lockheed Martin enhanced the NERC
interfaces
accordingly).
iFACTS successful development announcements were interrupted soon after
March the 7th 2007. Indeed soon after iFACTS hit NERC at the NATS final
trial, (probably, just by the time Praxis-HIS consults his formal
specifications and tried to figure what could have happened?).
A solution: keeping the rock and getting a new Ferry (rock proof)?
Praxis-HIS probably didn't yet realize it should be more cost and time
effective if Lockheed Martin were restarted the job, but in a compatible
NERC Maryland style manner - (i.e.: SEI CMMI level 3 or higher).
iFACTS development is following an old predictable pattern (e.g.: SEI CMMI
-
between level 1 and 2). i.e.: Increasing the divergences without
addressing
deficiencies, delays or reducing risks, that is not an innovation. ATC
projects are all interconnected. Better to keep that on track, like that:
http://www.bcferries.com/about/super_c_tracker.html)
NERC using Praxis' iFACTS is composing one hybrid system made from hybrid
technology and hybrid development process and methods.
It is increasingly common to see safety risks arising from the unforeseen
interactions of reliable sub-systems.
Get a problem. On which of these sub-systems a correction can be applied?
Consider both systems can have a few intrinsic defects. (One more than
the
other).
Knowing one dysfunction, can you retrace the related deficiency by
following
the anomalies across different conceptual models?
You would have to continuously transpose your finding from one model to
the
other, and reciprocally.
(Worst: software development environments have not to be compatible.
Problem solving tools either. Easy to get caught by a lot of non related
points - depending of the size of the views, they might look weird, but
are
not necessarily related to any anomaly).
Stuart, you already get mixed up by the transposition of a simple lack of
visibility (iFACTS lack of testing vs. misuse of Ferry equipment).
Ada wrote an application without a target to apply. Later, it worked!
iFACTS conceptual methods are also about math!
Never heard of the Laplace transform? - Application domains and purposes
are
different, but one corollary is the same: an error made in one domain can
hardly bee seen in the other, but within the applications' results - i.e.:
quite too late).
Please, would you be kind enough to re****t your finding to Praxis-HIS.
They
might appreciate your sup****t. (i.e.: While completing SHOLIS, they
perceived a few of the limitations for more complex projects. Whether they
didn't remember or wanted a second opinion).
From another hands, Praxis-HIS inappropriately promotes HIS High Integrity
Software capability by emphasizing the SPARK approach to safety and
security.
Better to say, "SPARK suits for writing programs that need to be reliable,
and thus particularly relevant to those applications areas where safety
and
security are im****tant." (John Barnes)
Reliability is based on the probability an item will perform its required
function in the specified manner over a given time period and under
specified or assumed conditions.
Beyond reliability, safety is not exactly a SPARK capability.
Safety is a planned, disciplined, and systematic approach to preventing or
reducing accidents throughout the life cycle of a system. That requires
getting the global safety picture (even the configuration data).
"Too narrow, a view of architecture will lead to a very pretty
infrastructure, but the wrong infrastructure for the problem at hand".
(Grady Booch)
"The safety risk associated with a complex software-intensive system is a
dynamic property that could easily vary with modifications to the system
or
changes to the operational environment.
Mechanical, electrical, chemical and many other engineering disciplines
have
well established approaches for managing safety risk. However, the
increasing dependence of complex systems on software control has
fundamentally changed the source of safety risk for such systems."
Engineering is not an exact science. There is no simple solution. Safe
systems require time, effort, special engineering knowledge and
experience.
Like it said, the SPARK Praxis-HIS approach has still that advantage: It
didn't made iFACTS reliable, but safe since iFACTS can't be used.
Assuming another safety risk is just a matter of not delaying for long
some
Medium Term Conflict Detection capabilities within NERC.
Cheers,
Michael,
Vancouver, BC
THE POINT:
"It is not enough to talk about "absolute safety" and of "zero accident".
There must also be proper organisation and management to ensure that
actions
live up to words." (UK Department of Trans****t)
iFACTS didn't go strait to this point! Praxis-HIS is not even pretending
he
could!
For satisfying DoT, an US detour seems appropriated.
http://www.praxis-his.com/pdfs/cost_effective_proof.pdf
http://www.anthonyhall.org/html/papers_on_formal_methods.html
|
