Experiment in the application of FMME techniques for scaling up assurance efforts by enhancing popular proof tools via the use of theory morphisms between sessions

The Cyber & Electronic Warfare Division (CEWD), Defence Science and Technology Group at Edinburgh, South Australia, have a requirement to conduct research advancing the scalability of assurance techniques for Trustworthy Systems. DST Group requires that a small experiment be conducted in the inclusion of scaling capabilities in existing systems assurance tools. This project will concentrate at the specification level, with the aim of using ZF as a mediator via theory morphisms with Isabelle HOL in the first instance. The expectation is that features required for large scale systems engineering efforts can be developed at the ZF level and used to generate specific system modelling contexts for analysis in Isabelle HOL.