[SystemSafety] Correctness by Construction
Roderick Chapman
rod at proteancode.com
Tue Jul 21 15:59:35 CEST 2020
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>
More information about the systemsafety
mailing list