We propose to directly synthesise formal verification formulas for multiple model checkers from naturallanguage requirements. Our approach utilises arrangements of logic-labelled finite-state machines (LLFSMs) to construct executable behaviour models. We can then prepare both the model (as a Kripke structure) and associated verification properties as input for each model checker, generating code in several programming languages as well, ensuring identical execution traces across all generated artefacts. We introduce a grammar-prompted Large Language Model (LLM) approach to obtain the Structured English Grammar (SEG) formula for the requirements, complementing the verification of these executable models without semantic gaps, using precisely the same traces in programming languages as well as model checkers. Our tools translate the full set of patterns of SEG formulas automatically to the specific syntax of five different model checkers, sparing developers from the steep learning curv e of mathematical formalisms for model checking, including the differences in syntax these model checkers require, even for the same temporal logic formalism, such as Linear Temporal Logic (LTL) or Computation Tree Logic (CTL). This work significantly reduces barriers to the adoption of formal methods, by enabling developers to work with familiar finite-state machine notation and natural language requirements while attaining formally verified properties and taking advantage of the particular, individual strengths of multiple model checkers.

This work proposes a deep learning (DL) architecture for estimating full-field deformation maps from ground-based complex radar data. Unlike existing methods that focus on estimating deformation time series at selected points, the proposed model directly estimates the entire deformation map from a single-frame complex radar observation. This capability enables faster, spatially comprehensive monitoring, which is crucial for real-time early warning systems (EWSs) in Internet of Things (IoT)-enabled environments. The primary input to the model is a 2-channel matrix formed by the real and imaginary components of the complex radar data. We propose a dual cross-attentive recurrent U-Net architecture (DCRU-Net) consisting of two networks trained simultaneously. The two networks, a primary and an auxiliary network, are based on long short-term memory (LSTM) units arranged in a U-Net architecture, where the model inputs are spatially restructured into sequences, enabling the model to learn deformation-related phase variations across the scene rather than modeling temporal dependencies as in conventional approaches. The primary network processes the 2-channel complex radar data, which is the leading network of the model. In contrast, the auxiliary network is guided by the amplitude dispersion index (ADI) to emphasize coherent scattering regions during training. A cross-attention mechanism enables interaction between the two networks, allowing the auxiliary network to guide the primary network toward physically meaningful regions and suppress clutter. The motivation behind this architecture is to predict the main features of the deformation maps while minimizing the impact of slight variations, which can result in clutter-induced distortions. The model is evaluated against benchmark methods, and the results demonstrate that our model outperforms existing methods and has better alignment with the ideal deformation maps, showing its potential for real-world radar applications.

Formally verifiable, executable models allow the high-level design, implementation, execution, and validation of reliable systems. But, unbounded complexity, semantic gaps, and combinatorial state explosion have drastically reduced the use of model-driven software engineering for even moderately complex real-time systems. We introduce a new solution that enables high level, executable models of decomposable real-time systems. Our novel approach allows verification in both the time domain and the value domain. We show that through 1) the use of a static, worst-case execution time, and 2) our time-triggered deterministic scheduling of arrangements of logic-labelled finite-state machines (LLFSMs), we can create succinct Kripke structures that are fit for formal verification, including verification of timing properties. We leap further and enable parallel, non-preemptive scheduling of LLFSMs where verification is feasible as the faithful Kripke structure has bounded size. We evaluate our approach through a case study where we fully apply a model-driven approach to a hard time-critical system of parallel sonar sensors.

How can there be Human-In-the-Loop-Learning (HILL) if datasets aimed at building classifiers have ever more dimensions? We make two contributions. First, we examine the few early results on the effectiveness of HILL for building autonomous classifiers and report on our own experiment that validates the merits of HILL. Second, we introduce a HILL system (by using parallel coordinates) for learning of decision tree classifiers (DTCs). DTCs importantly emphasise the relevance of attributes and enable attribute selection, and therefore are appreciated for their transparency. The proposed system addresses a number of the shortcomings of the many HILL systems and allows for easy exploration of datasets. In particular, we incorporate parallel coordinates effectively in our tool for visualisation of high dimensional datasets. We can not only focus the learning on the accuracy of classifiers, but we can enhance performance in other important factors such as system's interpretability and the ability to gain insight into datasets. Finally, we show the advantages of our HILL system in the application area of mobile robotics using the case study of image segmentation in robotic soccer.

For the UML, state charts are by far the most used modelling tools, both to communicate behaviour and to produce executable models. We investigate the inherent asymmetry of On-Entry and On-Exit Actions in UML Statecharts. We show first that the apparently simple and symmetric rules for handling the sequencing of On-Entry and On-Exit actions are hard to fully comprehend and apply effectively by software developers. Second, defining a semantics that results in executable models for applications such as reactive-systems and real-time systems is very delicate. Third, formal verification can be hampered because the semantics results in a combinatorial explosion of states. We evaluate the understandability of the semantics by taking out experiments with various tasks comprising sample UML Statechart and logic-labelled finite state machines (LLFSMs). Several experiments with software developers enable us to dissect how issues of understandability of state diagrams relate to nesting or event-driven vs logic-labelled. Since logic-labelled finite state machines achieve model composition through a subsumption architecture (suspend/restart/resume) we propose a specific alternative semantics for logic-labelled finite state machines that is suitable for robotic and embedded systems.

Logic-labeled Finite-State Machines (LLFSMs) are Communicating Extended Finite State Machines that execute concurrently but with a predefined sequential schedule. This capacity has enabled effective formal verification. Moreover, LLFSMs are very powerful tools for Model-Driven Software Engineering of the behaviour of robotic and embedded systems. Although existing schedulers are capable of executing several instances of the same model, the challenge is to provide mechanisms for creating parameterised models akin to function calls. Since recent task planning algorithms can synthesise behaviours as LLFSMs with parameters and recursion, it becomes necessary to have a useful operational tool that produces compiled executables for such behaviours. Moreover, parameterisation allows replication of generic system components, reducing overall design complexity. We produce safe mechanisms to set actual and formal parameters for multiple, concurrent instances of the same behaviour. We achieve the parameterisation of behaviour models analogous to a procedural abstraction and discuss its advantages and disadvantages on formal verification.

We show an architecture that enables runtime verification. Runtime verification focusses on the design of formal languages for the specification of properties that must hold during runtime. In this paper, we take matters one step further and describe a uniform modelling and development paradigm for software systems that can monitor the quality of software systems as they execute, set-up, tear-down and enforce quality behaviour on the fly. Our paradigm for modelling behaviour enables efficient execution, validation, simulation, and runtimeverification. The models are executable and efficient because they are compiled (not interpreted). Moreover, they can be developed using test-driven development, where tests are models derived from requirements. We illustrate the approach with case studies from robotics and embedded systems.

Engineering real-time communication protocols is a complex task, particularly in the safety-critical domain. Current protocols exhibit a strong tradeoff between flexibility and the ability to detect and handle faults in a deterministic way. Model-driven engineering promises a high level design of verifiable and directly runnable implementations. Arrangements of logic-labelled finite-state machines (LLFSMs) allow the implementation of complex system behaviours at a high level through a subsumption architecture with clear execution semantics. Here, we show that the ability of LLFSMs to handle elaborate hierarchical module interactions can be utilised towards the implementation of testable, safety-critical real-time communication protocols. We present an efficient implementation and evaluation of INCUS, a time-triggered protocol for safety-critical real-time communication that transcends the rigidity imposed by existing real-time communication systems through the use of a high-level subs umption architecture.

There are many areas where software components must interact witch each other and where middleware provides the appropriate benefits of robustness, decoupling, and modularisation. However, there is a potential performance overhead that, for autonomous robotic and embedded systems, may be critical. Proposals for robotic middleware continue to emerge, but surprisingly, they repeatedly follow the publish-subscriber model. There are several disadvantages to the push paradigm of the publisher-subscriber approach; in particular, its implication of a closer coupling where the subscriber must be active and able to keep up with the pace of events. We propose an alternative pull model, where consumers of messages handle information at their own time. We show that our proposal aligns with fundamental, time-triggered design principles, and produces simple module communication that reduces thread management and can enable rapid prototyping, validation, and formal verification.

We propose vectors of finite-state machines whose transitions are labeled by formulas of a common-sense logic as the modeling tool for embedded systems software. We have previously shown that this methodology is very efficient in producing succinct and clear models (e.g., in contrast to plain finite-state machines, Petri nets, or Behavior Trees). We show that we can capture requirements precisely and that we can simulate and validate the models. We can, therefore, directly apply Model-Driven Engineering and deploy the models into software for diverse platforms with full tractability of requirements. Moreover, the sequential semantics of our vector of finite-state machines enables model-checking, formally establishing the correctness of the model. Finally, our approach facilitates systematic Failure Modes and Effects Analysis (FMEA) for diverse target platforms. We demonstrate the effectiveness of our methodology with several examples widely discussed in the software engineering literature and compare this with other approaches, showing that we can prove more properties, and that some claims about verification in such approaches have been exaggerated or are incomplete.

In this paper we investigate how combining two types of modelling languages will increase their expressive power. The Behavior Tree method and non-monotonic logic will be integrated.