This paper presents a comprehensive Digital Twin (DT) tutorial using the case study of an incubator system designed for tempeh fermentation (a traditional Indonesian soy product). The study explores the development, calibration, and validation of models based on thermodynamics, offering insight into how DTs can enhance control and monitoring. Key DT services such as monitoring, decision support, and reconfiguration are implemented and evaluated. The tutorial demonstrates the potential of DTs in optimizing real-time systems while ensuring operational consistency.

This paper presents a formal modelling approach for BeliefDesire-Intention (BDI) agents using Isabelle/HOL and Z-Machines. The BDI architecture is widely used for modelling intelligent agents, where agents possess beliefs about the environment, desires or goals to achieve, and intentions to execute plans for goal attainment. The paper introduces a general-purpose model of the BDI architecture using Z-Machines. The modelling framework includes specifications for beliefs, actions, rules, plans, pattern matching, and rule applications. The proposed model can be used to formally verify BDI agents' behaviour using Hoare Logic and Isabelle/Z-Machines. This framework then contributes to advancing formal modelling and verification of agent-based systems, showing how we can integrate automated reasoning to establish invariant properties of agents with compositional techniques to prove more significant properties of BDI systems. We demonstrate the effectiveness of our approach through a case study of a nuclear inspector robot, showing how we can verify invariants and uncover bugs in the system's behaviour.

Systems that adapt to their environment or change based on new requirements pose challenges for runtime verification. Complexity is increased when the system needs to retain its internal state and continue monitoring while also updating properties or adding new ones during runtime. In this work, we propose DynSRV, a Stream Runtime Verification language that allows for dynamic updates of properties. A core benefit of this language is its capability to update properties at runtime without requiring a restart of the monitor, maintaining the internal state of the remaining properties. We formalise the semantics of our core primitives and demonstrate design patterns for allowing adaptations under certain constraints. Finally, we present an implementation of DynSRV and describe three memory strategies that balance memory usage and the ability to resolve dynamically added properties depending on historical data.

It is often the case that a robot must adapt to unexpected changes in its environment. It is, however, important that these changes can be demonstrated to maintain the safe operation of the robot. The adaptive systems community has developed the MAPE-K pattern as a widely recognised conceptual architecture. We propose extending MAPE-K to incorporate runtime verification, resulting in an architecture we call MAPLE-K. In this paper, we capture and formalise both the MAPE-K and MAPLE-K architectures using a domain-specific language. Additionally, we provide support for translation from architectural models to software models and code to facilitate the deployment of verified applications. MAPE-K is rarely maintained at the implementation level, but our work ensures traceability between the code and its design, enabling the use of architectural information to verify the correctness of the software.

Autonomous Systems (AS) enable systems to adapt to drastic and unprecedented environmental changes, a capability that can be enhanced through the utilization of Digital Twins (DTs). However, the additional capabilities of AS come at the cost of explainability, as the expanding adaptation space complicates the reasoning about the system's behavior. For certain types of systems, it is crucial to ensure that specific properties are upheld despite the system's autonomous behavior. To facilitate the monitoring of these properties, we propose the use of Runtime Verification (RV). This tutorial demonstrates the integration of RV tools into the Digital Twins as a Service (DTaaS) platform to monitor and verify the behavior of AS in real-time. By exploring various methods to incorporate RV tools within a DT context, the tutorial aims to advance the application of RV technologies in autonomic computing and self-adaptive system design. Specifically, we demonstrate how the behavior of a self-configuring DT can be verified utilizing RV. This is accomplished through the DTaaS platform, which supports seamless deployment of DT-based AS.

Digital twin is a technology that facilitates a real-time coupling of a cyber-physical system and its virtual representation. The technology is applicable to a variety of domains and facilitates more intelligent and dependable system design and operation, but it relies heavily on the existence of digital models that can be depended upon. In realistic systems, there is no single monolithic digital model of the system. Instead, the system is broken into subsystems, with models exported from different tools corresponding to each subsystem. In this paper, we focus on techniques that can be used for a black-box model, such as the ones implementing the Functional Mock-up Interface (FMI) standard, formal analysis, and verification. We propose two techniques for simulation-based reachability analysis of models. The first one is based on system dynamics, while the second one utilizes dynamic sensitivity analysis to improve the quality of the results. Our techniques employ simulations to obtain the model's sensitivity with respect to the initial state (or model's Lipschitz constant) which is then used to compute reachable states of the system. The approaches also provide probabilistic guarantees on the accuracy of the computed reachable sets that are based on simulations. Each technique requires different levels of information about the black-box system, allowing the readers to select the best technique according to the capabilities of the models. The validation experiments have demonstrated that our proposed algorithms compute accurate reachable sets of stable and unstable linear systems. The approach based on dynamic sensitivity provides an accurate and, with respect to system dimensions, more scalable approach, while the sampling-based method allows a flexible trade-off between accuracy and runtime cost. The validation results also show that our approaches are promising even when applied to nonlinear systems, especially, when applied to larger and more complex systems. The reproducibility package with code and data can be found at https://github.com/twright/FMI-Reachability-Reproducibility.

The bond-calculus is a language for modelling interactions between continuous populations of biomolecular agents. The calculus combines process-algebra descriptions of individual agent behaviour with affinity patterns, which can specify a wide variety of patterns of interactions between the sites of different agents. These affinity patterns extend binary molecular affinities to multiway reactions, general kinetic laws, and cooperative interactions. In this paper we explore bond-calculus modelling of gene regulation at both the molecular and network levels. At the molecular level, we show how affinity patterns can succinctly describe the λ-switch, a prototypical example of cooperative regulation. Moving to the network level, we develop a general model of gene regulatory networks using affinity patterns and an expanded Hill kinetic law. We illustrate the approach with a specific example: the complex plant circadian clock. We analyse these models via the bond-calculus's differential equation and stochastic semantics, and validate our results against existing models from the literature.

Signal Temporal Logic monitoring over numerical simulation traces has emerged as an effective approach to approximate verification of continuous and hybrid systems. In this paper we explore an exact verification procedure for STL properties based on monitoring verified traces in the form of Taylor model flowpipes as produced by the Flow* verified integrator. We explore how tight integration with Flow*’s symbolic flowpipe representation can lead to more precise and more efficient monitoring. We then show how the performance of monitoring can be increased substantially by introducing masks, a property-directed refinement of our method which restricts flowpipe monitoring to the time regions relevant to the overall truth of a complex proposition. Finally, we apply our implementation of these methods to verifying properties of a challenging continuous system, evaluating the impact of each aspect of our procedure on monitoring performance.

We present the bond-calculus, a process algebra for modelling biological and chemical systems featuring nonlinear dynamics, multiway interactions, and dynamic bonding of agents. Mathematical models based on differential equations have been instrumental in modelling and understanding the dynamics of biological systems. Quantitative process algebras aim to build higher level descriptions of biological systems, capturing the agents and interactions underlying their behaviour, and can be compiled down to a range of lower level mathematical models. The bond-calculus builds upon the work of Kwiatkowski, Banks, and Stark's continuous pi-calculus by adding a flexible multiway communication operation based on affinity patterns and general kinetic laws. We develop a compositional semantics based on vector fields and linear operators, which we use to define the time evolution of this system. This enables simulation and analysis via differential equation generation or stochastic simulation. Finally, we apply our framework to an existing biological model: Kuznetsov's classic model of tumour immune interactions.

We introduce a new mathematical framework for modelling biological systems at the molecular, cellular, and ecosystem level by combining process-algebra models that describe the behaviour of individual agents with an affinity network that specifies the dynamics of their interactions. We complement rule-based methods in focusing primarily on agent capabilities, from which reaction networks emerge as they interact. Our models generate conventional ODEs for behavioural simulation, but from a precise higher-level expression of the structures and mechanisms that give rise to that behaviour and are often left to informal description. This process-algebra approach is well-established in computer science for modelling networks of communicating agents by capturing not only the behaviour of individual agents but also their capability for mutual interaction. A. Regev and others have applied this to modelling a wide variety of biological systems, among which we build upon the work of Kwiatkowski, Banks, and Stark in linking process-algebra descriptions of agent interaction with differential equations that model their dynamics. We apply our framework to V. A. Kuznetsov's classic model of immune response to tumour growth, and present advances on previous work in capturing complex features including nonlinear interaction dynamics, n-party interactions, and dynamic binding of agents to form new agents. We show agent behaviour in isolation and when brought together, validating the observed dynamics of the model against our conceptual understanding of immune action.