Next Generation Technologies Fund – Formal Mathematical Modelling Environment (Medium priority) (closed)
Defence is rife with systems with critical properties that must be satisfied to ensure safety, security or mission-suitability. A regime of accreditation as `fit for purpose’ has been developed which incorporates evaluation aimed to be commensurate with the level of assurance required. It is widely-understood that the highest levels of assurance require a formal mathematical analysis of the system and its properties. However, this can be quite difficult to achieve in practice: current “proof-assistant” technology does not seem to have the appropriate structures to flexibly support large-scale mathematics, let alone engineering. The underlying problem seems to be a lack of flexibility in language support at the core of the tools, leading to an inability to support the typical elision and abstraction in engineering developments (of time, uncertainty, probability) in the consequent computational models.
We are seeking collaborative research proposals that can guide and shape the development of the next generation of formal methods tools capable of attacking such large-scale problems as arise in verifying safety and security in Defence systems. The development of assurance for large scale problems will need to leverage engineering notions such as modularisation, composition/refinement and re-use, and machine support is essential to deal consistently with the complexities that arise. We are interested in applying such ideas at the most fundamental levels: starting with the language underlying the tool, computational/reasoning structures, and the ability to translate between them.
One project of current interest is to utilise theory morphisms to ensure consistency for system-modelling development in a rich language such as Isabelle/ZF which, for particular system instances, throws proof obligations to a tightly-controlled context within Isabelle/HOL. In this way it is envisaged that a complete system design and implementation model can be developed in HOL, which has a well-structured and easily understood presentation at the ZF level.
Preference is for proposals that exhibit a long-term vision, coupled with tangible milestone outputs in the first 12 months.
This opportunity is open to all registered Australian Universities and Australian Publicly Funded Research Agencies.
- Successful applicants must be able to meet the milestones and timelines outlined in their submission.
- Successful applicants must enter into a Data61 University Collaboration Agreement.
- Successful applicants will enter into the appropriate contracting arrangement within 3 weeks of announcement.
Terms and conditions
Proposals submitted will be assessed equally on the following criteria:
- Alignment to Defence strategy and the project priorities articulated in this document
- Future science criticality
- Collaboration depth (e.g. Collaboration with DST staff, Data61 staff, other universities, an industry partner, etc.)
- Delivery of outcomes (e.g. the ability of the proposal to deliver the agreed outcomes and milestones).
- Game changing potential to Defence
Please limit submissions to no more than 2000 words. Ensure that all contact details, current and potential DST, Data61 collaborators and/or research partner details are on a separate page/covering sheet. The proposals will be de-identified during the selection process to eliminate any potential conflicts of interest.
Defence and Data61 reserves the right to fund all, some or none of the proposals received under this Call for Applications.
Contracts and Intellectual Property
Successful applicants will be required to enter into a Data61 University Collaboration Agreement and a subsidiary Collaborative Research Project Agreement with Data61 in order to access project funding. Data61 will enter into contracts with the lead party in each proposal.
Any IP generated as part of the projects will vest in Data61 unless otherwise agreed, and Defence will receive a license for Commonwealth purposes only.
Any Commonwealth funding contributed to the projects will be paid in accordance with successful completion of milestones and as negotiated by the parties. Where circumstances necessitate it is possible for a small payment to be made upon execution of the agreement and in accordance with Defence procurement rules.
How to apply
Please submit via the DST portal.
Proposals are to be submitted by 4.30pm Australian Eastern Daylight Time (AEDT), 15 August 2018. Only projects submitted via email to Cyber-NGTF@dst.defence.gov.au by the above deadline will be considered in this round.
For further information or assistance, please contact: