TLA+

[Jack Ring]

My associate, Dr. Tony Pizzarello, notes the following. I will appreciate any response, pro or con.

TLA+ is used by Microsoft and Amazon among others. TLA+ is a temporal logic based approach to show that a design (model) is acceptable.  However it is not adequate for approving existing candidates as Fit For Purpose or Ready for Mission. System Readiness certification must reflect the code that will be executed not abstractions that are easy to manipulate for temporal logic proofs. 

Jack Ring

[Jack Ring]

Thanks for this.  

I should have provided a reference for TLA+. See https://en.wikipedia.org/wiki/TLA%2B

The issue we raise may be rather obvious to many systems practitioners but not to enough. 

Yes, "System 'readiness for use' assertions must be based on as-is and as-configured, not merely as-designed.” We think that a TLA+ conformant design does not ensure this? We think actual components and code cannot be assessed with TLA+. 

Jack

On Apr 30, 2017, at 00:40, Hillary Sillitto <hillary....@blueyonder.co.uk> wrote:

Jack

I assume TLA does not in this case mean 'Three Letter Acronym'?

Presumably 'is acceptable' applied to a design model implies that the design adequately addresses the need in envisaged sunny and rainy day scenarios, and is ready for implementation. 

System 'readiness for use' assertions must be based on as-is and as-configured, not merely as-designed.

Best

Hillary

Sent from my iPad