<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<div class="moz-cite-prefix">On 15/07/2020 12:13, Dewi Daniels
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CANQd8eUiAu57gLyMhT5v-dtEWiD+W-bG3LfG=YZEgWzAtCyPPA@mail.gmail.com">At
Altran, they use Z to express requirements.</blockquote>
<p><font size="+1">Actually, I'm not sure I agree with Dewi's
description of Altran's work.</font></p>
<p><font size="+1">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.</font></p>
<p><font size="+1">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.</font></p>
<p><font size="+1">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:<br>
</font></p>
<p><font size="+1">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.<br>
</font></p>
<p><font size="+1">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.</font></p>
<p><font size="+1">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.</font></p>
<p><font size="+1">- Rod</font></p>
<p><font size="+1"></font><br>
</p>
</body>
</html>