Page 8 - Sirius_Annual_Report_2021

Analysis of Complex Systems: Formal methods for executable design
Now a days industry is experiencing more and more the need for digitization and digital transformation. Supporting technologies to assist industry into such process needs to deal with complex systems. Characteristics of such systems are that they are usually very difficult to understand and analyse due to many interdependent processes happening at the same time. In the oil & gas domain, we can observe such systems in emergent supporting technologies such e.g., digital twins, big networks of heterogeneous autono- mous systems, parallel processing of big data, etc. Formal methods are mathematical approaches to support the rigorous specification, design, and verification of the development of digital systems. They are very powerful
to capture the behaviours and interactions of complex systems, helping with the understanding of what is currently happening and to further develop predictive and prescriptive analysis. Currently the use of Formal Methods is being more and more accepted in industry. This program use and research formal methods for system specifications and formal methods to describe, predict and prescribe the behaviours and interactions of system executions based on the analysis of models.
• Objective 1 Theoretical development:
Analysis of formal models can span from lightweight automated simulations to heavyweight complex non-automated verification techniques. We aim to explore the middle ground, which we call systematic model and multi-model exploration.
• Objective 2 Tool development:
Tool development (both back- and front- end) for the developed methods. Knowledge extraction, visualization, and fill gaps in industries/market are important for tool development.
In the past year, our research program has continue maturing the tools and methods developed in the group and has started to explore other application domains. We now detail some of these activities.
ABS - Abstract Behavioural Specification Language
Figure 1: Specification and Simulation of a physical model in ABS.
ABS1 (Abstract Behavioural Specification
Language) is a language for executable design. ABS is a method and language for modelling, analysing and simulating distributed timed, resource-aware systems.
In addition to supporting modelling of functional behaviour and distributed algorithms and systems, ABS supports the modelling of resource restrictions and resource management. It combines implementation-level specifications with verifiability, high-level design with executability, and formal semantics with practical usability. It is a concurrent, object-oriented, modelling language that features functional datatypes and supports model variability based on feature models and delta- oriented specifications. Deployment modelling can be based on high-level deployment models. The ABS system supports the modelling of resource-aware and resource- restricted systems and provides a range of techniques for model exploration and analysis, based on formal semantics.
ABS was designed to be easy to read and use by industrial programmers. It is an open-source2 research project that is used in teaching and research, including industrial innovation research at Sirius.
For the end user, the main features and application areas of ABS are:
• Discrete-Event Simulation of timed, resource-aware systems • Custom visualization of live simulation data
8 | SIRIUS ANNUAL REPORT 2021