Automated model repair techniques enable machines to synthesise patches that ensure models meet given requirements. B-repair, which is an existing model repair approach, assists users in repairing erroneous models in the B formal method, but repairing large models is inefficient due to successive applications of repair. In this work, we improve the performance of B-repair using simultaneous modifications, repair refactoring, and better classifiers. The simultaneous modifications can eliminate multiple invariant violations at a time so the average time to repair each fault can be reduced. Further, the modifications can be refactored to reduce the length of repair. The purpose of using better classifiers is to perform more accurate and general repairs and avoid inefficient brute-force searches. We conducted an empirical study to demonstrate that the improved implementation leads to the entire model process achieving higher accuracy, generality, and efficiency.

This work follow the verification as planning paradigm and propose to use model-checking techniques to solve planning and goal reasoning problems for autonomous systems with high-degree of assurance. It presents a novel modelling framework — Goal Task Network (GTN) that encompass both goal reasoning and planning under a unified formal description that enables the use of assurance tools. The paper provides a systematic method that highlights how an industrial model checker (PAT) can be used to solve goal reasoning and planning problems modelled by GTNs. Further, this paper also introduces the design of an automated system framework for Goal Reasoning And Verification for Independent Trusted Autonomous Systems (GRAVITAS). The proposed framework is demonstrated in an experiment that simulates a survey mission performed by the REMUS-100 autonomous underwater vehicle.

Reflection is a notion that naturally emerges from philosophy, mathematics, and sciences. In short, reflection is the ability of an entity to alter its own behaviour. This paper suggests that reflection is crucial to the development of complex and trustworthy software systems. We present RL, a reflective computational model that aims to support the development of a large-scale framework for modelling and manipulating structured data. We give the formal semantics for this computational model. We also share preliminary work on a proof-of-concept implementation of RL and discuss future work.

Summary Computational simulation is becoming increasingly important in numerous research fields. Depending on the modeled system, several methods such as differential equations or Monte‐Carlo simulations may be used to represent the system behavior. The amount of computation and memory needed to run a simulation depends on its size and precision, and large simulations usually lead to long runs, thus requiring to adapt the model to a parallel system. Complex systems are often simulated using multi‐agent systems (MASs). While linear system based models benefit from a large set of tools to take advantage of parallel resources, multi‐agent systems suffer from a lack of platforms that ease the use of such resources. In this paper, we propose the use of Nested Graphs for a new modeling approach that allows the design of large, complex, and multi‐scale multi‐agent models, which can efficiently be distributed on parallel resources. Nested Graphs are formally defined and are illustrated on the well‐known predator‐prey model. We also introduce PDMAS (parallel and distributed multi‐agent system): a platform that implements the Nested Graph modeling approach to ease the distribution of multi‐agent models on High Performance Computing clusters. Performance results are presented to validate the efficiency of the resulting models.

Simulation has become an indispensable tool for researchers to explore systems without having recourse to real experiments. In this context multi-agent systems are often used to model and simulate complex systems. Depending on the characteristics of the modelled system, methods used to represent the system may vary. Whatever the modelling techniques used, increasing the size and the precision of a model increases the amount of computation needed, requiring the use of parallel systems when it becomes too large. Usually, to efficiently run on parallel resources, the model must be adapted to be distributed. In this paper, we propose a new modelling approach, based on nested graphs, that allows the design of large, complex and multi-scale multi-agent models which can be efficiently distributed on parallel resources. A PDMAS (Parallel and Distributed Multi-Agent Platform) that supports this approach and efficiently run parallel multi-agent models is introduced.