[SystemSafety] Correctness by Construction

[Roderick Chapman]

On 15/07/2020 12:13, Dewi Daniels wrote:
> At Altran, they use Z to express requirements.

Actually, I'm not sure I agree with Dewi's description of Altran's work.

I worked on several of the "CbyC" projects at Praxis and Altran over the 
years, notably SHOLIS, and the MULTOS CA, and had more peripheral 
involvement in Tokeneer and iFACTS.

I was not involved in the construction of Requirements and Specification 
artefacts on those projects (I was more on the implementation end of 
things). Those aspects were led by the likes of Anthony Hall, Jonathan 
Hammond and Janet Barnes.

I would characterize the overall approach as following Michael's Problem 
Frames model. I'm sure Michael will correct me if get this wrong, but I 
recall the basic approach as:

Requirements are optative statements concerning entities and things in 
the World that are made true by the introduction of the Machine. This is 
expressed in notations like system context diagrams and English.

Specifications (which is where Z does fit in) are formal/mathematical 
statements regarding the behaviour of phenomena at the interface between 
the Machine and the World.

Note: Z is excellent for some types of behavioural specification, and is 
always supported by English text. We also used CSP (for concurrency on 
the MULTOS CA), SCADE (closed-loop control on another project), Parnas 
tables, and whatever else might fit the bill. As Dewi said, Altran have 
recently started using Alloy on a project, but I have no idea what that 
particular application is at this time.

- Rod


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20200721/87bf59d1/attachment.html>