1 Introduction

The use of controlled robots in the realm of the Internet of Things (IoT) has received significant research attention. According to the 2020 World Robotics Report published by the International Federation of Robotics (IFR), there are currently 2.7 million robots deployed in factories and warehouses worldwide, with 1.7 million in Asia, 580,000 in Europe and 389,000 in the Americas [1]. These robots are equipped with actions that enable control [2,3,4], as demonstrated by companies such as Amazon, Ocado and Exotec in the Economist issue [5]. They are equipped with arms that embed cameras and bar code readers to identify goods, while AI algorithms monitor their actions to manage pickup and item sorting efficiently.

Robots in networked systems can communicate with each other either directly in a decentralized system or through a master controller in a centralized system [6,7,8]. Decentralized collaborative robots are designed to execute cooperative missions [9,10,11], and the success of these missions depends on the quality of communication among the robots [12, 13] and their processing speed [14, 15]. However, decentralized robot deployment can be costly in terms of programming as much of the functionality and orders rely on embedded AI algorithms [16]. The use case scenario developed by Robotnik is essential to the success of the Brain-IoT project. The company produces robots that are capable of remote control and self-adaptation in warehouse environments (as shown in Fig. 1). To meet the needs of customers, Robotnik controls the robots from a centralized computer while managing their actions and orders. For further information on the robots and physical structures used, please refer to [17].

Fig. 1
figure 1

Robotnik robots movement in warehouse [17]

Full size image

Building complex systems at a high level of abstraction is an effective method for predicting system behaviour, as most implementation flaws stem from design imperfections, as mentioned by Taylor Armerding [18]. According to Crnkovic and Larsson [19], component-based design is the ideal paradigm, from a software architect’s perspective, for building a system while effectively segregating business logic into individual components. Moreover, this approach offers various ways of composing and coordinating these components. As a result, the incorporation of the component-based design paradigm prompts the usage of model-driven design (MDD) methodologies [20], especially in embedded systems and IoT [21]. MDD provides assistance in the development of model systems by offering abstract characterization support, with a focus on platform-agnostic implementation and execution [22]. The BRAIN-IoT framework offers the fundamental elements required to model IoT systems through a series of refinements. Designers first define the platform-independent model (PIM), which is then translated into one or more platform-specific models (PSM) based on the platform definition model (PDM).

The paper builds upon the research conducted in [23] and [24]. So, to guarantee the correctness of Robots Orchestration, certain requirements must be met. For example, if a cart is detected, the robot should lift it off the ground and transport it to the storage area. Robotnik provides the requirements that must be satisfied during experimentation within the warehouse. The BIPFootnote 1 language, which has been maintained at Verimag Lab for decades [25,26,27] and has been utilized in successful projects such as CPS4EUFootnote 2 and ERGO,Footnote 3 is the language we use to construct formal models. To ensure accuracy, the modelling and verification phases will be conducted at the PIM level. The BIP Statistical Model Checker (SMC) [28] enables us to perform both quantitative and qualitative analyses of requirements that have been formalized in temporal logic [29]. Once the requirements are met, a code is generated for the specific execution platform, followed by validation through simulation at the PSM level.

The paper’s structure is as follows: Sect. 2 provides a review of the existing literature on the deployment of robot fleets, while Sect. 3 details the methodology and architecture of the BRAIN-IoT framework. Section 4 presents a background of the BIP formalism, and Sect. 5 highlights model transformation and the Java code generator. Section 6 models the orchestration in the robots’ warehouse, including verification and validation. Finally, Sect. 7 concludes the paper.

2 Related Work

In this section, we delve into works related to the model-driven approach for orchestrating networked collaborative robots, utilizing formal methods and simulation techniques. Formal modelling and verification techniques have primarily been employed in robotic applications such as controllers, motion planning and fault detection [30]. Among the works in this direction, the work presented in [31] proposes a toolchain that utilizes a UML profile for designing models of human–robot collaboration (HRC). Then, a formal model is expressed in terms of metric temporal logic that specifies the concepts defined in the UML model. Transcoding tools are used to automate the development process of the designed task on the chosen infrastructure after requirements satisfaction is enabled by the Zot tool [32]. The toolchain has experimented on some realistic case studies. The approach is also applied for risk analysis [30] in collaborative robotic applications, and Zot formal verification tool is used to identify and mitigate hazardous situations associated with non-negligible risks. Guiochet [33] proposes a hazard identification approach of human–robot interactions. This approach combines the semiformal UML notation with HAZOP (Hazard Operability) to describe robot manufacturers’ scenarios using use case, sequence and state machine UML diagrams, and then identify hazards and analyse their risks based on HAZOP tables. It also produces a list of hazards, recommendations and hypotheses. Analysis tools are not detailed in the article but are mainly based on diagram animations using simulation. The authors in [34] utilize the Brahms language for formal modelling of an autonomous assistant robotic system. The Brahms model is then translated into the PROMELA language to verify safety requirements via the SPIN model checker [35]. Dixon et al. [36] apply the NuSMV model checker [37] to analyse the safety and trustworthiness of robot behaviours in a robotic assistant located in a typical domestic environment. This work aims to prove that given temporal properties are satisfied on all the possible behaviours of the system. Mohammed et al. [38] propose a framework for formal specification and verification of multi-robot systems behaviours using Hybrid Finite State Machines. The framework provides two views (concurrent and hierarchical) to optimize the verification and the constructed models. Walter et al.[39] present a methodology for specifying and verifying the functional properties of autonomous vehicles and robots. The method applies the theorem prover Isabelle for interactive formal proof and verification. As all theorem provers, the engine requires multiple assertions to perform verification compared to Model checking. In the study by Murray et al. [40], system properties are established through the co-verification of interconnected models using platform mappings. These mappings establish the relationship between the inputs and outputs of both software and hardware components, as well as their corresponding sensors and actuators. The software components are modelled in RoboChart [41], while the hardware components are modelled in Simulink. To verify the system, the authors utilized Simulink Design Verifier (SDV) [42] and FDR [43]. The system properties were expressed using the formalism of Communicating Sequential Processes (CSP) [44]. The study by Walter et al. [45] presents a custom domain-specific language (DSL) for modelling scenarios involving robot movement and human intervention, which also accounts for the stochastic nature of human fatigue. The model is further refined to a Network of Stochastic Hybrid Automata and analysed using UPPAAL [46] for statistical model checking. The formal model’s adherence to reality is thoroughly validated through experimental scenarios created in the field of healthcare service robotics. In their work, Chowdhary and Chattopadhyay [47] propose algorithms for robot orchestration in warehouse and factory-like environments. These improved algorithms incorporate obstacle avoidance and are validated for fault tolerance through various experiments. In their paper, Delgado et al. [48] propose a new approach called OROS, which optimizes the navigation and sensing of robots, as well as the use of infrastructure resources, to minimize the completion times of mission-critical tasks for 5 G-connected robots and for battery life extension.In their paper, Tahir et al. [49] demonstrate how formal verification using UPPAAL [46] can be applied to an autonomous firefighting robot system. To model the system, they designed a customized arena and a sensor-equipped robot that throws balls into boxes to simulate ejecting water at the fire location. Multiple properties, including safety and liveness, were identified and validated during the simulation to ensure the system met the necessary requirements.

Not only robots are orchestrated but also automatic trains within MDA vision. Baouya et al. [22] proposed model-driven approach (MDA) to model the AATC systems in AADL [50]. The workflow is based on three levels: the platform-independent model (PIM), the platform-dependent model (PDM) and the platform-specific model (PSM), which highlight different refinement levels. Formal verification targets the PIM level since the architecture is abstracted while the simulation is done after deployment at PDM. Moreover, the specification in AADL is partially mapped into PRISM language [51, 52] to perform safety assessment [52,53,54] due to the limitation of the PRISM model checker [55]. The BRAIN-IoT framework [56] encompasses a set of tools from system modelling to code generation. The modelling aspect of the system is performed using BIP [57], a language that offers greater expressivity in component–port–connector formalism with C/C++ constructs. The dedicated statistical model checker SMC-BIP [28] is capable of verifying BIP models through a dedicated engine. Unlike PRISM [55], NuSMV [37] and UPPAAL [46], SMC-BIP compiles models instead of storing them in memory, resulting in reasonable verification times [58]. Furthermore, the code generator is capable of validating specifications through simulation.

3 Modelling and verification artefact of BRAIN-IoT framework

Fig. 2
figure 2

Functional assurance using modelling and verification artefact of BRAIN-IoT framework

Full size image

The BRAIN-IoT modelling and verification artefact relies on model-driven development (MDD) principles [59]. The system view is structured into three distinct viewpoints: the platform-independent model (PIM), the platform description model (PDM) and the platform-specific model (PSM). The PIM contains the system functionality in component-oriented architecture. The PDM describes the software resources and the hardware platform, whereas the PSM describes the mapping of the software components to the hardware platform. The PSM view is not established until the functionality assurance is met. Figure 2 portrays the BRAIN-IoT modelling and verification artefact. The boxes represent the steps, and the edges show their relationship. Statistical model checker [60] accepts the BIP models defined at the PIM level to perform verification \(\textcircled {1}\). Suppose the requirements are satisfied with a certain probability level. In that case, the deployment is performed while Java code is generated with robots communication libraries to perform simulation \(\textcircled {2}\) using the tool developed in [61]. Finally, The generated code is refined to the OSGi Bundles. When the requirements are unmet, as mentioned with a red line in Fig. 2, the architect using the BRAIN-IoT modelling and verification artefact has to redesign the software view at the PIM level. Documentation pertaining to the Brain-IoT project and its framework can be found on the project’s website.Footnote 4 Table 1 provides a summary of the main project deliverables that were used in writing this article.

Table 1 BRAIN-IoT stemming deliverables relative to the article
Full size table

3.1 PIM

The PIM relies on the utilization of BIPFootnote 5 constructs that adhere to the component-oriented approach. Two types of components are identified: atomic and compound components. Components exchange through ports endowed with native (i.e. float, integer and Boolean) and complex data. BIP has been used in multiple projects [62,63,64], and a formal description related to BIP language and statistical model checker is detailed in Sect. 4.

3.2 PDM and PSM

Our methodology supports the description of the hardware and software within three views: the hardware platform (PDM), the software platform view and the architectural view.

3.2.1 Hardware platform

This paper describes the hardware platform at a high level of abstraction (Macro architecture) without a specific language to model it. The software platform interacts with the hardware through dedicated services, which are supported by the “sensinact” gateway.Footnote 6 The software platform offers IoT service functions such as discovery and look-up services. Within a BRAIN-IoT environment, sensiNact Management service is responsible for the Operational management and monitoring of specific devices via the sensiNact gateway’s [65]. Discovery is provided by the generic service discovery mechanisms that return the relevant device based on a set of properties to be matched. The look-up service returns information about one physical entity based on the device ID.

Fig. 3
figure 3

Federated architecture

Full size image

3.2.2 Software platform view

The software platform called BRAIN-IoT Fabric is based on Paremus Service FabricFootnote 7 which provides a distributed runtime infrastructure for dynamic behaviour expressed in a set of bundles. Each behaviour is a result of Java code generation from the high-level representation in BIP as portrayed in Fig. 2. Each Fabric interacts with one or multiple devices depending on the local or federated architecture as mentioned in Fig. 3. A Fabric is composed of one or more BRAIN-IoT nodes, representing bundles. The BRAIN-IoT Edge nodes are nodes that provide the connectivity for the software artefacts to communicate with robot devices. The Edge node is played by the Sensinact Gateway [65].

3.2.3 Architectural view

The Architectural view describes:

  • The environment into which the BRAIN-IoT Fabric will be deployed and

  • The dependencies that BRAIN-IoT Fabric has on the elements of the environment.

The BRAIN-IoT runtime architecture consists of four structural layers and is portrayed in Fig. 4:

Physical layer A set of physical computing resources within the physical environment to be managed (inux Servers and ROS Robots) is selected to run BRAIN-IoT nodes. A BRAIN-IoT Fabric may be a set of one or more physical resources; the more resources available, the more robust the BRAIN-IoT runtime becomes. To participate as a BRAIN-IoT node, the compute resource must be capable of running Java and OSGi framework.

Fabric layer To create a Service Fabric, a set of \(OSGi^{\hbox {TM}}\)/Java agents are installed upon the physical layer. BRAIN-IoT nodes are responsible for negotiation, installing/assembling, managing and monitoring software artefacts. The application is written in any Java language.

Systems layer A System is a distributed entity composed of a set of interrelated software components. Meanwhile, it contains the following mandatory BRAIN-IoT infrastructure software components: (1) a “Bundle Installer Service”(BIS) responsible for dynamically deploying a specified Smart Behaviour to its local environment, (2) a “Behaviour Management Service” (BMS) responsible for selecting the most appropriate Smart Behaviour from the Marketplace, (3) the “EventBus” substrate that allows asynchronous events to be exchanged between the software components within the same system and (4) the sensiNact node that is responsible for managing communication between federated entities, between smart behaviour and devices.

Smart Behaviours In response to environmental triggers, each BRAIN-IoT System is capable of dynamically deploying sets of interrelated Smart Behaviours. BRAIN-IoT Smart Behaviours communicate with each other via asynchronous events. A behaviour issues an event which is routed to local or remote endpoints that have registered interest in events of that type: i.e. other Smart Behaviours. If an event cannot be forwarded because no third party has a registered interest, then the Behaviour Management Service consumes the event. The BMS searches the nominated BRAIN-IoT repository for an appropriate Smart Behaviour, and if a candidate is found, the BMS instructs a selected Bundle Installer Service (BIS) (local or remote) to instal the selected Smart Behaviour.

Fig. 4
figure 4

BRAIN-IoT architecture view

Full size image

4 Background on BIP component formalism

In this section, we provide a background on the modelling and the specification formalism supported by BIP [28, 29, 57, 60].

Atomic components are elementary building blocks for BIP systems. They are described as labelled transition systems extended with variables. Transitions between states are labelled by ports. A transition is associated with a guard g and an update function Func(V), which are, respectively, a propositional logic formula and a computation defined over local variables V. eval(V) is a function that assigns values to variables V. An atomic component in BIP [28, 29, 57, 60] is formally defined as follows.

Definition 1

(Atomic Components) An atomic component B=\(\langle S, P, T, s_{0} \rangle \) is a labelled transition system, where:

  • \(S=Loc\times Eval(V)\) is a set of states where Loc is a set of component locations and \(V = \{v_{0},\ldots ,v_{n} \}\) is a set of local variables,

  • P a set of communication ports,

  • T is a set of transitions of the form (\(s,p,g,s'\)) where s, \(s' \in S\), \(p\in P\), \(g\in Eval(\vartheta )\) is a guard, and

  • \(s_{0}= \{\langle l_{0},X\rangle \} \in S\) is the initial state.

Syntactically, A BIP code (i.e. a Program) is composed of a set of “m” components (\(m>0\)) where the behaviour of each component is described as a set of statements that take the following form:

figure a

The BIP transition can be considered as . “p” is the port labelling the transition preceded by the keyword “” and forces components to synchronize and execute actions simultaneously in a lock-step fashion. The current location “l” is preceded by the keyword “”, and the next state “” is preceded by the keyword “”. The transition is enabled when the Boolean expression g evaluates to true within the construct “ ()”. Let \(\mathbb {D}\) be a finite universal domain. Given a set of variables \(\vartheta \), we define valuations for variables as functions \(\vartheta : V \rightarrow \mathbb {D}\) that associate each variable in V with a value in \(\mathbb {D}\). To express the evolution of the atomic component, we introduce a token concept as in activity diagrams [66]. So, initially, the initial state is marked using the keyword “” and formally expressed as follows:

figure i

where . Also, we express a BIP-triggered transition as an update command:

figure k

where and

Within the BIP atomic component, for a given valuation of variables, a transition can be executed if and only if its associated guard evaluates to true. Moreover, to deal with the system’s interoperability, BIP formalism provides mechanisms for harmonizing and coordinating components’ behaviours, namely priorities and connectors [28, 67]. The result of the interaction is a composition of synchronized components obtained by using the component composition operator \(\gamma \) presented in Definition 2.

Definition 2

(Composition) The composition of two atomic components denoted by \(\gamma (B_{1},B_{2})\) is a composite component \(B=\langle S, P, T, s_{0}\rangle \), where:

  • \( s_{1} \xrightarrow {p,g_{1}} s'_{1}\wedge s_{2} \xrightarrow {p,g_{2}} s'_{2} \) such that \( s_{1},s'_{1}\in S_{1}, \ s_{2},s'_{2}\in S_{2} \) where \(p \in P_{1} \cap P_{2} \wedge X_{1}\models g_{1} \wedge X_{2}\models g_{2}\),

The SMCFootnote 8 implements the main statistical model checking techniques, namely hypothesis testing [68] and probability estimation [69]. Queries/requirements to be verified using SMC-BIP [28] shall be expressed in PBLTL (Probabilistic Bounded Linear Temporal Logic). The syntax of the PBLTL temporal logic is detailed in [28, 29, 57, 60]. Using this query language, it is possible to formulate probabilistic queries in this format:

  • Qualitative queries: \(\mathtt {P_{\ge \theta } [ \varphi ]}\), where \(\theta \in [0,1]\).

  • Quantitative queries: \(\mathtt {P_{= ?}[ \varphi ]}\), where \(\varphi \) is a bounded LTL formula.

Below are two illustrative examples with their natural language translation.

  • \( \mathtt { P_{\ge 0.68} [fail \ U^{\le 1000} reboot ]}\) “The probability of the system eventually reboots after failure is at least 0.68”. The path formula \(\mathtt {F^{\le 1000}}\) specifies that the length of the considered traces is 1000.

  • \( \mathtt { P_{=?} [F^{\le 1000} shutdown ]}\) “What is the probability that the system eventually shutdown?”.

BIP has been implemented in a distributed setting [70, 71], and the components exchange information through asynchronous messaging. This means that each component is capable of sending messages, waiting for notifications or performing internal computations based on harmonizing and coordinating protocols. However, it is important to note that this representation only shows a high-level view and does not reflect the actual software platform structure where the processor manages task scheduling.

5 Model transformation

Fig. 5
figure 5

BIP grammar integration in eclipse tool (supported by the eclipse foundation). The figure shows the BIP project explorer on the left and the BIP editor on the right

Full size image

In this section, we showcase the conventional model transformation process that utilizes Eclipse plug-ins to automatically generate the specific code needed for robot orchestration.

5.1 BIP models to Java code by example

Before integrating the event bus component, the model is fed into the code generator engine. The engine utilizes Xtend to capture the modelled atomic components, made possible through the Xtext module that enables grammar specification and keyword colouring. The result of such integration is portrayed in Fig. 5. Each atomic component is converted to Java class that extends Java thread and annotates with BIP ports. The example of the atomic component in Listing 1 is mapped to Java code in Listing 2. The initial state START and the next state LOADING characterize the atomic component. The command in line 9 is enabled if the START location is marked and the corresponding condition in the provided construct is satisfied.

figure n

A set of attributes and operations characterizes a Java class. These attributes are related to the data manipulated by atomic components and the locations identified by the “place” keyword. The data types of atomic components are mapped to the respective Java data types, while BIP locations are mapped to Boolean variables. For example, in Listing 2 lines 13–14, the activation of the port p means that the function preceded by the annotation “@p()” is called. If the location “START” is evaluated to true (line 15), then the guard is checked (line 16), while the do actions correspond to Java instructions. Functions that are not preceded by Java annotations are called by do actions.

figure o

BIP connectors are managed by a connector scheduler that facilitates communication between Java classes through scheduled send–receive operations. However, it is important to note that our generator only handles a subset of the communication styles supported by BIP Connectors [67].

5.2 Deployment of Java code at EventBus level

The connectors scheduler does not handle communication between generated components; instead, this task is the responsibility of the PAREMUS Event Bus. The bus is responsible for both data communication and eventing. Ports defined in Listing 2 are mapped to Java interfaces. Atomic components are now considered as Java Bundles or “SmartBehaviour”, where an additional Java class is created to handle event listening (as shown in Listing 3). The required interface (i.e. BIP Port) is specified as a consumed interface within the “@SmartBehaviourDefinition” annotation (line 2). The “notify” function is sensitive to the event; for example, in line 8, the “RobotImpl” class is listening for events of type “IresolveCollision” (line 8) and performs the corresponding actions.

figure p

6 From modelling to simulation of Robots Orchestration system

This section describes the scenario provided by Robotnik,Footnote 9 followed by the BIP model and architecture related to the case study for analysis.

6.1 Robots Orchestration scenario

A privately owned warehouse houses thousands of carts filled with two or three products, which are transported by Robotnik-manufactured robots programmed to travel in all four cardinal directions to reach their respective destinations (See Fig. 6, 7). Upon reaching the designated cart, the robots (see Fig.  8) execute a corkscrew motion to lift the unit from the ground, transporting it in its entirety to the storage area \(\textcircled {{\small 2}}\) as depicted in Fig. 6 where humans pack the appropriate items. After completing the delivery, the robot proceeds to the unload area \(\textcircled {{\small 3}}\) and locates a new cart amidst the densely packed shelves. A fog-based brain controller is responsible for coordinating the robot’s movements across the 2D surface (see Fig. 6 and Fig. 7).

Fig. 6
figure 6

2D map surface of the warehouse

Full size image

Every 0.5 s, the controller sends position requests, and the robots (see Fig.  8) will send back a structured response in JSON. The JSON scripts related to robot interactions are available in [72]. The robots read their positions from the QR code tag placed on the square grid (see Fig. 6). Also, the response contains the actual robot state, such as “stopped” or “running”. The robots are endowed with motion sensors in the front to switch to the “stopped” state if obstacles are detected, so the robot response includes an integer attribute “detect” taking values from 0 to 2. If it is 0, then no obstacle is detected else; the obstacle could be a door or robot. When the robot detects a door, the orchestrator will send a request to the automatic door to open, and then, the robot can enter the unload area. In case of collision shall be avoided, the controller will execute a “collision resolve” that orders the robots to update their positions. After retrieving the necessary carts and depositing them in the storage area, the robots return to their original positions in the docking area.

The companyFootnote 10 responsible for deploying this system would ensure that loading and unloading processes are functioning correctly while also ensuring that collision avoidance measures are properly executed. The central deployed orchestrator must fulfil two requirements:

  • REQ-1 If a cart with densely filled shelves is detected, the robot performs a corkscrew motion to lift the cart off the ground and transport the entire unit to the storage area.

  • REQ-2 If a robot in front is detected, collision avoidance measures shall be taken to ensure safe navigation towards the robot’s destination.

Fig. 7
figure 7

Robots movement direction

Full size image
Fig. 8
figure 8

Robot prototype

Full size image

6.2 Robots Orchestration model

To demonstrate the practical application of the BIP framework, we have precisely developed BIP models for Robots Orchestration by capturing the control flow of the scenario depicted in Sect. 6.1. First, it starts with a definition of functions that retrieve the position of robots using the reserved word , e.g.:

figure r

Other variables are used to check the nature of obstacles in front of the robots declared also as constant (Figs. 7 and 8):

figure s

Each transition is labelled with a port that needs to be declared in BIP. Two kinds of ports are declared in the model: “export port” and “internal port” as mentioned in Sect. 4. The “export port” is used to trigger transitions while synchronizing with external atomic component, whereas “internal port” are used to trigger internal transitions. So, we have to declare three port type using the reserved word :

figure u

The first port type is utilized for receiving and transmitting robot parameters from/to the orchestrator, which enables the resolution of collisions between robots. As mentioned in Fig. 9, the port is instantiated by the atom “Robot_Behavior” in and . The port instance referred to the third port definition while no parameters are sent. These kinds of ports are called silent. These ports are used to label transitions between different BIP states. In BIP, states are preceded by the reserved word :

figure z
Fig. 9
figure 9

Graphical BIP representation of individual robot behaviour

Full size image

The BIP model shown in Fig. 9, representing a robot, is suitable for all robots. Other robots (i.e. atomic components) are reusing the same model by instantiating it with a different name as in Listing 4 lines (4–6). Hence, the robots are instantiated with the names “Robot1”, “Robot2” and “Robot3”. The same manner will be applied for connectors as in lines 9–11. Connectors have three port parameters since they handle the communication between robots and the orchestrator. Further, some atoms ports are exported (i.e. used for synchronization) in the model of Fig. 9. They are identified on the frame edge with red colour, for instance, and , and ports.

figure ad

When the robot model is triggered, as portrayed in Listing 5 local variables (i.e. position) are initialized for the first execution. Also, the “id” of the robot in Listing 4 (line 4, id=1) is initialized with the parameter value “VID” of the component as in Listing 5 (line 2). Moreover, the robot retrieves its actual position by calling the function “getPosition()” that is declared above.

figure ae

The BIP model in Fig. 9 relies on multiple phases that are labelling the model transitions, for instance; the port “” labels START \(\rightarrow \) UNLOAD, “” labels UNLOAD \(\rightarrow \) UNLOAD, “” labels UNLOAD \(\rightarrow \) STORAGE, “” labels UNLOAD \(\rightarrow \) OBSTACLE. In case the door is detected while guard “position==isDoor” a transition is enabled OBSTACLE \(\rightarrow \) DOOR labelled with port instance , else, multiple robots are standing in the same position while they activate the for OBSTACLE\(\rightarrow \)ROBOT. When the collision is resolved, a transition occurs on ROBOT \(\rightarrow \) START labelled with .

Fig. 10
figure 10

Graphical BIP representation of door behaviour (left) and orchestrator behaviour (right)

Full size image

The red ports identified in Fig. 9 are synchronized with those portrayed in Fig. 10. Two atomic components are modelled: the left one (i.e. Door behaviour ) model is the door opening, whereas the right model is the orchestrator that is identified with tree states “START”, “COLLISION” and “RESOLVED”. The collision is resolved by calling external functions “resolvedPosition1(position1)”, “resolvedPosition2(position2)” and “resolvedPosition3(position3)”. These functions rely on Artificial Intelligence algorithms that return the new position of robots as to move forward/backward or moving left/right.

Three connectors are identified to ensure communication between atomic components, as mentioned in Listing 4. The first connector in line 9 allows the opening of the door following a Broadcast manner described in Sect. 4 where the door is triggered when one of the robots is ready on the transition DOOR \(\rightarrow \) START as portrayed in the chronogram of Fig. 11. The connection is handled cyclically, prioritizing the first available port. Listing 6 portrays a textual representation of the Broadcast connector to open the door. As the synchronization solely requires a basic notification to trigger the operation, no behaviour is impacted

figure am

In addition, robots simultaneously communicate their positions to the orchestrator to perform collision detection and avoidance. In this case, the robots send their positions at the same time to the orchestrator, which is handled by the Rendez-Vous connector. Transitions labelled with port in the model do not occur until the Rendez-Vous is satisfied, portrayed in the chronogram of Fig. 12. Listing 7 portrays a textual representation of the Rendez-Vous connector. During the synchronization, robots communicate their current positions to the orchestrator in lines (4–7).

Fig. 11
figure 11

Broadcast synchronization for connector of Listing 6

Full size image
Fig. 12
figure 12

Rendez-Vous synchronization for connector of Listing 7

Full size image
figure ao

Figure 13 depicts the global graphical architecture of the complete Robots Orchestration system. It is a graphical interpretation of the textual representation in Listing 4. The blue line links model the connectors, the red boxes model components, and the black circles model the ports.

Fig. 13
figure 13

Graphical BIP representation of Robots Orchestration system

Full size image

6.3 Verification and analysis of compliance with requirements

Utilizing the resulting BIP models, we rely on SMC-BIP to conduct statistical analysis. SMC-BIP [28] generates runtime traces required to verify probabilistic bounded LTL properties. One of the distinguishing features of SMC-BIP is that it can determine the probability of a specified PBLTL property holding based on the generated traces. Regarding the requirement expressed in the Robots Orchestration scenario, we formalize it in PBLTL as follows:

figure ap

The property \(\varphi _{1}\) expresses that the robot R1 is in the UNLOAD position for lifting the cart and then returned STORAGE position. The resulting probability is equal to 80%.

Moreover, we would check the total carts that have been collected by three robots (in our case we model a system with three carts). In this case, we define a new variable “cart” that is initialized to 3. The function “liftCart()” sends actions to the robots to perform the operation and returns the remaining cart. Thus, the value of the cart is updated through the transition statement OBSTACLE \(\rightarrow \) CART as follows:

figure aq
figure ar
Fig. 14
figure 14

Checking results of properties \(\varphi _{2}\), \(\varphi _{3}\) and \(\varphi _{4}\)

Full size image

The properties \(\varphi _{2}\), \(\varphi _{3}\) and \(\varphi _{4}\) express that when the robots R1, R2 and R3 are at the docking position, they move to unload position after visiting the storage area. The robot will lift the cart and place it in the unload area. Also, the properties evaluate the number of carts collected by the robots. Checking \(\varphi _{2}\) using SMC-BIP results in the graphs portrayed in Fig. 14. The findings indicate that the probability of robots collecting a single cart is high, at approximately 90%. However, there remains a possibility that the robots may not collect any carts. Therefore, the likelihood of robots collecting two carts consecutively is nearly 80%. Due to high levels of concurrency among the robots in the warehouse, collecting three carts successively has a relatively low probability ranging between 10% and 20%.

figure as

Moreover, we want to check how the orchestrator resolved the collision during the robot’s movement. The transition START \(\rightarrow \) COLLISION in the automata model of the orchestrator has for actions to increment the number of detected collisions. The property \(\varphi _{5}\) expresses that when the robots are in the docking area, then they collect a set of carts “C” with a certain number of collisions. The symbol “\(\texttt{O}\)” refers to the orchestrator component instance. The result of checking property \(\varphi _{5}\) is portrayed in Fig. 15. The likelihood of three collisions occurring during the movement of robots is low, as compared to one or two collisions. This trend can be attributed to the fact that when the robots collect carts, they return to their docking position and consequently reduce the number of robots in various warehouse areas, thereby minimizing potential collisions.

Fig. 15
figure 15

Checking results of property \(\varphi _{5}\)

Full size image

6.4 Validation at PSM level

While the BRAIN-IoT PIM level is based on statistical model checking, which enables estimation while satisfying requirements, behaviour may differ significantly at the PSM level. Components such as robots are not linked using connectors; instead, they communicate through dedicated libraries that facilitate send/receive operations with physical units. Connectors can be represented by buses that transport data using send/receive protocols. Furthermore, the quality of data transportation is determined by parameters such as the number of bus access conflicts and bus delays, which are not visible at the PIM level. The paper does not cover the verification procedure at the transaction level.

After verifying that all requirements were satisfied, we performed a model-to-text operation to generate Java code corresponding to the BIP models detailed in this paper. The code generated from this operation is available in [61]. Each atomic component has been translated into a Java class capable of handling all necessary operations for robot movements. Finally, we conducted a simulation using the generated Java code from the initial BIP models. Fortunately, while moving from docking to unloading areas, robots are able to collect available carts for transportation. This confirms that the deployed infrastructure aligns with PIM BIP models. Moreover, we observed that it is impossible for robots to collect two carts due to how communication APIs handle requests during conflict resolution.

Each class is wrapped within OSGi bundles that are accepted by the BRAIN-IoT Service Fabric. The OSGi bundles are deployed over a cluster with Ubuntu \(-\)16.04 desktop Intel core i7-950@3.07 GHz and ROS Kinetic with STAGE [73] and rviz GUI [74].

Also, we use sensinact controllers [65] that implement the mechanic to communicate with the simulation platform called ROS-REST API. We use rviz to plan the intelligent robot’s movement within a 3D movement area and STAGE to capture a robot’s movement into 2D plan. This simulation is done to validate the requirement REQ-2. The sequence of robot movements is portrayed in Figs. 16, 17 and 18. Figure 16 presents the initial state of the robots in the docking area. Figure 17 presents the state of the blue robot in front of the door, so the door is not visible in the figure. Figure 18 portrays the carts and robots in the unloading area. Through the simulation, no collision is observed due to well orchestration management and competitive access to the unloading area. In addition, we could observe that the door reacts to the robot’s demand to open it. These observations help the designer make judgments about the accuracy of the modelled system. Also, these observations validated the requirements expressed formally in LTL.

Fig. 16
figure 16

Robots in docking area

Full size image
Fig. 17
figure 17

Robots in front of the door

Full size image
Fig. 18
figure 18

Robots in storage area

Full size image

7 Conclusion

This paper presents the functional assurance artefact of the BRAIN-IoT framework, which relates to the orchestration of a fleet of robots within warehouses by Robotnik System Company. The scenario at hand involves utilizing a central computer that is equipped with AI algorithms to detect and manage collisions. Our proposed approach to accomplish this task is through the utilization of a model-driven design (MDD) methodology, which establishes several refinement levels.

This research specifically focuses on the design level of the orchestrator-controlled robotic network, which is developed using the BIP language. To ensure the accuracy of the design, we utilize SMC-BIP to verify a set of properties expressed in PBLTL at the PIM level. By utilizing mathematical reasoning, this formal verification technique provides designers with functional assurance for robotic scenarios. A Java code is generated through model-to-text transformation, enriched with Brain-IoT Fabric annotations and communication libraries, to facilitate the deployment of IoT nodes.

In addition to the high-level analysis, we validate our findings through simulation, which takes into account the features of both the robot’s communication services and the BRAIN-IoT Service Fabric. In our future work, we will conduct verification at the transaction level by accurately modelling communicating buses. We will also focus on validating a second use case for the water dam system that regulates drained water in Corona, Spain.