Event-B is a well known methodology for the verified design and development of systems that can be characterised as discrete transition systems. Hybrid Event-B is a conservative extension that interleaves the discrete transitions of Event-B (assumed to be temporally isolated) with episodes of continuously varying state change. While a single Hybrid Event-B machine is sufficient for applications with a single locus of control, it will not do for autonomous systems, which have several loci of control by default. Multi-machine Hybrid Event-B is designed to allow the specification of systems with several loci of control. The formalism is succinctly surveyed, pointing out the subtle semantic issues involved. The multi-machine formalism is then used to specify a relatively simple incident response system, involving a controller, two drones and three responders, working in a partly coordinated and partly independent fashion to manage a putative hazardous scenario.

Trust is a crucial component in collaborative multiagent systems (MAS) involving humans and autonomous AI agents. Rather than assuming trust based on past system behaviours, it is important to formally verify trust by modelling the current state and capabilities of agents. We argue for verifying actual trust relations based on agents abilities to deliver intended outcomes in specific contexts. To enable reasoning about different notions of trust, we propose using the refinement-based formal method Event-B. Refinement allows progressively introducing new aspects of trust from abstract to concrete models incorporating knowledge and runtime states. We demonstrate modelling three trust concepts and verifying associated trust properties in MAS. The formal, correctness-by-construction approach allows to deduce guarantees about trustworthy autonomy in human-AI partnerships. Overall, our contribution facilitates rigorous verification of trust in multiagent systems.

Autonomous Systems (AS) like Humanoid Robots, Autonomous Vehicles, or Unmanned Aerial Vehicles are becoming increasingly complex and need to interact with dynamic environments and with each other. For this reason, robots require tools to enable advanced perception and understanding of the environment, or capabilities to operate in complex situations. Artificial Intelligence is extending the capability of perception and action of the agents and allows robots to operate in environments not suitable for robots just a few years ago. In most common scenarios the complexity of the environment requires to the robot to have different skills, the capability of different actions, and hence also a certain degree of reasoning and understanding of which action to take and when. A relevant example could be an urban road, with car, pedestrian, and signals.

Nowadays, it is well accepted that formal ontologies are commonly used as support for the axiomatisation of the knowledge describing a domain of interest. In particular, for domains in the engineering area where concepts are well mastered by the different stakeholders, ontologies play a major role for knowledge exchange and heterogeneity reduction. Meanwhile, we observe that defining a formal framework for integrating both ontologies represented by knowledge models and design models of particular systems did not draw the attention of many researchers in system engineering. Approaches like those of [3][4][5][7][9][12] supporting the integration of both ontologies and design models contribute to strengthen these design models by offering the capability to design models to borrow knowledge from ontologies, using a particular annotation relationship. As a consequence, the design models are enriched and strengthened with axioms, theorems or invariants issued from the used ontologies. This paper presents a summary of the work achieved in the context of the French ANR IMPEX research project. Ontologies are formalised as theories with axioms, theorems and reasoning rules. Event-B [1] has been chosen as the ground formal modelling technique for all our developments.

Refinement is a powerful mechanism for mastering the complexities that arise when formally modelling systems. Refinement also brings with it additional proof obligations -- requiring a developer to discover properties relating to their design decisions. With the goal of reducing this burden, we have investigated how a general purpose theory formation tool, HR, can be used to automate the discovery of such properties within the context of Event-B. Here we develop a heuristic approach to the automatic discovery of invariants and report upon a series of experiments that we undertook in order to evaluate our approach. The set of heuristics developed provides systematic guidance in tailoring HR for a given Event-B development. These heuristics are based upon proof-failure analysis, and have given rise to some promising results.