ABSTRACT. An obstacle to apply formal specification techniques to industrial projects is that stakeholders with little engineering background may experience difficulty to comprehend the specification. Forming a common understanding of a specification is indeed essential in software development because a specification is consulted by many kinds of stakeholders, including those who do not necessarily have an engineering background. This paper introduces ViennaDoc, a specification documentation tool that interleaves animation of a formal specification into informal texts written using natural language. ViennaDoc helps readers to understand the behaviour of the specified system by providing opportunities to verify their understanding by executing the specification in the context of the informal explanation. ViennaDoc also helps maintainers of the specification by enabling unit testing that asserts equality between values embedded in the informal specification with formal expressions.

ABSTRACT. The popularity of Eclipse, which Overture is based on, is in rapid decline. According to RebelLabs' most recent developer productivity report, IntelliJ exceeds Eclipse by 21% as the IDE of choice for Java developers. Although the popularity of IDEs varies over time, it would aid in the adoption of Overture if its core features were made available for other IDEs, as suggested by Fraser at the 16th Overture workshop. However, migrating language analysis components to a different IDE is a demanding task that (1) may require reimplementing these components to conform to the ecosystem of the targeted IDE and (2) entails writing code to expose these features to the users. To improve this situation, we report on lessons learned from migrating some of Overture's core features to a different IDE and discuss to which extent this is possible without having to reimplement everything from scratch. As part of this, we have developed Emacs packages for writing and analysing VDM specifications. These packages interact with Overture's command-line interface to create an IDE-like experience in Emacs. We estimate the efforts needed to develop these packages, and propose a way forward, based on the Language Server Protocol, that will further aid in the adoption of Overture.

ABSTRACT. The INTO-CPS Application is a common interface used to access and manipulate different model-based artefacts produced by the INTO-CPS tool chain during the model-based development of a Cyber-Physical System. The application has been previously developed during the INTO-CPS project. It uses web-technologies on top of the Electron platform, and it requires a local installation and configuration on each user desktop. In this paper, we present a cloud-based version of the developed INTO-CPS Application while researching the potential of cloud technologies to support the INTO-CPS tool chain environment. The proposed application has the advantage that no configuration or installation on the local desktop is needed. It makes full usage of the cloud resource management, and its architecture allows for a desktop version, maintaining the current local approach.

ABSTRACT. The INTO-CPS Application is a common interface used to access different artefacts in the development of a Cyber-Physical System (CPS) making use of a collection of tools centred around Functional Mockup Interface (FMI). For the configuration of the composition of Functional Mockup Units (FMUs) the application currently imports this information from a SysML model made using the Modelio tool. The contribution presented in this paper is the addition of a graphical editor to the application which eliminates the need of external tools. Additionally, this editor extends the existing functionality by allowing several types of semantic adaptations to be applied to one or more FMUs. Furthermore the paper defines how these concepts can be represented under the recently published System Structure and Parameterization (SSP) standard.

ABSTRACT. In order to ensure that co-simulation of Cyber-Physical Systems (CPSs) can be more streamlined a de-facto standard called the Functional Mockup Interface (FMI) has been defined. In FMI this is organised as a collection of Functional Mockup Units (FMUs) and the requirements for these is described in the FMI standard. The contribution presented in this paper is an initial formalisation of these requirements using the VDM Specification Language. Interestingly it looks like the standard contains a number of constraints that are not considered by many of the tools that are able to produce such FMUs.

ABSTRACT. Definitions of cyber-physical systems (CPSs) often include humans within the system boundary, however design techniques often focus on the technical aspects and ignore this important part of the system. Multi-modelling and co-simulation offer a way to bring together models from different disciplines together to capture better the behavious of overal system. In this paper we present some initial results of incorporating ergonomic models of human behaviours within a cyber-physical multi-model. We present two case studies, from the autonomous aircraft and railway sectors, including initial experiments and discussion of future potential.