Abstract Digital twins couple computational models with physical systems to enable services such as predictive reasoning and runtime analysis that support decision–making for maintenance, optimisation and system evolution. They create a technically rich setting for applying formal methods throughout the system lifecycle beyond design-time. This tutorial introduces the elements of digital twin technology, identifying emerging opportunities for formal techniques, including the verification of evolving models under uncertainty, integration of heterogeneous models and rigorous composition of digital twin-enabled systems.

A building occupant’s experiences are not passive responses to environmental stimuli, but are the results of multifaceted, prolonged interactions between people and space. We present a framework and prototype software tool for logically reasoning about occupant perception and behaviour in the context of dynamic aspects of buildings in operation, based on qualitative deductive rules. In particular, we focus on the co-presence of different user groups and the resulting impact on perceptual and functional affordances of spatial layouts by utilising the concept of spatial artefacts. As a first proof of concept of our approach, we have implemented a prototype crowd analysis software tool in our new system ASP4BIM, developed specifically to support architectural design reasoning in the context of public-facing buildings with complex signage systems and diverse intended user groups. We evaluate our prototype on the Urban Sciences Building at Newcastle University, a large, state-of-the-art living laboratory and multipurpose academic building. Our findings are that the ASP4BIM-based prototype supports a range of novel query services for formally analysing the impacts of crowds on pedestrians that are logically derived through the use of qualitative deductive rules, that complements other powerful crowd analysis approaches such as agent-based simulation.

Advances in sensing, communications and data analytics have made it possible to construct virtual replicas of Cyber-Physical Systems (CPSs). Such replicas, known as digital twins, can in principle inform decision making during operation and evolution of the systems they model. This short paper introduces the ISoLA 2020/21 series of papers on the technology and practice of engineering digital twins for CPSs. The focus is on the relationship between model-based design, machine learning, digital twins and CPSs.

Businesses, particularly small and medium-sized enterprises, aiming to start up in Model-Based Design (MBD) face difficult choices from a wide range of methods, notations and tools before making the significant investments in planning, procurement and training necessary to deploy new approaches successfully. In the development of Cyber-Physical Systems (CPSs) this is exacerbated by the diversity of formalisms covering computation, physical and human processes. In this paper, we propose the use of a cloud-enabled and open collaboration platform that allows businesses to offer models, tools and other assets, and permits others to access these on a pay-per-use basis as a means of lowering barriers to the adoption of MBD technology, and to promote experimentation in a sandbox environment.

No abstract available.

Cyber-Physical Systems (CPSs) [ 1 ] connect the real world to software systems through a network of sensors and actuators in which physical and logical components interact in complex ways. There is a diverse range of application domains [ 2 ], including health [ 3 ], energy [ 4 ], transport [ 5 ], autonomous vehicles [ 6 ] and robotics [ 7 ]; and many of these include safety critical requirements [ 8 ]. Such systems are, by definition, characterised by both discrete and continuous components. The development and verification processes must, therefore, incorporate and integrate discrete and continuous models. The development of techniques and tools to handle the correct design of CPSs has drawn the attention of many researchers. Continuous modelling approaches are usually based on a formal mathematical expression of the problem using dense reals and differential equations to model the behaviour of the studied hybrid system. Then, models are simulated in order to check required properties. Discrete modelling approaches rely on formal methods, based on abstraction, model-checking and theorem proving. There is much ongoing research concerned with how best to combine these approaches in a more coherent and pragmatic fashion, in order to support more rigorous and automated hybrid-design verification. It is also possible to combine different discrete-event and continuous-time models using a technique called co-simulation. This has been supported by different tools and the underlying foundation for this has been analysed. Thus, the track will also look into these areas as well as the industrial usage of this kind of technology.

This paper proposes a systematic model-based approach to the architectural description of faults and fault tolerance mechanisms in systems of systems (SoSs). The challenges of engineering dependable SoSs motivate a proposal for the view elements that would be needed to support a fault tolerance profile for SoSs using the Systems Modelling Language (SysML). The effectiveness of the approach is evaluated on a case study based on a real emergency response SoS. Results suggest that this is a promising approach, and that a comprehensive solution to the engineering of dependable SoSs requires that such a profile is linked to methods and tools for requirements elicitation, safety analysis, architectural design and formal verification.

The effective use of model-based formal methods in the development of complex embedded systems requires the integration of discrete-event models of controllers with continuous-time models of their environments. This paper proposes a new approach to the development of such combined models (co-models), in which an initial discrete-event model may include approximations of continuous-time behaviour that can subsequently be replaced by couplings to continuous-time models. An operational semantics of co-simulation allows the discrete and continuous models to run on their respective simulators and managed by a coordinating co-simulation engine. This permits the exploration of the composite co-model's behaviour in a range of operational scenarios. The approach has been realised using the Vienna Development Method (VDM) as the discrete-event formalism, and 20-sim as the continuous-time framework, and has been applied successfully to a case study based on the distributed controller for a personal transporter device.

Maintaining semantic consistency of data is a significant problem in distributed information systems, particularly those on which a business may depend. Our current work aims to use Event-B and the Rodin tools to support the specification and design of such systems in a way that integrates well into existing development processes. This paper presents Event-B patterns that may be used to represent recovery from time-bounded inconsistency and illustrates their use in a model derived from industrial applications.

Distributed information systems are critical to the functioning of many businesses; designing them to be dependable is a challenging but important task. We report our experience in using formal methods to enhance processes and tools for development of business information software based on service-oriented architectures. In our work, which takes place in an industrial setting, we focus on the configuration of middleware, verifying application-level requirements in the presence of faults. In pilot studies provided by SAP, we used the Event-B formalism and the open Rodin tools platform to prove properties of models of business protocols and expose weaknesses of certain middleware configurations with respect to particular protocols. We then extended the approach to use models automatically generated from diagrammatic design tools, opening the possibility of seamless integration with current development environments. Increased automation in the verification process, through domain-specific models and theories, is a goal for future work.

Abstract We describe the design and delivery of two courses that aim to develop skills of use to students in their subsequent professional practice, whether or not they apply formal methods directly. Both courses emphasise skills in model construction and analysis by testing rather than formal verification. The accessibility of the formalism is enhanced by the use of established notations (VDM-SL and VDM ++ ). Motivation is improved by using credible examples drawn from industrial projects, and by using an industrial-strength tool set. We present examples from the courses and discuss student evaluation and examination performance. We stress the need for exercises and tests to support the development of abstraction skills.

Dynamic coalitions are temporary alliances formed between agents in order to achieve specific business goals. Such coalitions can vary widely in architecture, scale, complexity and lifetime. Few techniques have so far emerged to assist in the analysis and design of coalitions. We apply formal model- oriented techniques to help structure the space of dynamic coalitions, with an emphasis on modelling information flow. A series of models is developed in VDM, each emphasising a different "dimension" of the space. These are used to characterise a new dynamic coalition architecture under development for the chemical engineering industry. Tool-supported analysis of this formal model has identified potential improvements in the coalition architecture.

The Vienna development method (VDM) is one of the longest established and best known formal methods. Recent developments in VDM have included its extension to support object-oriented design and concurrency in VDM++ and providing a capability for modelling real-time distributed systems. VDM is model-oriented - the formal language is used to construct a model of the system of interest, given in terms of data and functionality. In this paper, we draw on experience in developing the semantics and tool support for VDM, and in applying VDM technology in industry, to identify achievements and challenges in providing lightweight but effective formal methods.

No abstract available.