Re: SPARK User Group 2008

["Michael" <Michael@home.ca>]

"Stuart" <stuart@0.0> wrote in message 
news:483d26f5$1_1@glkas0286.greenlnk.net...
> "Michael" <Michael@home.ca> wrote in message
> news:ZCY_j.169009$rd2.39062@pd7urf3no...
>
>  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 report your finding to Praxis-HIS.  They 
might appreciate your support.  (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 important." (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 Transport)

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