UKRI Trustworthy Autonomous Systems Node in Verifiability

点击翻译按钮获取中文摘要

Autonomous systems promise to improve our lives; driverless trains and robotic cleaners are examples of autonomous systems that are already among us and work well within confined environments. It is time we work to ensure developers can design trustworthy autonomous systems for dynamic environments and provide evidence of their trustworthiness.Due to the complexity of autonomous systems, typically involving AIcomponents, low-level hardware control, and sophisticated interactions withhumans and the uncertain environment, evidence of any nature requires efforts from avariety of disciplines. To tackle this challenge, we gathered consortium ofexperts on AI, robotics, human-computer interaction, systems and softwareengineering, and testing. Together, we will establish the foundations andtechniques for verification of properties of autonomous systems to informdesigns, provide evidence of key properties, and guide monitoringafter deployment.Currently, verifiability is hampered by several issues: difficulties tounderstand how evidence provided by techniques that focus on individualaspects of a system (control engineering, AI, or humaninteraction, for example) compose to provide evidence for the system aswhole; difficulties of communication between stakeholders that use differentlanguages and practices in their disciplines; difficulties in dealing withadvanced concepts in AI, control and hardware design, software for criticalsystems; and others. As a consequence, autonomous systems are often developedusing advanced engineering techniques, but outdated approaches toverification.We propose a creative programme of work that will enable fundamental changesto the current state of the art and of practice. We will define amathematical framework that enables a common understanding of the diversepractices and concepts involved in verification of autonomy. Our frameworkwill provide the mathematical underpinning, required by any engineeringeffort, to accommodate the notations used by the various disciplines. Withthis common understanding, we will justify translations between languages,compositions of artefacts (engineering models, tests, simulations, and so on)defined in different languages, and system-level inferences fromverifications of components.With such a rich foundation and wealth of results, we willtransform the state of practice. Currently, developers build systems fromscratch, or reusing components without any evidence of theiroperational conditions. Resulting systems are deployed in constrainedconditions (reduced speed or contained environment, for example) or offeredfor deployment at the user's own risk. Instead, we envisage the futureavailability of a store of verified autonomous systems and components.In such a future, in the store, users will find not just systemimplementations, but also evidence of their operational conditions andexpected behaviour (engineering models, mathematical results, tests, and soon). When a developer checks in a product, the store will require all theseartefacts, described in well understood languages, and will automaticallyverify the evidence of trustworthiness. Developers will also be able to checkin components for other developers; equally, they will be accompanied byevidence required to permit confidence in their use.In this changed world, users will buy applications with clear guarantees oftheir operational requirements and profile. Users will also be able to askfor verification of adequacy for customised platforms and environment, forexample. Verification is no longer an issue.Working with the EPSRC TAS Hub and other nodes, and our extensive range ofacademic and industrial partners, we will collaborate to ensure that thenotations, verification techniques, and properties, that we consider,contribute to our common agenda to bring autonomy to our everyday lives.