[SystemSafety] Correctness by Construction

[Michael Jackson]

Dewi, 

Thank you for your helpful reply. I certainly don't imagine that CbyC has no value: setting aside my pedantry about the word 'correct',  its practitioners have obviously been very successful. 

My question "What are requirements?" may be too naive to be understood, but I am still puzzled. In the CbyC context, what do 'requirements' describe, and at what granularity? For example, is 'desirable flying quality' a requirement (insofar as it is affected by the flight control software)? To what extent do requirements describe given properties of the problem world? To what extent do requirements mandate specific detailed behaviours to achieve desired properties? Are there commonly accepted notions of the structure of a set of requirements? 

Would it be right to see the requirements as the CbyC interface between aeronautical experts and software experts? If so, do formal requirements constitute an impenetrable firewall? What requirements were---or should have been---provided for MCAS software development? If requirements---even formal requirements---should be permeable, what should pass between one side and the other, and how and when? 

Your final paragraph is intriguing. 

Yours, 

-- Michael 

> On 15 Jul 2020, at 12:13, Dewi Daniels <dewi.daniels at software-safety.com> wrote:
> 
> Michael,
> 
> At Altran, they use Z to express requirements. I believe that Altran are moving to Alloy. At Callen-Lenz, we're using D-RisQ's Kapture requirements language.
> 
> You make a good point about the physical problem world. Your observation highlights the boundaries of Correctness by Construction. Consider a flight control system. Just because we can prove that the code is a correct implementation of a PID controller (for example) doesn't mean that the flight control system flies the aircraft accurately (or at all). That depends on how the PID controller is tuned and how it interacts with the airframe. We can verify the flight control system using a flight model, though the flight model itself is an abstraction of the real aircraft. Even if we can show that the flight control system flies the aircraft accurately, it doesn't necessarily mean that the aircraft has desirable handling qualities.
> 
> This doesn't mean that Correctness by Construction has no value. At Callen-Lenz, we're developing a flight control system for air taxis and personal air vehicles. We're using formal methods (specifically D-RisQ's Modelworks, CLawZ and FEVER tools) to verify that the binary is a correct implementation of the software requirements, which are expressed in Kapture. That greatly reduces the number of tests that we need to write (it does not eliminate testing altogether), meaning that we can deploy working, certifiable code very quickly using our model-based development environment.
> 
> One of the best compliments I've received was when someone said, "Dewi has the ability to just write working code". I'm not sure that person appreciated how much thought I'd put into the requirements and the design before I wrote a single line of code.
> 
> Yours,
> Dewi Daniels | Director | Software Safety Limited
> 
> Telephone +44 7968 837742 | Email dewi.daniels at software-safety.com
> 
> Software Safety Limited is a company registered in England and Wales. Company number: 9390590. Registered office: Fairfield, 30F Bratton Road, West Ashton, Trowbridge, United Kingdom BA14 6AZ
> 
> 
> On Tue, 14 Jul 2020 at 10:14, Michael Jackson <jacksonma at acm.org> wrote:
> Dewi: 
> 
> Yes: but how are requirements to be expressed and communicated to the software developers? And if the requirements are communicated, 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? And is 'correctness' a proper word to use about artifacts in the physical world at the scales relevant to software engineering? 
> 
> Yours, 
> 
> -- Michael
> 
> > On 13 Jul 2020, at 20:55, Dewi Daniels <dewi.daniels at software-safety.com> wrote:
> > 
> > Michael,
> > 
> > In the context of “Correctness by Construction”, I would say that Correctness means “compliance with requirements”.
> > 
> > Yours,
> > Dewi
> > 
> > On Mon, 13 Jul 2020 at 13:59, Michael Jackson <jacksonma at acm.org> wrote:
> > Hoping for illuminating replies, I ask an open question. 
> > 
> > In the phrase "Correctness by Construction", what does 'correctness' mean? 
> > 
> > -- Michael
> > _______________________________________________
> > The System Safety Mailing List
> > systemsafety at TechFak.Uni-Bielefeld.DE
> > Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
> > -- 
> > Yours,
> > 
> > Dewi Daniels | Director | Software Safety Limited
> > 
> > Telephone +44 7968 837742 | Email dewi.daniels at software-safety.com
> > 
> > Software Safety Limited is a company registered in England and Wales. Company number: 9390590. Registered office: Fairfield, 30F Bratton Road, West Ashton, Trowbridge, United Kingdom BA14 6AZ
> > 
>