[SystemSafety] Correctness by Construction

[David Crocker]

On 14/07/2020 17:06, Brent Kimberley wrote:
> >> how are the software developers to reason reliably about the
> physical problem world where the important requirements are located
> and defined, and will---or will not---be satisfied?
>
> An automated World view inquiry framework? epistemology automation? ;)

The way I suggested doing that when using Perfect Developer to develop
and (to some extent) verify the software requirements is to include a
model of the external physical system in the requirements specification.
It is then possible to reason and construct proofs about the combined
behaviour of the software + physical system, including the effects of
external inputs. This approach is in principle applicable to other
tool-supported formal specification languages, for example Z.

Although this is conceptually simple, the problem lies in constructing a
model of the physical system and possible external inputs that is
sufficiently accurate and complete to make the proofs meaningful and useful.

Cheers

David Crocker, Escher Technologies Ltd.
http://www.eschertech.com
Tel. +44 (0)20 8144 3265 or +44 (0)7977 211486


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