arXiv CSopen access

Scenario-based System Testing for Distributed Robotics Applications

Scenario-based System Testing for Distributed Robotics Applications Jan Peleskaa , Felix Brüningb , Wen-Ling Huanga , Anne E. Haxthausenc

arXiv:2604.25772v1 [cs.SE] 28 Apr 2026

a

University of Bremen, Bibliothekstraße 1, Bremen, 28359, Bremen, Germany b Verified Systems International GmbH, Am Fallturm 1, Bremen, 28359, Bremen, Germany c DTU Compute, Technical University of Denmark, Building 322, Lyngby, 2800, Lyngby, Denmark

Abstract We present the SCenario Specification Language (SCSL) for automated generation and execution of system-level tests. SCSL targets complex distributed systems (e.g., collaborating autonomous robots) where classical model-based testing becomes impractical because (1) the overall system complexity is too high for a single monolithic model, (2) test behaviour cannot be fully precomputed due to substantial nondeterminism in the distributed system under test (SUT), and (3) the SUT configuration may change dynamically at runtime. Challenge (1) is addressed by scenarios: each scenario specifies test-specific expected SUT behaviour and/or stimuli to be applied during execution. Complex system tests are composed from elementary scenarios using sequential and parallel composition. To address (2), the SCSL tool platform supports online (on-the-fly) testing, selecting and executing test steps during runtime. For (3), SCSL provides a collaboration construct that supports dynamic reconfiguration: removing unavailable components, registering newly joining components, and rewiring interfaces during test execution. We illustrate the syntax and semantics of SCSL using a system-test example in which robots perform a salvage mission, and we use an automatically generated test execution to demonstrate the concepts supported by our prototype tool platform. Keywords: System testing, Scenario-based testing, Collaborating robots, Linear Temporal Logic

1. Introduction 1.1. Objectives The objective of this article is to present the SCenario Specification Language (SCSL) for defining and executing functional system tests for complex cyber-physical systems (CPS). The presentation uses a typical example of a system test for several robots collaborating in a joint mission. When comparing “classical” model-based system testing (MBT) to the scenario-based approach, the crucial differences are as follows. • MBT aims to capture all admissible system behaviours within a comprehensive system model. From this model, test cases, test data, and test procedures are derived to achieve a certain level of coverage. This model coverage may also be related to requirements coverage, if the underlying formalism allows for tracing model elements to requirements and vice versa [1]. • Scenarios are more restrictive behavioural models, each scenario describing a relevant behavioural aspect of the system, for example, a traffic scenario for an autonomous vehicle. Each relevant system behaviour should be covered by at least one scenario. The collection of all scenarios, referred to as the scenario library, serves as a structured specification of system behaviour for testing purposes. A separate validation activity not discussed in this paper ensures that all relevant behaviours are covered by the library [2]. • Typically, scenarios types are parameterised, so that they can be instantiated in different system test situations with different parameter values. A scenario instance is a concrete behavioural specification, where all parameters have been associated with concrete values (so-called actual parameters). • The objects under test – in the example presented below, the collaborating robots and a command centre supervising the mission – are input parameters to the test scenarios, and their expected behaviour is specified in the scenario, since only the scenario-specific behavioural aspects need to be described. • A scenario-based system test consists of a set of scenario instances that define a meaningful end-to-end system behaviour in alignment with specific test objectives. 2

Consequently, scenarios are easier to specify than the reference models needed in MBT, where the expected behaviour of a system under test (SUT) needs to be modelled for all operational situations. Apart from their complexity, the distributed CPS that have influenced the design of the SCSL typically pose two further challenges: The local autonomy of the SUT components induce a very high degree of nondeterminism. Consequently, pre-calculated linear test steps will often be unsuitable to reach the system test objectives. Therefore, the underlying tool platform needs to support online testing, where the consecutive test steps are calculated at runtime, based on the currently observable state of the SUT. Note that this capability just depends on the underlying tool implementation, it is possible both for MBT (see Larsen et al. [3]) and scenario-based testing. The final challenge consists in the fact that complex distributed CPS may change their configuration at runtime: robots, for example, may autonomously decide to leave or enter the SUT configuration, they may no longer be available due to some component failure, and interfaces may be “rewired” at runtime. Therefore, modelling formalisms only able to describe static process networks [4] are unsuitable for describing (comprehensive models or) scenarios for testing these CPS. 1.2. Test Configurations Typical test configurations for the scenario-based approach advocated by the authors will be variants of the one depicted in Figure 1. The CPS under test is a distributed system where control computers communicate with each other and may act on electro-mechanical peripherals. In a system test configuration, some of these control computers will be present as original equipment OE, while others are replaced by simulations SIM. Hardware peripherals could also be replaced by other simulations, or they could be present as original peripherals PER. The solid lines between boxes each represent one or more interfaces for data exchange. Interfaces (to be introduced in Section 3.8) realise uni-directional data flows between components participating in a system test. The objective of system tests is to check the functional behaviour of all original equipment and peripherals, as well as their interactions. The “local” behaviour of original equipment is monitored by original equipment harnesses OEH. These harnesses run test-specific elementary scenarios specifying the expected behaviour of their OE during the system test, as well as 3

the stimulations to be provided for some OE input interfaces, as far as these are not provided by other OE or by simulations or peripherals.

Coordinator Agent

Emergent Property Monitor

Figure 1: System test configuration.

The succession of elementary scenarios to be executed by each OEH is coordinated by a coordinator agent CA. The CA receives status information about ongoing elementary scenario executions performed by each OEH and provides further elementary scenarios to be scheduled by the associated OEH. The collaboration between all components of the CPS will result in certain emergent properties [5] achieved by the overall system. These can be checked by an emergent property monitor EPM observing all communications between CPS sub-components and its operational environment (typically replaced by simulations during a system test). 1.3. Contributions Previous work by the authors. This article is based on the authors’ conference contribution to TAROS2025 [6]. There, the SCSL syntax and its semantics have been introduced in abbreviated form. A robotics system test 4

where all scenarios acted as observers (i.e. test oracles) had been used to illustrate SCSL usage. While other existing scenario modelling languages are frequently domain-specific, the SCSL has been expressly designed to allow for applications in any domain: Domain-specific details (e.g. physical laws) can be encapsulated in separate elementary scenarios that are collected in a reusable library. Another distinguising feature of the SCSL is that elementary scenarios may combine declarative and imperative specification styles: Linear Temporal Logic (LTL) allows for declarative specifications, and a guarded action language allows for imperative specification. From our experience, this facilitates behavioural modelling in a considerable way. • Declarative specifications are good for including all acceptable behaviours without having to enumerate them algorithmically. On the downside, it may be quite hard to produce declarative specifications that capture all acceptable behaviours without inadvertently including some unwanted behaviours. • Imperative specifications, when designed with a focus on simple readability, may exclude alternative acceptable solutions. A further distinguishing SCSL feature is that its semantics takes explicitly into account that typical controllers in a CPS run in execution cycles of constant duration. New inputs are read and outputs are written at the beginning of each cycle. Therefore, they no longer behave like perfect physical models whose differential equations specify piecewise smooth evolutions for each real-valued observable (such as location or velocity). Instead, controllers produce variable updates at each cycle that should be close approximations of the discretised differential equations of the underlying physical models. Our position (which is also shared by other authors working in the field of CPS [7]) is that formalisms using a semantics close to physical models (like, for example, the Multi-Lane Spatial Logic MLSL [8]) should only be used to describe the idealised physical view of a CPS, while modelling formalisms used to derive test cases for the implemented system should take into account the cyclic nature of the controllers involved. The challenges posed by SUTs with dynamically changing configurations have been solved by means of a collaboration specification which is part of an SCSL system test specification and my be modified during the test execution. New contributions in this article. For this article, we have extended our previous work as follows. 5

1. The elementary scenario syntax has been extended by auxiliary framevariables. These make it easy to specify whether an elementary scenario should act as an observer or a stimulator, influencing SUT reaction: An orginal equipment harness running an elementary scenario instance may change object parameters that are registered in the frame to ensure that the LTL specifications are fulfilled. If the frame is empty throughout the test execution, the scenario instance acts as an observer, and a violation of an LTL specifications is reported as a failure of the test execution. 2. The system test example has been modified to allow for both observer scenario instances and simulated equipment instances. 3. Auxiliary object have been introduced to facilitate inter-scenario communication at runtime. 4. The section on related work has been updated to take latest developments into account. 5. The behavioural semantics of scenarios is now explained in full detail in an appendix. 6. A new section presents a system test example with automatically generated data. This is also used to illustrate the basic functionality of the underlying prototype tool platform. While contributions 1 — 4 are minor (but in case of 1,2,3 quite effective) extensions, contributions 4 and 6 are substantial. 1.4. Overview In Section 2, the system test used as an example for introducing the SCSL is described in natural language. The SCSL objects and scenarios involved, as well as the resulting system test configuration are presented in Section 3. In this section, the SCSL syntax and its intuitive semantics are explained as well. A system test exeacmple with explanations on the SCSL prototype platform is discussed in Section 4. In Section 6, related work is discussed. Section 7 contains a conclusion and discusses future work. In Appendix A, we present a more formal comprehensive explanation of SCSL behavioural semantics. 2. A System Test for Verifying Distributed Collaborating Robots Mission. The robots’ mission is to salvage goods from a known location in a hazardous area, where a salvage by humans is deemed to be impossible, due 6

to various adverse environmental conditions. Goods to be salvaged. The goods consist of m > 0 items (like boxes or barrels) that can be picked up by a robot arm and loaded onto a transport-capable robot. Each item has a unique id, which can be spotted by the robots.1 Terrain. We assume that the terrain where the goods are located has several exclusion zones (such as cliff edges), so that the robots cannot reach their destination on a straight path from their starting points.

Figure 2: Rover-type robot.

Robots. There are n robots of the rover type (see Fig. 2): they move on wheels that are suitable for the terrain. Each rover is identically equipped and has the same capabilities: (1) A robot arm to pick up an item. (2) A cargo bed where an item can be placed. (2) Sensors allowing to detect the boundaries of exclusion zones. (3) A GPS sensor to determine its location. (4) Autonomous moving capabilities to circumvent exclusion zones and find a path to a given destination, if such a path exists from their actual location. (5) Cameras, image recognition functions, RFID readers to detect and pick up an item and place it on a robot’s flatbed. (6) Communication equipment 1

Typical identification techniques could be QR codes or RFID tags

7

to send status information to a command centre and receive commands from there. (7) Controllers to process the commands received. Mission planning. As the optimal path to the goods is unknown, rovers are deployed from different starting points, but they all get the same destination coordinates where all items to be salvaged are located. It is expected that some rovers will get stuck on their path and be unable to reach the destination. Others may have hardware faults, and some might be destroyed by inadvertently entering an exclusion zone. Therefore, n rovers are initially sent on the mission, while only m < n rovers are needed to pick up and return the salvaged goods. The first m to reach the destination will be commanded to pick up the goods. To this end, the command centre sends different item ids to the rovers, so that they all approach and load different items. As soon as a rover has managed to load an item onto its flatbed, it is commanded to return to a specific location. If a rover becomes unavailable, either due to entering an exclusion zone or experiencing a failure, the command centre may reassign the corresponding task to another rover that has already returned with an item, instructing it to collect a new item that was originally assigned to the now unavailable rover. All rovers that get stuck or fail during their mission are commanded to return (even if it is uncertain whether they will be able to return at all). The same holds for operative rovers that are no longer needed since all items to be salvaged have been picked up by other robots. Return locations may vary between rovers, especially for those that failed to reach the destination and can exit the hazardous area more quickly via alternative paths. Pass criterion. The system test passes if at least m ≤ n rovers arrive before time tatDst (arrival deadline) and at least k ≤ m rovers return carrying salvaged items before time tend > tatDst (mission completion deadline). System test configuration. For the system test considered here, it is assumed that all robots are available as original equipment, but that the command centre should be simulated by the testing environment. 3. Scenario-based System Test Specification in SCSL 3.1. Overview A complete SCSL system test specification consists of (1) elementary type specifications, such as enumerations, (2) composite data type specifications, 8

similar to mathematical data types in Z or VDM [9, 10], (3) global constants and function definitions, (4) object type specifications for the types of components participating in a system test, (5) elementary scenario type specifications, and (6) a system test configuration. A system test configuration references all the participants in the test execution, as well as their means of interaction, and the test execution schedule. The participants are instances of object type specifications. Each object represents original equipment, peripherals, or simulations thereof. Auxiliary objects may be used as data containers storing information to be communicated between elementary scneario instances. The means of interaction between objects are provided by interfaces. Objects and interfaces are comprised in a collaboration 2 which is the first part of a system test configuration. The execution schedule (second part of the system test configuration) shows how original equipment should evolve (i.e. expected/checked at runtime) and how simulations will evolve (i.e. enforced by the test environment) over time during the system test execution. An elementary scenario refers to one or more objects and specifies their required behaviour for that particular test situation. Crucially, SCSL follows a scenario-centric style: object types provide interfaces and state/data structure, while the situation-dependent behaviour relevant to a test step is specified in the scenarios that involve the objects (and their parameters). Instead of specifying the full behavioural model of an object type inside the object type, the behaviour required in a given test situation is specified in an elementary scenario that refers to the object and instantiates its parameters. In the terms introduced in Section 1, elementary scenarios runs on an original equipment harness (OEH). Note that system test schedules usually involve more than one elementary scenario, since this type of test aims at verifying end-to-end functionality, as perceived by end users of the system. In the system test of the robots described in this paper, for example, separate elementary scenarios are used to describe robots approaching the salvage destination, robots loading items to be salvaged, and robots returning with or without items. 2

The term collaboration is used here in a generic sense to denote the set of participants and their interconnections; unlike UML [11] collaborations, SCSL collaborations are instance-based and dynamically reconfigurable.

9

In the remainder of this section, each of the six SCSL language elements will be explained, using the system test described in Section 2 as an example. While we give some intuitive explanations about the SCSL behavioural semantics in this section, a more formal comprehensive specification of semantics is presented in Appendix A. 3.2. Primitive Types and Composite Data Types Each rover accepts commands from the command centre: initially, command goToDst will set a rover into motion, trying to reach the specified destination. Command pickUpItem orders a rover that has reached the target destination to pick up an item to be salvaged. Command returnToDst directs a rover to return to a specific position.3 In the other communication direction, each rover sends status information to the command centre. While trying to reach the specified target destination, a rover is in state approaching, but it may also get broken along the way (state fault) or get stuck such that it will be unable to reach the destination (state stuck). After a rover has successfully picked up an item at the target destination, it transits to state itemLoaded, and then to returningWithItem after having been commanded to return to a specified position. After arrival at the return position, the final state of rovers carrying items is returnedWithItem. Some rovers will have to return without carrying items; for these, the states returning and returned apply. These enumeration types are declared as shown in Listing 1. Listing 1: Enumeration types. enum RoverCommands : {goToDst, returnToDst, pickUpItem}; 3 Status : {initial, approaching, stuck, fault, atDst, itemLoaded, 4 returning, returningWithItem, returned, returnedWithItem}; 5 end enum 1 2

We need a composite data type Location for specifying geographic coordinates (e.g. GPS) used for target and return destinations sent to the rovers. Also, each rover can establish its own position in coordinates of 3

In principle, commands goToDst and returnToDst have the same effect. We use two distinct commands, however, to clarify that first the target destination is specified to direct the robots to the goods to be salvaged (command goToDst), and after that the destination is specified to let the robots return to a home base (command returnToDst).

10

type Location. Another composite data type is Zone for specifying the exclusion zones that are present in the system testing area and should never be entered by any rover.4 3.3. Global Constants The constants needed for our system test are specified in Listing 2. Listing 2: Global constants. global const 2 n : N; -- initial number of rovers 3 m : N; -- number of items to be salvaged 4 k : N; -- minimal number of items to be salvaged 5 constraint 6 k≤m≤n 7 end constraint 8 tatDst : R≥0 ; -- arrival deadline when at least m rovers should 9 -- have arrived at destination 10 tend : R≥0 ; -- mission deadline when at least 11 -- k items should have been salvaged 12 constraint 13 tatDst ≤ tend 14 end constraint 15 targetDst : Location; -- target destination where the 16 -- items to be salvaged can be found 17 numZones : N; -- number of exclusion zones in the testing range 18 exclusionZone : Zone[numZones]; -- array of exclusion zones 19 startPos : Location[n]; -- start positions for each rover 20 returnDst : Location[n]; -- return destinations for each rover 21 allIds : ItemId∗ ; -- List of item identifiers 22 -- for each item to be salvaged 23 constraint 24 #allIds = m -- there are m items to be salvaged 25 end constraint 26 end const 1

3.4. Object Types The object types for our system test are rovers and command centres. Rovers accept commands cmd from the control centre, the specification of destinations dst to be reached by each rover, identifications id of items to be picked up and salvaged, and their actual position pos provided by some 4

Typically, a Zone element would be represented as a simple polygon.

11

external positioning system like GPS. As output, each rover communicates its current status s to the command centre. This interface specification is given in Listing 3, lines 1 and 2. As motivated in Section 1, original equipment, peripherals, and simulations thereof operate in fixed processing cycles that may differ between object types. Therefore a cycle time is specified in relation to the (faster) observation and stimulation cycles that can be performed by the test equipment. The specification cycletime 20 states that any instance of type Rover performs one processing cycle in 20 observation cycles of the test equipment. Listing 3: Object type ‘Rover’. object type Rover(in cmd : RoverCommands, in dst : Location, in id : ItemId, 2 in pos : Location, out s : Status) 3 cycletime 20 4 end type 1

Command centres accept an array s[i], i : 0..(n − 1), of status values, one from each rover, as inputs. They communicate possibly different commands cmd[i], destination specifications dst[i], and item identifications id[i] to the rovers. This is specified in Listing 4. Listing 4: Object type ‘CommandCentre’. object type CommandCentre( in s : Status[n], out cmd : RoverCommands[n], 3 out dst : Location[n], 4 out id : ItemId[n] ) 5 cycletime 10 6 end type 1 2

Note that these object type specifications do not indicate how outputs of some objects will be linked to inputs of others, since this cannot be determined once and for all on type level. Instead, the mapping from outputs to inputs is specified on object level in the collaboration part of the system test configuration (see Section 3.8). 3.5. Auxiliary Object Types While the object types introduced above represent constituents of the system under test, auxiliary object types can be introduced with the same syntax as introduced above for storing “meta data” related to the test execution status and performing auxiliary services to support the test execution. Instances of auxiliary object types are created in the testing environment 12

and executed, for example, on original equipment harnesses or as parts of simulations. 3.6. Global Function Declaration For evaluating the system test, a counting function is needed: numRovers(r, S) counts the number of rovers in array r whose state has one of the values specified in set S. Boolean function inExclusionZone(pos, exclusionZone) returns true if and only if the geographic position pos is in one of the exclusion zones exclusionZone[i], i : 0..(numZones − 1).5 Boolean function isCloseTo(pos, dst) returns true if and only if a robot’s actual position pos is close to the destination coordinate dst, so that the robot is in the position to load an item. Listing 5: Global functions. global function numRovers : Rover[n] × P(Status) −→ N; 3 (r, S) 7→ #{i : 0..(n − 1) | r[i] ̸= null ∧ r[i].s ∈ S}; 4 inExclusionZone : Location × Zone[numZones] −→ B; 5 -- inExclusionZone(pos, exclusionZone) = true iff pos is contained in one 6 -- of the exclusion zones exclusionZone[i] 7 -- (application of the ray casting algorithm) 8 isCloseTo : Location × Location −→ B; 9 -- isCloseTo(pos, dst) = true iff pos is close to dst 10 end function 1 2

For functions inExclusionZone and isCloseTo, the detailed specifications have been ommitted in Listing 5. They would also be specified in Z-style, as illustrated in the case of the function numRovers. 3.7. Elementary Scenario Types Scenario structure and behavioural specification. Elementary scenario types specify how the objects of interest should behave or interact with each other in certain operational situations. In SCSL, each elementary scenario type comes with the following sub-components. 1. An interface specification containing parameters representing object references6 and scalar input values used for scenario configuration. 5

For determining whether a coordinate is inside a simple polygon, the ray casting algorithm could be used [12]. 6 Similar to Java, instances of object types are passed by reference to the elementary SCSL scenarios

13

2. A precondition over interface parameters, specifying the conditions of an elementary scenario instance to start its execution. 3. A behavioural specification consisting of (a) LTL formulae over interface parameters and auxiliary variables, (b) optional initial actions setting the initial values of auxiliary variables, (c) optional condition-action pairs defining writes to auxiliary variables, depending on conditions over interface parameters and auxiliary variables. For elementary scenario types, all parameters are inputs, so keyword “in” is superfluous: Auxiliary outputs to be relayed to other scenarios at runtime are communicated via auxiliary objects (Section 3.5). Conditions in condition-action pairs can be • guards g that trigger the associated action in every execution cycle where g evaluates to true. • change conditions chg that trigger the associated action in every execution cycle where chg changes from false to true. This concept for behavioural modelling deliberately mixes declarative and imperative specification styles: LTL formulae are implicit (=declarative) behavioural specifications that are refined by adding conditions and actions in imperative style that is quite similar to state machines used in UML [11]. From our experience, LTL formulae (or declarative specifications in general) often specify behaviours that are too general, so that some unwanted executions are still accepted by these formulae. The condition-action pairs changing auxiliary variables and the use of the latter in LTL formulae allows to narrow down the accepted behaviours in an effective way. The exclusion of unwanted behaviours is additionally supported by the utilisation of frames, as originally introduced in the Vienna Design Method VDM [10]. Pre-defined set-valued auxiliary variable frame contains the names of all object parameters that may be changed in the current execution cycle. This helps in situations where the SUT should conform to a declarative specification φ(o1 .v1 , o2 .v2 , . . . , ok .vk ) without changing a subset of the object parameters oi .vj . The symbol names of changeable object parameters must always be contained in variable frame. Auxiliary variable frame is implicitly set to the complete collection of all parameters of all objects referenced in 14

the scenario parameter list. It can be changed in the actions specified for the scenario type by adding or removing object parameter symbols. Moreover, each elementary scenario is associated with an implicitly defined variable active that is set to true when the precondition evaluates to true for the first time. When active is reset to false, this indicates the termination of the scenario execution. After scenario termination, the behavioural specifications need to hold no longer. One global variable EoT is false at the beginning of a system test execution, but can be set to true by any elementary scenario, whereupon the system test terminates. If EoT is never set to true, a system test ends when all elementary scenarios involved have terminated (status change from active = true to active = false). Rover-specific scenario types. For the system test under consideration, three elementary scenario types cover the rover-specific behaviours: Scenario type Approach specifies rover behaviour while approaching the target destination. Scenario Pickup specifies rover behaviour while picking up an item to be salvaged. Scenario Return specifies rover behaviour while returning to a specified location, with or without a loaded item. The Approach scenario type is declared in Listing 6. As input, each Approach-instance gets a reference to a specific rover r and the location startPos from where the rover shall start its journey to the target destination. The latter is specified in r.dst, and this destination is communicated from the command centre to the rover, before the scenario becomes operative. The precondition for an Approach scenario instance to become active states that (1) the rover’s initial state is initial (this is an expected behaviour when the rover is started), (2) the rover must have been placed at its starting position (this must be ensured by the system testing crew), and (3) the command input to the rover must be goToDst (so a scenario instance can only become active after the command centre has sent this command to the rover). For scenario type Approach, the behaviour is specified by LTL formulae only – no condition-action specifications are necessary: the first formula specifies the scenario termination condition. It states that active will be set to false after either (1) the rover inadvertently enters an exclusion zone (this actually destroys the rover, as will be handled in scenario type MishapHandler), or (2) the rover actually reaches the specified destination or gets stuck or broken before reaching it, or (3) the command centre sends a new command to the rover, indicating that reaching the target destination is no longer 15

necessary. The second formula asserts that the rover will finally get close to the target destination r.dst and change its state to r.s = atDst, unless it vanishes in an exclusion zone, gets broken or stuck, or receives another directive from the command centre. Scenario type Approach is an observer scenario. It specifies expected behaviour only, and instances of Approach must not change any object parameters. Therefore, the empty set is assigned to the frame-variable in the initial action. The original equipment harness running the scenario instance of Approach for a specific rover would signal an error if the second specification does not become true before the system test terminates. Listing 6: Approach scenario. elementary scenario Approach( r : Rover, const startPos : Location ) precondition r.s = initial ∧ isCloseTo(r.pos, startPos) ∧ r.cmd = goToDst; 3 spec G (inExclusionZone(r.pos, exclusionZone) ∨ r.s ∈ {stuck, fault, atDst} ∨
4 r.cmd ̸= goToDst) ⇒ X¬active ; 5 spec F inExclusionZone(r.pos, exclusionZone) ∨ r.s ∈ {stuck, fault} ∨
6 r.cmd ̸= goToDst ∨ (isCloseTo(r.pos, r.dst) ∧ r.s = atDst) ; 7 initact frame := ∅; 8 end scenario 1 2

Scenario type Pickup (Listing 7) specifies the expected rover behaviour during the pickup phase. Its precondition to become active is that the rover is commanded to either pick up an item or return to a given return destination. In the latter case, the first LTL formula states that the scenario will immediately become inactive, since there is no item to be picked up. Other scenario termination conditions are that the rover enters an exclusion zone or gets stuck or broken while trying to load the item, or that the item has been successfully loaded. If the command pickUpItem applies, the rover will finally succeed in loading the item, unless it fails before. This is expressed by the second LTL formula. Again, Pickup is an observer scenario type. Listing 7: Pickup scenario. elementary scenario Pickup( r : Rover ) 2 precondition r.cmd ∈ {pickUpItem, returnToDst}; 3 spec G (r.cmd = returnToDst ∨ inExclusionZone(r.pos, exclusionZone) ∨
4 r.s ∈ {stuck, fault, itemLoaded}) ⇒ X¬active ; 5 spec r.cmd = pickUpItem ⇒
6 F inExclusionZone(r.pos, exclusionZone) ∨ r.s ∈ {stuck, fault, itemLoaded} ; 1

7

initact frame := ∅;

16

8

end scenario

Observer scenario type Return (Listing 8) specifies how a rover returns to a given address. It becomes active as soon as a returnToDst command has been received from the command centre. Here we have an initial action that introduces a Boolean auxiliary variable auxisLoaded (its type is determined automatically from the right-hand side part of the assignment expression) which is set to true if and only if the rover has loaded an item. As usual, the rover may be lost after entering an exclusion zone, or it may get stuck or broken along the way. If, however, all goes well, it will finally arrive at the return destination and assume status returnedWithItem or returned, depending on whether it returns with an item or not. While approaching the return destination, the rover state r.s is returningWithItem or returning, depending on the value of auxisLoaded . Note that auxiliary variables need not be declared: their type is specified implicitly from the right-hand-side expressions in the assignments, similar to auto declarations in C++ . Listing 8: Return scenario. elementary scenario Return( r : Rover ) precondition r.cmd = returnToDst; 3 spec G (inExclusionZone(r.pos, exclusionZone) ∨ 4 r.s ∈ {stuck, fault, returned, returnedWithItem})
5 ⇒ X¬active ;
6 spec (r.s = returningWithItem ∧ auxisLoaded ) ∨ (r.s = returning ∧ ¬auxisLoaded ) 7 U 8 inExclusionZone(r.pos, exclusionZone) ∨ r.s ∈ {stuck, fault} ∨ 9 (isCloseTo(r.pos, r.dst) ∧ auxisLoaded ∧ r.s = returnedWithItem) ∨
10 (isCloseTo(r.pos, r.dst) ∧ ¬auxisLoaded ∧ r.s = returned) ; 11 initact frame := ∅; auxisLoaded := (r.s = itemLoaded); 12 end scenario 1 2

Scenarios for interactions between rovers and command centre. We need four elementary scenario types for describing the interaction between the command centre and the rovers during their approach to the items to be salvaged (ApproachHandler), while picking up items (PickupHandler), while returning to their specified destinations (ReturnHandler), and in the special case where a rover inadvertently enters an exclusion zone (MishapHandler).

17

Listing 9: Scenario for rovers approaching the target destination. elementary scenario ApproachHandler( cc : CommandCentre, r : Rover, 3 i : N0 )
4 spec G inExclusionZone(r[i].pos, exclusionZone) ⇒ X¬active ; 5 spec G r[i].s ∈ {initial, approaching} ⇒
6 (cc.cmd[i] = goToDst ∧ cc.dst[i] = targetDst) ; 7 initact frame := {cc.cmd[i], cc.dst[i]}; 8 end scenario 1 2

Scenario type ApproachHandler (Listing 9) inputs references to the command centre, the robots, and an index of the specific rover r[i] whose interaction with the command centre is considered in an ApproachHandler instance. The first LTL formula specifies that a scenario instance will terminate immediately if rover r[i] enters an exclusion zone, since the rover will be lost and can never reach the target destination. The second LTL formula asserts that when the rover has just been initialised or while it is still approaching the target destination, the command centre will continuously transmit the goToDst command and the targetDst (location of the items to be salvaged) to the rover. Note again that the transmission interfaces from cc.cmd[i] to r[i].cmd and from cc.dst[i] to r[i].dst are not specified in the elementary scenario declarations, but will be specified for the concrete objects in the collaboration which is part of the test configuration shown below. Elementary scenario type PickupHandler (Listing 10) specifies how the command centre directs rovers having arrived at the target destination to load items to be salvaged. To this end, three auxiliary variables are initialised (line 8): 1. auxid is initialised with the list allIds containing identifications of all items to be salvaged. 2. auxrAtDst is initialised as the empty set and then used to store all indexes of rovers that have arrived at the target destination, but have not yet been assigned an item to carry (line 9). 3. auxrLoading is initialised as the empty set and then used to store all indexes of rovers that have been assigned to carry an item but have not yet completed the task of loading the item (lines 10—11).

18

Listing 10: Scenario for rovers commanded to pick up an item. elementary scenario PickupHandler( cc : CommandCentre, r : Rover[n] )  V 3 spec i:0..(n−1) G r[i] ̸= null ⇒ i ∈ auxrLoading ⇒ 1 2

4

 (cc.cmd[i] = pickUpItem ∧ cc.id[i] = auxloadItemId [i]) ;

spec G auxid = ε ∨ (auxrAtDst = ∅ ∧ numRovers(r, {initial, approaching}) = 0) ⇒
7 X¬active ; 8 initact frame := ∅; auxid := allIds; auxrAtDst := ∅; auxrLoading := ∅; 9 cndact [true] / auxrAtDst := {i : 0..(n − 1) | r[i].s = atDst} \ auxrLoading ; 10 auxrLoading := auxrLoading \ {i : 0..(n − 1) | r[i].s ∈ {itemLoaded, stuck, fault}}; 11 if (auxid ̸= ε ∧ auxrAtDst ̸= ∅) then 12 ℓ := min auxrAtDst ; 13 auxrAtDst := auxrAtDst \ {ℓ}; 14 auxrLoading := auxrLoading ∪ {ℓ}; 15 auxloadItemId [ℓ] := popfront(auxid ); 16 endif 17 frame := {cc.cmd[i], cc.id[i] | i ∈ auxrLoading }; 18 end scenario 5

6

The assignment of items to rovers is performed in the condition-action expression in lines 11—16: as long as there are still items to be loaded (auxid ̸= ε), and whenever at least one rover is located at the target destination but still without an assigned item (auxrAtDst ̸= ∅), the following action is performed: 1. The rover with the smallest index ℓ in auxrAtDst is selected to load the next item in the list. 2. This index ℓ is removed from the set auxrAtDst of rovers that could still load an item and added to the set auxrLoading of rovers currently loading an item. 3. In auxiliary array auxloadItemId , the id of the next item to be loaded is written to index ℓ and removed from the list of items still to be salvaged (this is performed by instruction popfront(auxid ) which returns the list head and removes it from the list at the same time). The first LTL formula (lines 3—4) specifies that the command centre sends a pickUpItem command to all rovers that still exist in the collaboration (r[i] ̸= null) and whose index has been inserted into set auxrLoading . Moreover, the command centre provides the associated item id in output parameter cc.id[i]. The second LTL formula specifies that the scenario shall 19

terminate after all items have been assigned to rovers for loading or if there aren’t any rovers left to carry an item. Since scenario PickupHandler acts as a simulation, the frame-variable must be set in every cycle in such a way that the scenario is allowed to set cc.cmd[i] and cc.id[i] can be set by this simulations. Therefore, the frame variable is always set in line 17 to all cc.cmd[i], cc.id[i] where rover i is contained in set auxrLoading . Elementary scenario type ReturnHandler (Listing 11) specifies the return conditions and the associated commands from the command centre to the rovers. Again, this is a simulation scenario, as explained in Section 2. Return commands will be finally sent to all rovers that are still part of the (dynamically changing) system test configuration. This is checked by condition r[i] ̸= null: a rover that is no longer existent will be marked by r[i] = null in the collaboration part of the configuration. The LTL formula in lines 3 and 4 specifies that return commands will be immediately sent to any rover that has loaded its designated item to be salvaged (it is then in state itemLoaded) or that is stuck or broken. In the latter cases it is unclear whether the robot will still be able to execute the return command, but the command is at least issued by the centre. A return command returnToDst to rover r[i] is associated with a destination value returnDst[i] which is a predefined constant. The second LTL formula in lines 5 to 10 specifies return commands to rovers that are still operative, approach the target destination or have already arrived there. These rovers are commanded to return if they are no longer needed, because all items to be salvaged are already being transported by other rovers. Listing 11: Handler for rovers that should return to a specified destination. elementary scenario ReturnHandler( cc : CommandCentre, r : Rover[n] ) V 3 spec G r[i] = ̸ null ⇒ (r[i].s ∈ {stuck, fault, itemLoaded} ⇒ i:0..(n−1)
4 X(cc.cmd[i] = returnToDst ∧ cc.dst[i] = returnDst[i])) ; V 5 spec i:0..(n−1) G r[i] ̸= null ⇒ 6 (r[i].s ∈ {approaching, atDst} ∧ 7 numRovers(r, {itemLoaded}) + 8 numRovers(r, {returningWithItem}) + 9 numRovers(r, {returnedWithItem}) = m ⇒
10 X(cc.cmd[i] = returnToDst ∧ cc.dst[i] = returnDst[i])) ; 11 initact frame := {cc.cmd[i], cc.id[i] | i = 0, . . . , (n − 1)}; 12 end scenario 1 2

20

The effect of rovers entering exclusion zones is specified by scenario type MishapHandler. Such robots have to be removed from the system test collaboration, since they are no longer existent. This is expressed by the change condition and action in line 3 of the scenario: when a robot enters an exclusion zone for the first time, action delete(r) is performed on the collaboration coll. This resets the reference r to the rover to null and deletes all interfaces connecting r-parameters to parameters of any other object. After this, the scenario is terminated, as specified by the LTL formula in line 2. Listing 12: Mishap handler scenario. elementary scenario MishapHandler( r : Rover, coll : collaboration
) spec G inExclusionZone(r.pos, exclusionZone) ⇒ X¬active ; 3 cndact when ( inExclusionZone(r.pos, exclusionZone) )/coll.delete(r); 4 end scenario 1 2

Scenario for checking emergent properties. The evaluation of pass criteria for a system test is also specified in one or more elementary scenario types. For the test discussed here, the pass criteria are specified in the EmergentPropertyChecker scenario type in Listing 13. For a test to pass, 1. at least m rovers shall arrive at the salvage destination before time tatDst , and 2. at least k rovers shall return with a salvaged item before time tend . The system test is terminated at time tend + 10. The built-in variable t̂ denotes the current test execution time, starting with zero when the test execution begins. Listing 13: Emergent property checker. elementary scenario EmergentPropertyChecker( r : Rover[n] ) spec (t̂ < tatDst ) U (numRovers(r, {atDst, itemLoaded, returning, 3 returningWithItem, returned, returnedWithItem}) ≥ m); 4 spec (t̂ < tend ) U (numRovers(r,
{returnedWithItem}) ≥ k); 5 spec G t̂ = tend + 10 ⇒ XEoT ; 6 initact frame := ∅; 7 end scenario 1 2

Remark – specification of object behaviour. Note that in principle, preconditions and behavioural specifications can also be defined for object types – this is syntactically and semantically well-defined. However, object type behaviours should only be defined if they hold in every elementary scenario 21

instance an object is involved in. For the system test example discussed here, we could not identify any behaviours that would hold in arbitrary operational situations. We suspect that this is very likely to hold in most scenario-based test specification for cyber-physical systems. 3.8. System Test Configuration and Deployment A system test configuration represents a composite scenario: it specifies how SUT objects and instances of elementary scenarios should interact to perform a system test. For the system test described in Section 2, the configuration is shown in Listing 14. Listing 14: System test configuration. systemtest coll : collaboration 3 r : Rover[n]; 4 cc : CommandCentre; 1 2

5 6 7 8 9 10

interface Is[i] from r[i].s to cc.s[i] for i : 0..(n − 1); interface Icmd [i] from cc.cmd[i] to r[i].cmd for i : 0..(n − 1); interface Idst[i] from cc.dst[i] to r[i].dst for i : 0..(n − 1); interface Iid [i] from cc.id[i] to r[i].id for i : 0..(n − 1); end collaboration

11 12 13

schedule   ∥i:0..(n−1) Approach(coll.r[i],startPos[i]);Pickup(coll.r[i]);Return(coll.r[i]);

∥i:0..(n−1) ApproachHandler(coll.cc,coll.r[i],i) ∥i:0..(n−1) MishapHandler(coll.r[i],coll) 16 ∥ PickupHandler(coll.cc,coll.r) 17 ∥ ReturnHandler(coll.cc,coll.r) 18 ∥ EmergentPropertyChecker(coll.r) 19 end schedule 20 end systemtest 14

15

The collaboration. The collaboration part of our system test specification introduces n robots r[i], i : 0..(n − 1) of object type Rover and one command centre cc of type CommandCentre. Object types are similar to classes in programming languages. The interfaces declared in a collaboration specify how output parameters of certain objects are mapped to input parameters of others. For example, interface Is[i] specifies that the output parameter s (for “status”) of rover r[i] is mapped to input parameter s[i] of the command centre cc (cc.s is a status 22

array of length n). Since all objects collaborating in a system test operate in a cyclic mode, the semantics of the interface mappings is fairly easy: • A new parameter value written to s by r[i] in cycle p becomes visible at cc.s[i] at the start of r[i]’s execution cycle p + 1. • If cc operates with a slower cycle time than r[i], then the most recent value written by r[i] to s becomes visible at the start of cc’s next cycle, so previous writes may be lost. • If cc cycles faster than r[i], it may read the same value several times (interfaces are like shared variables). • If two objects communicate over a communication medium that needs more time than a single cycle to deliver new values to their destination, an auxiliary object with a slower cycle time has to be introduced. This object represents the communication medium. An essential characteristic of system tests for interacting autonomous robots7 is that the collaboration may change during the test execution. In the example discussed here, robots can get lost when inadvertently entering an exclusion zone. In other system tests, new robots might enter the collaboration or leave it in an orderly fashion. Therefore, collaborations are semantically represented as abstract data types allowing operations like 1. coll.delete(r[k]). Delete rover r[k] from the collaboration, including all interfaces r[k] contributes to. The deletion is marked by setting coll.r[k] = null. This helps to check in elementary scenarios whether a robot still exists in the collaboration. 2. coll.create(r[n + ℓ] : Rover). Extend the collaboration by a new rover object that is registered under the new array index n + ℓ.8 3. coll.create(interface Is[n + ℓ] from r[n + ℓ].s to cc.s[n + ℓ]) creates a new interface in the collaboration. These operations are atomic, so the collaboration abstract data type acts like a monitor. This is necessary since several concurrent elementary scenarios may request configuration changes simultaneously during their execution. 7

or, for systems of systems in general [5] Arrays in SCSL are variable-size containers whose elements can be accessed via indexes, similar to ArrayList objects in Java. 8

23

Remark – auxiliary objects. The robotic system test example discussed here does not require auxiliary object types (Section 3.5) for communicating test execution data between elementary scenarios. If needed, instances of auxiliary object types and interfaces between such objects are declared just as SUT-related objects in the collaboration section. The schedule. The schedule part of a system test configuration specifies the test execution by means of elementary scenario instances that are sequentially composed or run in parallel. For example, Approach(coll.r[i],startPos[i]) specifies an instance of elementary scenario type Approach(. . . ), where the formal parameter r has been substituted by the concrete rover instance coll.r[i] that is part of the collaboration. Concrete parameter startPos[i] is an element of a constant array specifying the starting positions from where each rover commences its salvage expedition. After Approach(coll.r[i],startPos[i]) has terminated, scenario instance Pickup(coll.r[i]) can execute, after which instance Return(coll.r[i]) runs. This sequential execution of three elementary scenarios is performed concurrently for each rover coll.r[i], i : 0..(n − 1). In a similar way, instances of the remaining elementary scenarios are specified to be executed concurrently. System test deployment denotes the task of mapping the logical components of a system test – these are identified in the system test configuration – to software procedures, threads, processes, hardware interfaces, and processors. The details of system test deployment are beyond the scope of this paper, but we indicate some important concepts and variants. Coordinator Agent CA

Interface-Stubs

Interface-Stubs 1

Interface-Stubs 2

: further RoverSW instances and their handlers and simulations

EmergentPropertyChecker

Figure 3: Instantiation of Fig. 1 for the ‘software-only’ system test deployment.

24

Deployment variant ‘software only’. System tests like the one described in this paper are usually quite costly to be performed in the real world. Therefore, tests are usually performed in several phases, each phase using a different deployment. The first test phase is typically “software only”, where no target hardware is involved. In this setting, the original equipment OE0 , OE1 , . . . consists only of the software of the command centre and the robots, as sketched in Fig. 3 which specialises the generic test configuration diagram of Fig. 1 for the software-only deployment of our system test. The communication interfaces of each robot are stubbed, since the hardware interfaces and peripherals are not available in the software-only configuration. This allows to realise the interface declarations shown in the system test configuration by shared variables, procedure calls, socket communication, or similar means of data exchange between software components. Consequently, any deployment requires a specification explaining how the interfaces identified in the system test configuration should be implemented. Also, since the OE software does not run on original hardware, a deployment configuration needs to map the OEi to processors available for the software test execution.9 Since the hardware peripherals are missing in the software-only deployment, their feedback to the OE needs to be simulated. For example, each rover’s outputs to motors setting wheel angles and wheel speed is caught by a software simulation (see SIM1 in Fig. 3) that calculates the rover’s position changes that would result from these motor actuations in the real world. The calculated positions would be passed to the rover software, simulating satellite positioning information that would be received in the real world. The original equipment harnesses OEH0 , OEH1 . . . each execute a subset of the elementary scenario instances identified in the system test schedule. For instance, OEH0 , the handler for the command centre, would execute ∥i:0..(n−1) ApproachHandler(coll.cc,coll.r[i],i) ∥ PickupHandler(coll.cc,coll.r) ∥ ReturnHandler(coll.cc,coll.r), 9

For example, the software-only tests could be executed in the cloud, and each OEi could be encapsulated in a separate docker container that is executed in a Kubernetes POD of its own, see https://kubernetes.io/docs/concepts/workloads/pods/.

25

while the rover-specific OEHi , i = 1, 2, . . . would execute   Approach(coll.r[i],startPos[i]);Pickup(coll.r[i]);Return(coll.r[i]); ∥ MishapHandler(coll.r[i],coll). A global scenario execution unit executes the EmergentPropertyChecker(coll.r) instance. The coordinator agent monitors requested changes of the collaboration and provides the actual collaboration state to all elementary scenario instances under execution. Deployment variant ‘real-world’. For testing the salvage mission described above in the real world, the OE instances consist of the command centre, the complete robots (hardware with embedded software), the real communication service (for example, satellite-based or radio-based message exchange), and the real location service (e.g. GPS or Galileo). The only simulation left in a fully automated real-world system test would mimic users in the command centre initiating the salvage mission, as all physical hardware, sensors, and communication channels are real. 4. The SCSL Tool Platform The SCSL Tool Platform consists of two main components. The first component is responsible for the generation of test artifacts from SCSL specifications, including test suites, runtime monitors, executable oracles, and simulations. A single specification language is used to derive these different artifacts, enabling a unified and consistent development process. In particular, LTL-based runtime monitors and executable oracles are used to assess the correctness of the SUT during execution. Oracles are executed in parallel within test executions to verify the observed behavior of the SUT, while simulations actively stimulate the SUT to trigger additional state transitions and expose potential failure behavior. The second component of the SCSL Tool Platform is a cloud-based execution environment that orchestrates simulations, oracles, and test executions against the SUT. This environment is based on a time-synchronised, UDP-based, eventually consistent shared-state communication model for distributed runtime verification. It is composed of multiple agents, each deployed as a Docker container10 . Depending on its role, an agent may execute 10

Docker is a virtualisation engine that enables applications to run in lightweight,

26

a simulation, an oracle, a test executor, or provide a virtualised environment for running the SUT software. Inter-agent communication follows a blackboard-style architecture implemented as a time-triggered shared communication state. Each agent continuously publishes its output state as JSON11 -encoded messages via UDP multicast over a Docker MACVLAN network12 . Incoming messages are received asynchronously and aggregated into a local input state. At each global time tick, agents create a snapshot of this input state, which is then used for deterministic local evaluation. Both components are described in more detail in the following sections. 4.1. SCSL-Based Test Artifact Generation The SCSL Artifact Generator follows a three-layer architectural paradigm. In the first layer, a parser processes the scenario specification files, including scenario definitions, scheduling rules, and variable/class type declarations. As output, the parser produces a structured intermediate representation consisting of • a set of elementary scenario specifications, • a set of instance specifications, • a directed acyclic graph of scenario scheduling rules and • a set of typed variable definitions. portable containers with all their dependencies isolated from the host system; for reference visit https://www.docker.com/ 11 JSON (JavaScript Object Notation) is a lightweight, text-based data exchange format based on key–value pairs; for reference, see https://www.json.org/ 12 MACVLAN is a special Docker network driver that assigns each container a unique MAC address, allowing it to appear as a device on the physical local network without significant virtualization overhead, thereby enabling fast, near real-time communication; for reference, see https://docs.docker.com/engine/network/drivers/macvlan/

27

Figure 4: SCSL-Based Test Artifact Generation Workflow

In the second layer, each parsed scenario specification is transformed into a formal behavioral representation. For each scenario, the associated precondition and behavioral constraints are combined into a temporal logic specification. In particular, whenever the defined precondition is satisfied, all associated behavioral specifications are required to hold in the subsequent time step. This relationship is formalised as: ! ^ ϕscsl ≡ precondition ∧ X specificationi i

Note that at this stage, only the scenario specification and the precondition are considered; condition/action items and scenario parameters are not yet incorporated. Condition/action items are evaluated later during test generation, simulation execution, or oracle evaluation, while scenario parameters are handled in a subsequent step. The resulting formula ϕscsl is then abstracted into a propositional form ϕscsl-abstracted , where complex expressions and function calls are replaced by atomic Boolean propositions, as in the example shown below.

28

⇒

  ϕscsl = (x > 0) ∧ X (x = z) U (x < 100)
ϕscsl-abstracted = p0 ∧ X p1 U p2

This step of propositional abstraction mapping enables automated synthesis using standard linear temporal logic (LTL) tools. Subsequently, the well-known tool ltl3ba [13] is used to translate the abstracted LTL formula into a Büchi automaton. The resulting automaton is then analysed by the SCSL Artifact Generator to construct an internal symbolic Büchi automaton. More precisely, ltl3ba outputs a Hanoi ω-Automaton (HOA) representation of the Büchi automaton corresponding to ϕscsl-abstracted . This representation is parsed using the HOAF parser library13 . During this step, the atomic propositions associated with each transition are mapped back to their corresponding concrete expressions, yielding a symbolic Büchi automaton with transition guards represented as quantifier-free first-order expressions. Based on the instance specifications defined in the scheduling rules, concrete scenario instances are created by instantiating elementary scenarios with unique instance identifiers and parameter assignments. Each instance therefore represents a parameterised realisation of a scenario template. To ensure correct usage of scenario parameters during execution, parameter assignments are systematically integrated into the behavioral model. In particular, the conjunction of all parameter variable assignments associated with an instance is incorporated into each transition guard of the corresponding symbolic Büchi automaton. As a result, transitions are only enabled when both the original behavioral conditions and the instance-specific parameter constraints are satisfied. This guarantees that the behavior of each instantiated scenario is evaluated consistently with respect to its parameterisation. These instances form the nodes of a scheduling graph, which is constructed according to the dependencies and ordering constraints specified in the scheduling rules. The graph is rooted in a designated start scenario instance and terminates in one or more end scenario instances, thereby defining a complete execution flow from system initialisation to a target end condition. Intermediate nodes represent scenario instances whose execution is governed by scheduling rules that define ordering, branching, and dependency 13

https://automata.tools/hoa/cpphoafparser/

29

relationships. These rules guide the progression of the test execution by determining which scenario instances may follow a given state and under which conditions they are activated. As a result, the scheduling graph encodes not only structural dependencies but also the permissible execution paths through the system under test.

sc0

sc1

sc2

sc4

sc3

sc5

Figure 5: Example Scheduling Graph, sc4 and sc5 are End-Scenarios.

The resulting graph defines how and when individual scenario instances are executed at runtime, thereby enabling the controlled and coordinated execution of multiple interacting scenarios. In this way, the scheduling graph serves as the foundation for end-to-end test generation, ensuring that generated test executions follow well-defined paths from a start scenario to a corresponding end scenario while respecting all specified behavioral and scheduling constraints. In the third layer, the previously constructed symbolic Büchi automaton and the scheduling graph are processed to derive executable artifacts. This layer comprises two main components: • test case generation and • simulation and oracle generation. This is described in more detail in the next sections. 4.1.1. Test Generation The test generator systematically explores the scheduling graph by traversing all possible paths from the designated start scenario instance to the corresponding end scenario instances. Each path represents a valid end-to-end 30

execution sequence and is therefore considered for test generation. Even paths that differ only in a single transition are explored independently to ensure coverage of all possible execution combinations. For each path in the scheduling graph, the corresponding sequence of scenario instances is considered. Each scenario instance is represented by a symbolic Büchi automaton. In cases where multiple scenario instances are active concurrently, multiple symbolic Büchi automata are considered in parallel. Each elementary scenario is additionally associated with its own set of condition/action items, which are preserved during instantiation and therefore also present in the corresponding scenario instances. These condition/action items follow a guarded-command semantics, where execution is defined by the evaluation of a predicate over the current state and scenario variables. More precisely, each transition is associated with a guard, a condition, and a set of actions that update temporary variables. A transition is enabled if the conjunction of its guard, condition, and the current valuation of temporary variables is satisfied. If this evaluation yields true, the corresponding actions are executed and may update the temporary variable state, thereby influencing subsequent transition evaluations. This corresponds to a symbolic guarded transition system with state updates, where transitions are defined in the form of guarded commands of the type "if condition then update state". In this work, this semantics is adopted based on the C-Language, where statements are executed sequentially after the condition becomes true, adapted to a symbolic and SMT-solved execution setting. This mechanism allows the system to express control-flow-like behavior within the formal execution model while maintaining compatibility with symbolic evaluation using SMT solving. Test generation proceeds by exploring the transitions of the involved symbolic Büchi automata starting from their initial states in a depth-first search (DFS) order. Test generation and execution for a given scenario instance only start once its corresponding precondition is satisfied. From that point on, the symbolic Büchi automaton of that instance is traversed in DFS order. If the precondition is not satisfied, the corresponding execution path is not explored and no transitions are traversed for that instance. This mechanism ensures that scenario execution is context-dependent and only activated under valid conditions. Within active executions, transitions are evaluated based on their guards together with associated condition/action items and the current temporary 31

variable state. The traversal aims to cover relevant behavioral paths, in particular those leading to accepting states. This results in a set of symbolic execution paths characterised by transition guards. Concrete test cases are obtained by solving the accumulated transition constraints along these paths using Microsoft’s Z314 SMT solver. The resulting variable assignments constitute concrete input stimuli for the system under test. Output validation is not embedded in the generated test cases, as correctness is verified separately using runtime oracles. Consider the symbolic Büchi automaton in Figure 6. Variables z and x are both output variablues while p0 is a parameter of the scenario and set to p0 := 42 in this instance. The test generation algorithm yields a test suite consisting of two test cases, as shown in Table 1 (Test Case 1) and Table 2 (Test Case 2).

s0

z = 0 ∧ x = p0 ∧ p0 = 42 z = 1 ∧ x = p0 − 25 ∧ p0 = 42

s1

z = p0 ∧ x = 1 ∧ p0 = 42 accept

Figure 6: Example symbolic Büchi automaton.

Step 1

Transition s0 → accept

Transition Expression z = 1 ∧ x = p0 − 25 ∧ p0 = 42

Concrete Valuation {z := 1, x := 17, p0 = 42}

Table 1: Test Case 1: Direct transition s0 → accept

The resulting test suite is serialised into a structured JSON representation, which enables persistence, interoperability, and execution within the 14

https://www.microsoft.com/en-us/research/project/z3-3/

32

Step 1 2

Transition s0 → s1 s0 → accept

Transition Expression z = 0 ∧ x = p0 ∧ p0 = 42 z = p0 ∧ x = 1 ∧ p0 = 42

Concrete Valuation {z := 0, x := 42, p0 = 42} {z := 42, x := 1, p0 = 42}

Table 2: Test Case 2: Transition s0 → accept

distributed runtime environment. The SUT must pass both test cases of the test suite in order to pass the scenario specification. 4.1.2. Simulation and Oracle Generation Simulation and oracle artifacts are generated by transforming the symbolic Büchi automaton, together with condition/action specifications, into executable C++ code. Through the Jinja2-based15 code generation process, each automaton is compiled into a dedicated C++ class that encapsulates all input variables, constants, and scenario parameters as private member variables. Input variables are updated via external interface calls, while scenario parameters are refreshed at each iteration of the execution loop. The transitions of the symbolic Büchi automaton are directly mapped to C++ conditional statements. In particular, each transition guard is translated into an if-condition over the private member variables (e.g., x > 0). If a guard evaluates to true, the corresponding transition is executed, including state updates and optional output actions. Output variables are written via a write() function, which forwards data through a configurable wrapper interface to other agents, enabling flexible deployment across different execution environments. In the cloud-environment, the data is serialised to JSON packages and sent via UDP multicast. Each automaton state is stored as a private member variable within the generated class and is evaluated inside a cyclic main loop implemented using a switch-case structure. Importantly, for oracles, the resulting execution model does not require any external constraint solving or runtime SMT reasoning. All transition decisions are resolved through direct evaluation of compiled C++ boolean expressions, resulting in a lightweight and highly efficient execution mechanism with predictable constant-time guard evaluation. In contrast, simulation requires the use of an SMT solver to evaluate the 15

https://jinja.palletsprojects.com/en/stable/

33

outputs of the system under test (SUT) and to determine the subsequent transition to be taken. Furthermore, the SMT solver is used to compute the expected system responses, thereby generating appropriate outputs of the simulation in reaction to the observed SUT behavior. The generated SCSL-Based Simulation utilises the SMT-Solver Microsoft Z316 . Each oracle or simulation instance follows a uniform execution scheme. First, the corresponding class is instantiated. During runtime, scenario parameters are re-initialised at each iteration of the main loop, ensuring that parameter-dependent behavior remains consistent with the scheduling semantics. Execution remains idle until the precondition of the specification becomes satisfied. Once activated, the system enters its main evaluation loop. In each iteration, a snapshot of the current input state is taken, and all outgoing transitions of the current active states are evaluated sequentially. If a transition guard evaluates to true, the corresponding action is executed and the automaton transitions to the next state. Importantly, the nondeterminism inherent to Büchi automata is explicitly preserved within this evaluation scheme. When multiple outgoing transitions are enabled simultaneously, the system does not enforce an arbitrary deterministic choice. Instead, the execution maintains a set of active states, exploring all valid continuation candidates in parallel. If a specific state within this set fails to provide a suitable outgoing transition for the current input, it is pruned. Should the state set become empty, it indicates that the SUT has deviated from the behavior specified by the test oracle, signaling a violation of the acceptance conditions. 4.2. Cloud-Based Execution Environment The second component of the SCSL Tool Platform is a cloud-based execution environment that orchestrates simulations, oracles, test executions, and the SUT within a unified distributed runtime infrastructure. The environment is designed as a time-synchronised, UDP-based, eventually consistent shared-state communication system for distributed runtime verification. The environment is designed as a time-synchronised, UDP-based, eventually consistent shared-state communication system for distributed runtime verification, following related approaches in multi-agent and distributed monitoring 16

https://www.microsoft.com/en-us/research/project/z3-3/

34

frameworks [14, 15]. 4.2.1. Local Agent Execution Model Each agent in the execution infrastructure is realised as a self-contained runtime component generated from a symbolic Büchi automaton using a Jinja2-based code generation pipeline. The resulting C++ implementation encapsulates the complete automaton logic, including all input variables, constants, and scenario parameters, as private member variables within a dedicated class. This design ensures strict encapsulation of the execution state and enables deterministic behaviour across distributed deployments. The generated automaton is executed using a two-threaded runtime model. A dedicated receiver thread is responsible for continuously processing incoming UDP multicast messages. These messages contain JSON-encoded state updates from other agents and are merged into the agent’s local input state representation. This thread maintains the most recent view of the distributed system and ensures that the input state is continuously updated asynchronously with respect to the execution logic. In parallel, an execution thread performs the actual automaton evaluation. At each iteration of a cyclic main loop, the current input state is accessed as a snapshot, ensuring temporal consistency during evaluation. Scenario parameters are re-initialised at the beginning of each loop iteration to reflect the scheduling semantics of the system. Each agent initially remains in an idle state until its associated precondition becomes satisfied. Once activated, the execution thread continuously evaluates the automaton in a loop, processing transitions based on the latest snapshot of the input state provided by the receiver thread. This separation of communication and execution ensures both responsiveness to distributed state changes and deterministic local behaviour. 4.2.2. Time-Synchronised Distributed Agent Execution Model The execution infrastructure follows a homogeneous agent-based design. Each component, including the SUT, test executor, oracle, and simulation engine, is deployed as an independent agent within a Docker container. All agents adhere to a common execution ontology, meaning that they share a uniform representation of state, time, and message semantics, regardless of their specific role. This enables interchangeable interaction patterns between testing, simulation, and verification components.

35

Inter-agent communication is implemented using a blackboard-style architecture based on a globally synchronised time tick. At each time step, agents publish their local output state as JSON-encoded messages via UDP multicast over a Docker MACVLAN network. Incoming messages are received asynchronously and merged into each agent’s local input state. To ensure deterministic evaluation, all agents take a consistent snapshot of the current input state at each global time tick before performing local computation. At each global time tick, the system evolves in a strictly synchronised sequence of operations. First, each agent acquires a snapshot of its current local input state, ensuring that all computations are performed over a consistent view of the distributed system. Based on this snapshot, every agent then evaluates its local transition function, which determines the next control state and the corresponding output actions. Subsequently, agents emit their output messages via UDP multicast in JSON-encoded form. These messages are disseminated to all other agents participating in the system. Finally, all incoming messages are merged into the respective input states of each agent, forming the basis for the next time step. This cycle defines the discrete-time evolution of the overall distributed system. At the top level, a dedicated coordinator component is responsible for orchestrating distributed test execution. The coordinator initialises all executor agents using a test execution configuration, which specifies the location of the test suite and binary artifacts in an external object store (e.g., a MinIO-based S3-compatible storage system17 ). Once initialisation is complete, all agents are synchronised and start execution simultaneously at a globally defined start time, using a shared logical clock. During execution, test cases are transmitted as stimulation inputs by the test executor via UDP multicast in JSON format over the MACVLAN network. The SUT, oracles, and simulations process these inputs uniformly using the same communication and state update mechanisms. This ensures that all runtime components operate on a consistent semantic model of system behaviour. Throughout the test run, execution status and intermediate verdicts are continuously monitored and displayed in a test management interface. Upon completion, each agent uploads its execution logs and final verdicts to the 17

https://www.min.io/

36

object store. Finally, all agents are reset to their initial state, enabling reproducible re-execution of test campaigns under identical conditions. 5. A System Test Example The SUT comprises three autonomous rovers tasked with retrieving three items within a bounded environment containing designated exclusion zones. The rovers operate on a two-dimensional Euclidean plane, where the state of each rover i is defined by its coordinates (xi , yi ). Similarly, each target item j is assigned a static position (xj , yj ) within the operational area. 5.1. Test Configuration and Setup The test setup is implemented as a set of communicating Docker containers comprising the simulation components, oracle, test suite execution environment, and the SUT, interconnected via a MACVLAN network and UDP multicast, as illustrated in Figure 7. The overall test execution is divided into an initialisation phase and an execution phase. During the initialisation phase, items and exclusion zones are distributed across the operational field.

Figure 7: The Architecture of the System Test Execution.

An excerpt of the test suite is shown in Listing 15. These placements are defined as parameterised scenarios within a sequential composition: target items are positioned first, followed by the delineation of exclusion zones, as shown in Figure 8.

Figure 8: Test Suite Schedule.

37

The simulation remains in a paused state until the simulation_start signal is issued by the sendSimulationStart scenario. Upon activation, the ApproachHandler, ReturnHandler, and PickupHandler initiate execution in coordination with all rover-specific scenarios, as governed by the predefined schedule. Throughout the mission, the Emergent Property Monitor continuously audits the system state for any property violations. Listing 15 shows the test configuration in JSON format. This representation is not the original SCSL specification, but an internal representation of the initialisation scenario. Listing 15: Excerpt of the Initialization Phase (Scenario 1). { " name ": " Scenario -1 - Initialization " , " stimulation ": { " set_item1 ": true , " set_item1_x ": 5 , " set_item1_y ": 5 , " set_item2 ": true , " set_item2_x ": 6 , " set_item2_y ": 6 }, " e x p e c t e d _ o b s e r v a t i o n s ": { " condition ": "" } }

5.2. Scenario: GPS-Induced Navigation Failure To evaluate realistic system behaviour, a GPS signal glitch is simulated. The test is considered passed if at least two of the three rovers survive and all items can be salvaged. This setup allows assessment of the system’s response when a rover receives erroneous position data, subsequently enters an exclusion zone, and becomes unavailable. In such cases, the command centre is expected to reassign the task by selecting an alternative rover to collect the respective item. The scenario is activated under the condition that the rover under consideration is not already located within an exclusion zone and is currently in the Approaching state, i.e. navigating towards a designated item. Once these preconditions are met, the GPS glitch is introduced. Upon reaching the glitch timestamp (i.e., a predefined future time at which a GPS glitch is introduced), the rover’s reported position remains static, while the test engine continues to track its true position. As the rover assumes a standstill situation, it continues driving until it enters an exclusion zone. This condition persists until a predefined glitch counter reaches a specified maximum threshold, which is provided as a configurable parameter.

38

Listing 16: Scenario for Simulating GPS Glitch. 1

elementary scenario GPSGlitch( r : Rover, glitchTime : t, glitchCntMax : R )

2 3 4 5

spec G (¬inExclusionZone(r.pos, exclusionZone) ∧ r.s = approaching)
⇒ Xactive ;
spec G (glitchCnt = glitchCntMax) ⇒ X¬active

6 7 8 9 10

initact frame := {r.pos}; glitchCnt := 0 cndact [t = glitchTime]/glitchPos := r.pos cndact [t > glitchTime]/r.pos := glitchPos; glitchCnt = glitchCnt + 1 end scenario

This scenario is instantiated with Rover 3. The glitch time is defined to 5, while the maximum value of the glitch counter is set to 3. The rover is considered to go to item (5, 7) in forward direction, so heading a exclusion zone at (5, 4). From the timestamp of 5 seconds after start, its reported position becomes artificially frozen, meaning that further movement is no longer reflected in the received GPS signal, despite the rover potentially continuing its internal navigation process. This discrepancy persists in a time-dependent manner and is regulated by a glitch counter mechanism. The counter increments with continued operation under faulty signal conditions until it reaches the predefined maximum value of 3. Note that the test engine receives the true position of the rover while the rover receives the faulty position. Once this limit is reached, the rover continues to assume correct localisation despite the underlying GPS fault. As a result, it believes it remains on its intended trajectory, while its actual position may already be within an exclusion zone that should have been avoided. Due to the faulty trajectory information, this deviation is not detected in time, leading to a violation of the exclusion zone constraint. Listing 17: Scenario Instance for Simulating GPS Glitch 5 seconds after start. 1 2

instance gpsGlitch of scenario GPSGlitch( r := rover3, glitchTime := 5, glitchCntMax := 3 );

As can be observed in the scenario execution in Listing 18, the position of Rover 3 is held constant at (5, 1) once the GPS glitch is triggered. Despite this apparent stalling in the reported localisation, the rover remains in the Approaching state throughout this phase, as the high-level behavioural state is not immediately affected by the corrupted position updates. 39

Listing 18: Output of the System Test with GPS Glitch. [GPS] Simulate fault for Rover 3 [GPS] Rover 3 True(5,1) GPS(5,1) 3 [17:28:01.147] [INFO] Rover 3 Pos (5,1) (State: APPROACHING) 4 [17:28:01.647] [INFO] Rover 3 Pos (5,1) (State: APPROACHING) 5 [17:28:02.149] [INFO] Rover 3 Pos (5,1) (State: APPROACHING) 6 [17:28:02.650] [INFO] Rover 3 Pos (5,4) (State: DEAD) 7 [17:28:07.344] [CommandCentre] Reschedule Item 1 (5, 7) to Rover 2 1 2

The rover continues to operate under the assumption of valid navigation data until the glitch counter reaches its configured maximum value. At this point, normal GPS functionality is restored. However, due to the accumulated discrepancy between the rover’s actual trajectory and its previously frozen reported position, the system updates cause an abrupt correction in localisation. Upon detecting its true position within this exclusion zone, Rover 3 transitions into a failed operational state and actively reports its dead state to the command centre. This notification indicates that the rover is no longer capable of participating in mission execution. Consequently, the system classifies Rover 3 as unavailable for further task allocation, and higher-level coordination logic is triggered to reassign the affected task to an alternative rover (here: Rover 2, as shown in Listing 18). Additionally, it can be observed that, until the end of the system test, the oracle evaluations associated with this rover – namely the Return oracle and the Pickup oracle – reach a passed state, as shown in Listing 19. This can be attributed to the rover’s entry into an exclusion zone. Listing 19: Output of the Oracles during GPS Glitch Test. [Approach3-ORA] PASS. [Pickup3-ORA] PASS. 3 [Return3-ORA] PASS. 1 2

The successful oracle resolution can be attributed to the system’s correct handling of the rover’s disrupted operational lifecycle following the simulated GPS glitch and its transition into the exclusion zone. Despite Rover 3 being unable to complete the original task, the system adapts appropriately, resulting in both the pickup oracle and return oracle reaching a passed state. As a result, both oracles converge to a successful verification outcome, indicating that the expected behavioural criteria have been satisfied. Furthermore, all items were successfully salvaged and the minimum required number of rovers remained operational. Consequently, the overall system 40

test for Rover 3 is considered passed. The system test took 75 seconds for execution. 5.3. Parameter Sensitivity To evaluate the effectiveness of the EmergentPropertyChecker (Listing 13), we conducted a sensitivity analysis by varying the temporal and spatial parameters of the initialization scenarios. The property defined in the specification establishes mission-critical deadlines and throughput requirements. By systematically decreasing the parameter tatDst (Time at Destination from start) while increasing the spatial distance of target items, we identified the operational boundaries of the rover swarm. Table 3: Impact of Parameter Variation on Property Verification.

Test ID T-1 T-2 T-3 T-4

Target Dist. 5 steps 15 steps 15 steps 25 steps

Deadline (tatDst ) 20s 20s 10s 20s

Verdict PASS within assumptions PASS within assumptions FAIL: Temporal Violation FAIL: Temporal Violation

The results demonstrate that the test suite successfully passed under the nominal operational assumptions, where the allotted time tatDst was sufficient for the rovers to traverse the Euclidean distance to the items. Conversely, the framework correctly issued a FAIL verdict when the parameters were pushed beyond the physical capabilities of the robots, such as in T-3 and T-4. 5.4. Experimental Evaluation The experimental evaluation indicates a highly efficient end-to-end workflow for the generation and execution of scenario-based system tests. In particular, the derivation of oracles and simulation artefacts directly from the specification was completed in less than two seconds (Table 4), demonstrating minimal overhead in the transformation step from formal description to executable test components. Furthermore, the generated Oracle and Simulation C++ code could be compiled without significant delay, and the corresponding runtime environment was set up rapidly. This fast provisioning process enables an iterative testing workflow in which even small modifications to the specification can be translated into new executable tests with negligible turnaround time. As a 41

Table 4: Time to generate executable Oracles and Simulations from SCSL on a AMD Ryzen 7 PRO 5850U CPU.

Oracle/Simulation Approach Oracle Pickup Oracle Return Oracle Approach Simulation Pickup Simulation Return Simulation

Time 0.946s 0.977s 1.622s 0.556s 0.677s 1.142s

result, test execution and result retrieval can be performed in a highly responsive manner, supporting rapid experimentation and continuous refinement of scenarios, as shown in Table 4. In addition, preliminary experiments with simple baseline scenarios revealed a trajectory-following issue in cases where only a single feasible path exists around an exclusion zone. In such situations, the rover fails to correctly navigate along the constrained route, exposing a limitation in the current navigation behaviour. This observation demonstrates that the proposed approach is capable of uncovering non-trivial system faults even in seemingly simple scenarios, thereby highlighting its effectiveness for systematic error detection. In terms of system communication, the use of Docker-based isolation in combination with MACVLAN networking, and UDP multicast results in a very low communication overhead. This setup allows the distributed components of the test environment to exchange messages efficiently, with minimal latency introduced by the infrastructure layer below 2 ms. Empirical timing observations further suggest that message exchange operates in a near realtime manner, with no noticeable delays or disruption effects under normal test conditions. Overall, the measurements indicate that the proposed setup is well-suited for time-sensitive system testing, as it achieves both fast test generation and low-latency inter-component communication. 6. Related Work Early work in the road vehicle domain. Gipps [16] created a mathematical specification formalism for computer-based car-following simulation. Gipps’ 42

model captures the behaviour of a single vehicle in a traffic stream, specifically how it reacts to the vehicle in front. The model specifies each braking and acceleration action of the following vehicle. Building on Gipps’ work, the Intelligent Driver Model (IDM) [17] introduces time-continuous traffic flow scenario specification with environmental aspects. This enables the simulation of braking manoeuvres or minimum spacing between cars. This was further extended by additional physical simulations of longitudinal dynamics, expressed by the Optimal Velocity Model (OVM) [18]. OVM enables the dynamical adjustment of the acceleration after the lead vehicle brakes. The model uses mathematical equations to specify acceleration and braking values. Ulbrich et al. introduced fundamental formal definitions and examples for scene, situation and scenario, where a scene is considered as a snapshot of the environment including static and dynamic elements, a situation is defined as a context-specific scene and a scenario as a description of a temporal evolution of multiple scenes [19]. Hilscher et al. developed an abstract model using spatial interval logic to represent multi-lane roadways with potential lane changes of ego vehicles, called Multi-Lane Spatial Logic (MLSL). The formalism enables the verification of lane changes for a single vehicle in an environment with multiple ego vehicles, while a distance controller ensures safe spacing between vehicles [8]. Schwammberger [20] extended MLSL by incorporating property checks into the lane-changing controller for motorway scenarios, ensuring that undesirable events never occur, as initially proposed by Hilscher et al. [8]. Schwammberger implemented the line-change controller in UPPAAL to verify the implemented timed automaton and the line changing protocol. Damm et al. introduced Traffic Sequence Charts (TSC) as a formal and visual specification language for designing traffic scenarios in the context of autonomous vehicle testing [21]. Recent work uses TSCs for runtime monitoring of complex scenario-based requirements, thereby supporting scenario-based testing during execution [22]. TSCs are designed textually or visually, enabling structure-based validation to improve safety assurance by creating a scenario catalogue. For scenario specification of distributed event-based systems, Petri Nets [23] are employed to define scenarios in form of subsequent events. Petri Nets facilitate the formal description of system requirements which are then used as input models for test generation, as outlined in Sarmiento et al. [24]. Today’s scenario modelling is primarily graphics-based, like ASAM OpenSCENARIO [25], which is designed for the automotive domain, focusing on defining real-world traffic scenarios and simulating automotive components. 43

Simulations of traffic behaviours are then utilised to test automotive components. Recent trends. In the recent literature on scenario-based validation of cyberphysical systems (notably automated driving and, increasingly, automated railway systems), scenario descriptions are used predominantly as artefacts for testing/validation and runtime monitoring, and are typically embedded in domain-specific world models and toolchains. This is reflected, for example, by end-to-end scenario-based testing pipelines and scenario generation frameworks for automated driving [26, 27, 28] as well as closed-loop scenario-based simulation frameworks for highly automated railway systems [29]. Wide-spectrum scenario formalisms. In contrast to domain-tailored traffic scenario languages, there also exist wide-spectrum, domain-independent scenario modelling formalisms based on interaction/sequence specifications, for example message sequence charts and their executable variants such as Live Sequence Charts (LSCs). These formalisms are used beyond testing, e.g. for requirements specification, consistency checking, and synthesis of reactive behaviour from scenario-based descriptions [30]. In addition to that, there are several proprietary car traffic simulation platforms, such as PT-VISSIM [31], which is designed for trajectory modelling. Beyond automotive applications, the latest SysML V2 Standard [32] offers syntactic support for domain-independent test scenario definitions, based on occurrences, verification definitions, constraint definitions, interactions, and state machines. SysML V2 introduces enhancements over its predecessor to better support system-level modelling. The strengths of SysML V2 are in defining system interactions, state-driven behaviour and high-level operational scenarios. In the aviation sector, the graphical Aviation Scenario Definition Language (ASDL) [33] supports formal specification of comprehensive aircraft landing scenarios. Scenario specification is also explored through Time Modelling, particularly for system requirements verification. For example, the Clock Constraint Specification Language (CCSL) [34] translates specifications into clock graphs. These graphs facilitate constraint-solving using SMT solvers. Each existing scenario specification formalism has disadvantages: formalisms like ASAM OpenSCENARIO, IDM, or PT-VISSIM offer strong domain-dependent capabilities for behaviour specification and simulations 44

but lack support for behaviour simulation of arbitrary domains and test generation. On the other hand, SysML V2, Petri-Nets and the Clock Constraint Specification Language (CCSL) are primarily domain-independent, but lack a simple, expressive syntax. Additionally, they are not fully suitable for formal behaviour specification. While test and code generation is possible with these formalisms, it often requires significant resources. SCSL, however, offers a deliberately simple and expressive, scenariocentric syntax for formal system-test scenario specification. By leveraging existing formalisms from UML/SysML and VDM, the LTL syntax is extended by using condition-actions on state transitions and frames to restrict variable modifications. SCSL is intentionally designed to be domain-independent, supporting specification of re-usable, parametrised scenario models that can be assembled into domain-specific libraries. The state-based behaviour of LTL is a notable feature that enables straightforward test and code generation from specified scenarios. 7. Discussion 7.1. Conclusion We have introduced the domain-independent scenario specification language SCSL and illustrated its use for system test specifications verifying collaborating robots. Compared to other existing scenario modelling languages, in particular, those based on variants of UML and SysML, SCSL has a fairly simple syntax and a formal behavioural semantics that can be comprehensively specified with acceptable complexity in a compact way. Domain-specific support can be easily realised by introducing libraries of predefined types, objects, and elementary scenarios, the latter specifying typical behaviours of the application domain, such as physical laws applicable under specific environmental conditions or typical manoeuvres of the domainspecific objects. The usability of SCSL has been demonstrated by means of a system test example describing a salvage mission of collaborating robots. A major advantage of the formal SCSL semantics is that SCSL specifications can be automatically transformed into test data generators, executable simulations or into test oracles to be embedded into original equipment harnesses stimulating a system component under test and checking its reactions against SCSL specifications.

45

7.2. Future Work While this paper focuses on introducing the syntax and semantics of SCSL, the suitability and effectiveness of SCSL will be demonstrated in a case study using specifications from the EULYNX standard18 that has been designed for harmonising the communication between components of modern railway signalling systems in Europe. We will compare the effectiveness of SCSL to that of well-known model-based testing approaches that rely on comprehensive monolithic system models. Relevant evaluation criteria include modelling effort, reusability, scalability, requirements coverage, and fault detection capability. For example, mutation testing could be applied to assess the relative fault detection power of both approaches. In domains such as automotive or avionics, where MBT is well established, comparative studies will help determine whether scenario-based specifications offer measurable advantages in terms of productivity, maintainability, or test completeness. To the best of our knowledge, there is currently no comprehensive and domainindependent empirical study systematically comparing the effectiveness of scenario-based testing approaches—such as those enabled by SCSL—with classical model-based testing approaches relying on monolithic behavioural models. As such, we consider this a novel and promising direction for future work. To facilitate the creation of LTL specifications that are essential for describing the behaviour of a scenario, we plan to use LTL-specific generalised pre-trained transformers (GPTs) that are capable of creating LTL formulae from natural language specifications [35]. A recent publication by Peled et al. [36] indicates that this can be achieved with a very low failure rate. The automated generation can be complemented by mechanisms to detect erroneous LTL encodings with high probability.19 18

https://eulynx.eu/resource-hub-deliverables/ Suitable validation mechanisms range from automated procedures to others involving manual interaction. An example for automated validation is to let a GPT create witness traces for the created formula and its negation. Then it is checked by a verified algorithm that these witnesses indeed fulfil the formulae. An error in witness generation indicates that the GPT does not have the “correct understanding” of the formula semantics, so the text-to-formula transformation cannot be trusted. An example for validation involving manual interaction is to let engineers decide whether correct formula witnesses conform to their expectations expressed in the natural language specification. This manual process can be supported by letting a GPT transform witness traces of even the whole generated formula back to natural language. 19

46

As readers may have noticed, the essential feature of behavioural SCSL scenario specifications is that they can be interpreted on sequences of valuation functions whose values have been obtained from components operating with cyclic execution semantics. Consequently, the combined LTL and condition-action syntax is not the only way to write behavioural SCSL specifications. As an alternative, for example, RoboSim state machines20 [37] and similar discrete time formalisms could be used.

20

https://www.cs.york.ac.uk/circus/RoboCalc/robosim/robosim-reference.

pdf

47

References [1] J. Peleska, J. Brauer, W. Huang, Model-based testing for avionic systems – proven benefits and further challenges, in: T. Margaria, B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice - 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part IV, Vol. 11247 of Lecture Notes in Computer Science, Springer, 2018, pp. 82–103. doi:10.1007/978-3-030-03427-6\_11. URL https://doi.org/10.1007/978-3-030-03427-6_11 [2] F. Hauer, T. Schmidt, B. Holzmüller, A. Pretschner, Did we test all scenarios for automated and autonomous driving systems?, in: 2019 IEEE Intelligent Transportation Systems Conference, ITSC 2019, Auckland, New Zealand, October 27-30, 2019, IEEE, 2019, pp. 2950–2955. doi:10.1109/ITSC.2019.8917326. URL https://doi.org/10.1109/ITSC.2019.8917326 [3] K. G. Larsen, M. Mikucionis, B. Nielsen, Online testing of real-time systems using uppaal, in: J. Grabowski, B. Nielsen (Eds.), Formal Approaches to Software Testing, Springer Berlin Heidelberg, Berlin, Heidelberg, 2005, pp. 79–94. [4] S. D. Brookes, A. W. Roscoe, Deadlock analysis in networks of communicating processes, Distributed Comput. 4 (1991) 209–230. doi: 10.1007/BF01784721. URL https://doi.org/10.1007/BF01784721 [5] C. B. Nielsen, P. G. Larsen, J. S. Fitzgerald, J. Woodcock, J. Peleska, Systems of systems engineering: Basic concepts, model-based techniques, and research directions, ACM Comput. Surv. 48 (2) (2015) 18:1–18:41. doi:10.1145/2794381. URL https://doi.org/10.1145/2794381 [6] J. Peleska, F. Brüning, A. E. Haxthausen, W. Huang, Scenario-based system testing for distributed robotics applications - (invited paper), in: A. Cavalcanti, S. Foster, R. Richardson (Eds.), Towards Autonomous Robotic Systems - 26th Annual Conference, TAROS 2025, York, UK, August 20-22, 2025, Proceedings, Vol. 16045 of Lecture Notes in Computer Science, Springer, 2025, pp. 310–337. doi:10.1007/ 48

978-3-032-01486-3\_25. URL https://doi.org/10.1007/978-3-032-01486-3_25 [7] A. Cavalcanti, R. M. Hierons, Challenges in testing of cyclic systems, in: Y. Aït-Ameur, F. Khendek, D. Méry (Eds.), 27th International Conference on Engineering of Complex Computer Systems, ICECCS 2023, Toulouse, France, June 14-16, 2023, IEEE, 2023, pp. 1–6. doi:10.1109/ICECCS59891.2023.00010. URL https://doi.org/10.1109/ICECCS59891.2023.00010 [8] M. Hilscher, S. Linker, E. Olderog, A. P. Ravn, An abstract model for proving safety of multi-lane traffic manoeuvres, in: S. Qin, Z. Qiu (Eds.), Formal Methods and Software Engineering - 13th International Conference on Formal Engineering Methods, ICFEM 2011, Durham, UK, October 26-28, 2011. Proceedings, Vol. 6991 of Lecture Notes in Computer Science, Springer, 2011, pp. 404–419. doi:10.1007/ 978-3-642-24559-6\_28. URL https://doi.org/10.1007/978-3-642-24559-6_28 [9] J. M. Spivey, The Z Notation: A Reference Manual, 2nd Edition, Prentice Hall, New York, NY, USA, 1992. [10] C. B. Jones, Systematic Software Development Using VDM, PrenticeHall, 1986. [11] Object Management Group, OMG Unified Modeling Language (OMG UML), superstructure, version 2.5.1, Tech. rep., OMG (2017). [12] I. E. Sutherland, R. F. Sproull, R. A. Schumacker, A characterization of ten hidden-surface algorithms, ACM Comput. Surv. 6 (1) (1974) 1–55. doi:10.1145/356625.356626. URL https://doi.org/10.1145/356625.356626 [13] S. Mochizuki, M. Shimakawa, S. Hagihara, N. Yonezaki, Fast translation from ltl to büchi automata via non-transition-based automata, in: S. Merz, J. Pang (Eds.), Formal Methods and Software Engineering, Springer International Publishing, Cham, 2014, pp. 364–379. [14] K. I. Eder, W. Huang, J. Peleska, Complete agent-driven model-based system testing for autonomous systems, in: M. Farrell, M. Luck49

cuck (Eds.), Proceedings Third Workshop on Formal Methods for Autonomous Systems, FMAS 2021, Virtual, October 21-22, 2021, EPTCS, 2021, pp. 54–72. doi:10.4204/EPTCS.348.4. URL https://doi.org/10.4204/EPTCS.348.4 [15] R. Ganguly, Y. Xue, A. Jonckheere, P. Ljung, B. Schornstein, B. Bonakdarpour, M. Herlihy, Distributed runtime verification of metric temporal properties for cross-chain protocols, CoRR abs/2204.09796 (2022). arXiv:2204.09796, doi:10.48550/ARXIV.2204.09796. URL https://doi.org/10.48550/arXiv.2204.09796 [16] P. Gipps, A behavioural car-following model for computer simulation, Transportation Research Part B: Methodological 15 (2) (1981) 105–111. doi:https://doi.org/10.1016/0191-2615(81)90037-0. URL https://www.sciencedirect.com/science/article/pii/ 0191261581900370 [17] M. Treiber, A. Hennecke, D. Helbing, Congested traffic states in empirical observations and microscopic simulations, Physical Review E 62 (2) (2000) 1805–1824. doi:10.1103/physreve.62.1805. URL http://dx.doi.org/10.1103/PhysRevE.62.1805 [18] M. Bando, K. Hasebe, K. Nakanishi, A. Nakayama, Analysis of optimal velocity model with explicit delay, Phys. Rev. E 58 (1998) 5429–5435. doi:10.1103/PhysRevE.58.5429. URL https://link.aps.org/doi/10.1103/PhysRevE.58.5429 [19] S. Ulbrich, T. Menzel, A. Reschka, F. Schuldt, M. Maurer, Defining and substantiating the terms scene, situation, and scenario for automated driving, in: IEEE 18th International Conference on Intelligent Transportation Systems, ITSC 2015, Gran Canaria, Spain, September 15-18, 2015, IEEE, 2015, pp. 982–988. doi:10.1109/ITSC.2015.164. URL https://doi.org/10.1109/ITSC.2015.164 [20] M. Schwammberger, Introducing liveness into multi-lane spatial logic lane change controllers using UPPAAL, in: M. Gleirscher, S. Kugele, S. Linker (Eds.), Proceedings 2nd International Workshop on Safe Control of Autonomous Vehicles, SCAV@CPSWeek 2018, Porto, Portugal, 10th April 2018, Vol. 269 of EPTCS, 2018, pp. 17–31. doi: 50

10.4204/EPTCS.269.3. URL https://doi.org/10.4204/EPTCS.269.3 [21] W. Damm, E. Möhlmann, T. Peikenkamp, A. Rakow, A formal semantics for traffic sequence charts, in: M. Lohstroh, P. Derler, M. Sirjani (Eds.), Principles of Modeling - Essays Dedicated to Edward A. Lee on the Occasion of His 60th Birthday, Vol. 10760 of Lecture Notes in Computer Science, Springer, 2018, pp. 182–205. doi:10.1007/ 978-3-319-95246-8\_11. URL https://doi.org/10.1007/978-3-319-95246-8_11 [22] R. Stemmer, I. Saxena, L. Panneke, D. Grundt, A. Austel, E. Möhlmann, B. Westphal, Runtime monitoring of complex scenariobased requirements for autonomous driving functions, Science of Computer Programming 244 (2025) 103301. doi:10.1016/j.scico.2025. 103301. [23] C. A. Petri, Kommunikation mit Automaten, Dissertation, Schriften des IIM 2, Rheinisch-Westfälisches Institut für Instrumentelle Mathematik an der Universität Bonn, Bonn (1962). [24] E. Sarmiento, J. C. Leite, E. Almentero, G. Sotomayor Alzamora, Test scenario generation from natural language requirements descriptions based on petri-nets, Electronic Notes in Theoretical Computer Science 329 (2016) 123–148, cLEI 2016 - The Latin American Computing Conference. doi:https://doi.org/10.1016/j.entcs.2016.12.008. URL https://www.sciencedirect.com/science/article/pii/ S1571066116301153 [25] ASAM, ASAM OpenSCENARIO, https://publications.pages. asam.net/standards/ASAM_OpenSCENARIO/ASAM_OpenSCENARIO_XML/ latest/index.html (2024). [26] F. Finkeldei, C. Thees, J.-N. Weghorn, M. Althoff, Scenario factory 2.0: Scenario-based testing of automated vehicles with commonroad, Automotive Innovation 8 (2025) 207–220. doi:10.1007/ s42154-025-00360-0. [27] S. Yan, X. Zhang, K. Hao, H. Xin, Y. Luo, J. Yang, M. Fan, C. Yang, J. Sun, Z. Yang, On-demand scenario generation for testing automated driving systems, 2025, accepted by FSE 2025. doi:10.1145/3715722. 51

[28] Y. Zhao, J. Zhou, D. Bi, T. Mihalj, J. Hu, A. Eichberger, A survey on the application of large language models in scenario-based testing of automated driving systems, IEEE Transactions on Intelligent Transportation Systems (2025). doi:10.48550/arXiv.2505.16587. [29] M. Wild, J. S. Becker, C. Schneiders, E. Möhlmann, A scenario-based simulation framework for testing of highly automated railway systems, in: Proceedings of the 11th International Conference on Vehicle Technology and Intelligent Transport Systems (VEHITS 2025), 2025, pp. 88–99. doi:10.5220/0013286600003941. [30] D. Harel, H. Kugler, A. Pnueli, Synthesis revisited: Generating statechart models from scenario-based requirements, 2005, microsoft Research Technical Report / preprint. URL https://www.microsoft.com/en-us/research/wp-content/ uploads/2005/01/he05.pdf [31] PTV Group, Multimodal traffic simulation software, https://www. ptvgroup.com/en/products/ptv-vissim (2024). [32] OMG, OMG systems modeling language v2, https://www.omg.org/ spec/SysML/2.0/Beta2/About-SysML (2024). [33] S. Jafer, B. Chhaya, U. Durak, T. Gerlach, Formal scenario definition language for aviation: aircraft landing case study, in: AIAA modeling and simulation technologies conference, 2016, p. 3521. [34] F. Mallet, Clock constraint specification language: specifying clock constraints with UML/MARTE, Innov. Syst. Softw. Eng. 4 (3) (2008) 309– 314. doi:10.1007/S11334-008-0055-2. URL https://doi.org/10.1007/s11334-008-0055-2 [35] Y. Chen, R. Gandhi, Y. Zhang, C. Fan, NL2TL: transforming natural languages to temporal logics using large language models, in: H. Bouamor, J. Pino, K. Bali (Eds.), Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, EMNLP 2023, Singapore, December 6-10, 2023, Association for Computational Linguistics, 2023, pp. 15880–15903. doi:10.18653/V1/2023.EMNLP-MAIN. 985. URL https://doi.org/10.18653/v1/2023.emnlp-main.985 52

[36] I. Cohen, D. Peled, End-to-end AI generated runtime verification from natural language specification, in: B. Steffen (Ed.), Bridging the Gap Between AI and Reality - First International Conference, AISoLA 2023, Crete, Greece, October 23-28, 2023, Selected Papers, Vol. 14129 of Lecture Notes in Computer Science, Springer, 2023, pp. 362–384. doi:10.1007/978-3-031-73741-1\_23. URL https://doi.org/10.1007/978-3-031-73741-1_23 [37] A. Cavalcanti, A. Sampaio, A. Miyazawa, P. Ribeiro, M. Conserva Filho, A. Didier, W. Li, J. Timmis, Verified simulation for robotics, Science of Computer Programming 174 (2019) 1–37. doi:https://doi.org/10.1016/j.scico.2019.01.004. URL https://www.sciencedirect.com/science/article/pii/ S0167642318301655 [38] G. D. Giacomo, M. Y. Vardi, Linear temporal logic and linear dynamic logic on finite traces, in: F. Rossi (Ed.), IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013, IJCAI/AAAI, 2013, pp. 854–860. URL http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/ view/6997 [39] K. R. Apt, F. S. de Boer, E.-R. Olderog, Verification of Sequential and Concurrent Programs, Springer, Berlin Heidelberg New York, 2010.

53

Appendix A. Behavioural Semantics of SCSL System Test Configurations Appendix A.1. Valuation functions The behaviour of system test configurations is formalised by finite sequences π = σ0 .σ1 . . . σq of valuation functions σi : Vi −→ D. The index i of valuation σi is the number of the observation and stimulation step performed by the test equipment, and σi (v) is the value of some symbol v ∈ Vi that has been set or observed by the test equipment in this step. The symbol sets Vi contain the following variable names. 1. All parameter symbols of objects that are active in step i. If, for example, rover number j is part of the collaboration and active in step i, then Vi contains symbols coll.r[i].cmd, coll.r[i].dst, coll.r[i].id, coll.r[i].pos, coll.r[i].id. 2. All auxiliary variable symbols of active instances of elementary scenarios, including the implicitly defined auxiliary variables like active. If scenario instance Return(coll.r[j]) is active in step i, for example, Vi contains symbols Return(coll.r[j]).active and Return(coll.r[j]).auxisLoaded . 3. The global auxiliary variable symbol EoT indicating the end of the system test. The set D is the union of all variable types. The symbol sets Vi change between steps under the following conditions. 1. If an object is deleted from the collaboration in step i, its parameter symbols are no longer present in Vi+1 . 2. If an object is added to the collaboration in step i, its parameter symbols become elements of Vi+1 , Vi+2 , . . . until the object is removed again from the collaboration. 3. If an elementary scenario instance is runnable and its precondition is fulfilled in step i, its auxiliary variables are visible in Vi+1 . 4. If the execution state of an elementary scenario instance changes from active to ¬active in step i, then its auxiliary variable symbols are no longer contained in Vi+1 . 5. A schedule is illegal if an active scenario tries to evaluate attributes of a non-existing object (“runtime error”). Active scenarios can always check object reference ̸= null to ensure that these runtime errors do not occur. 54

Symbol EoT is contained in all symbol sets V0 , V1 , . . . , Vq . For valuations σi , i = 0, . . . , (q − 1), its value is σi (EoT) = false. Only the last valuation fulfils σq (EoT) = true. Appendix A.2. Execution cycles. Depending on the object type and its cycletime, objects need k ≥ 1 observation steps of the test equipment to complete one execution cycle. During this processing time, outputs remain unchanged, and only the last write to an input is considered in the next processing cycle. For example, if a processing cycle of the object starts in observation step i, the input values specified by σi are used in this cycle. Any output parameter y remains unchanged until the end of the cycle, that is, σi (y) = σi+1 (y) = · · · = σi+k−1 (y), and σi+k (y) returns the new value of y. If input parameter z is an end point of an interface connecting output y with z, then σi+1 (z) = σi+2 (z) = · · · = σi+k (z) = σi (y) and σi+k+1 (z) = σi+k (y). For the next processing cycle starting in step (i+k) and any input parameter x, the valuation σi+k (x) is considered. Previous valuations σi+k−1 (x), . . . , σi+1 (x) are disregarded. Appendix A.3. Scheduling. The following scheduling rules determine when an elementary scenario instance becomes active. 1. Every scenario instance transits through execution states passive −→ runnable −→ active −→ passive. 2. State active is characterised for a scenario instance S by S.active = true. 3. The auxiliary symbols of a scenario are visible in Vi if and only if it is active in observation step i. 4. A runnable scenario instance becomes active in step i + 1, if its precondition φ evaluates to true in step i. Since φ only refers to object parameters and never to auxiliary variables, it can be evaluated in any step i where all object parameter symbols occurring in φ are contained in Vi . If this is not the case because parameters of objects are referenced that are no longer part of the collaboration, the precondition is considered to be false. 5. In a parallel composition of scenario instances S1 ∥ S2 , both S1 and S2 become immediately runnable. 55

6. In a sequential composition of scenario instances S1 ; S2 , S2 remains passive until the S1 has traversed execution states passive −→ runnable −→ active −→ passive, whereafter S2 becomes runnable. Appendix A.4. The effect of interface definitions Suppose that a collaboration has interface interface I from O1 .a to O2 .b with objects O1 , O2 . An interface transfers the data “as fast as possible”, that is, in one observation cycle, from source to target. Therefore, in any test execution π = σ0 .σ1 . . . σq , the valuations involved satisfy ∀i : 0..(q − 1)  O1 .active ∈ dom σi ∧ O2 .active ∈ dom σi+1 ∧ σi (O1 .active) ∧ σi+1 (O2 .active) ⇒ σi+1 (O2 .b) = σi (O1 .a). Appendix A.5. The effect of collaboration changes As described in Section 3.8 dynamic collaboration changes are triggered by operations delete and create to be called in an action of an elementary scenario instance. This changes the collaboration variable in a atomic way: concurrent calls to change the collaboration are processed in an interleaving manner with nondeterministic sequencing. The collaboration acts like a monitor as created, for example, in Java using the synchronized statement. As with writes to other auxiliary variables written to in an action at cycle i, the effect of the collaboration change becomes visible at the beginning of the next cycle i + 1, so that the data distribution performed in cycle i + 1 is already based on the new collaboration status with its new interface wiring. Appendix A.6. Execution semantics of elementary scenario instances Given an elementary scenario instance S and a system test execution π = σ0 .σ1 . . . σq , the execution π conforms to S if certain S-specific rules hold. To explain these rules, let π ′ be the trace segment of π where S is active. Let Φ be the conjunction of LTL formulae that have been specified in the elementary scenario type of S, but with all parameter symbols exchanged by the corresponding concrete object parameters. For example, scenario type Pickup refers to symbols r, cc.cmd[i], cc.id[i] and others. These symbols are exchanged in Φ by the concrete object references and parameter names that are specified in the system test collaboration, that is, coll.r, coll.cc.cmd[i], coll.cc.id[i]. The latter are exactly the 56

symbols associated with concrete values by the valuation functions σi . Therefore, it can be checked whether π ′ is a model for Φ and consistent with the condition-action executions specified in the scenario type of S. Since we are dealing with finite sequences π ′ only, a finite interpretation of LTL semantics is required. For our purposes, the semantics proposed by De Giacomo and Vardi [38] is most appropriate. We only need to adapt the Next-operator semantics to take the cycle time of objects into account. Let π = σ1 . . . σk and assume that 1 ≤ i ≤ k. Then the following rules specify whether an LTL formula holds in position i of π ′ . 1. π ′ , i |= expr iff σi |= expr. Here, expr is a Boolean expression over actual parameters and auxiliary variables of the scenario instance. 2. π ′ , i |= ¬φ iff π ′ , i ̸|= φ. 3. π ′ , i |= φ1 ∧ φ2 iff π ′ , i |= φ1 and π ′ , i |= φ2 . 4. Let φ be an LTL formula referring to object parameters, parameters of S, and auxiliary variables of S. Let c ≥ 1 be the maximal cycle time of these objects.21 Then π ′ , i |= Xφ iff ∃ℓ ∈ {i + 1, . . . , min(k, 2c − 1)}  π ′ , ℓ |= φ. 5. π ′ , i |= φ1 Uφ2 iff there exists i ≤ j ≤ k such that π ′ , j |= φ2 and ∀ℓ ∈ {i, . . . , k − 1}  π ′ , ℓ |= φ1 . 6. A formula holds on the complete sequence π ′ , if it holds at the first index i = 1, that is, π ′ |= φ iff π ′ , 1 |= φ. The usual syntactic abbreviations Fφ ≡ trueUφ, Gφ ≡ ¬F¬φ, φ1 ⇒ φ2 ≡ ¬(φ1 ∧ ¬φ2 ), and φ1 ⇔ φ2 ≡ (φ1 ⇒ φ2 ∧ φ2 ⇒ φ1 ) are defined just as in conventional LTL. The modified semantics of the Next-operator is motivated as follows. If the formula application is performed in step i, then φ must become true in one of the next steps i + 1, . . . , i + 2c − 1, since in the worst case, the slowest object needs c − 1 steps to become aware of the state σi , and then another c steps to perform the actions that will make ψ evaluate to true. Note that in this finite-trace semantics Fφ must become true on π ′ . This is reasonable for elementary scenarios implementing test oracles: It is required to observe that φ becomes true at least once, and the test execution 21

If only parameters and auxiliary variables of S are referenced in φ, c = 1, since elementary scenario instances are executed with maximal processing speed.

57

must be long enough to make this happen. Conversely, Gφ just requires that φ is not violated while S is active. This is – of course – not a proof that Gφ holds on infinite executions, but it reflects the state of practice to test safety properties with a finite test execution. During the execution of S, all parameter symbols contained in the framevariable may be set by S, so that the LTL specifications become true or remain true. For observer scenario instances, frame is always empty, and the consistency of π ′ with the LTL specifications must be ensured by the referenced SUT objects alone. For the effect of condition-action executions, the following rules apply. 1. If the precondition of S evaluates to true for the first time in σi , then the effect of the initial action becomes visible in σi+1 . 2. If a condition-action has a guard condition [g] that evaluates to true in σj and S is active in σj and σj+1 , then the effect of the associated action becomes visible in σj+1 . 3. If a condition-action has a change condition when ( ψ ) and ψ evaluates to false in σj−1 and to true in σj , then the effect of the associated action becomes visible in σj+1 , provided that S is active in steps (j − 1), j, (j + 1). 4. The action semantics is that of conventional while-languages [39], but with terminating loops only. With this interpretation, auxiliary variables that are not affected by any action in step j remain unchanged in σj+1 .

58

Related documents

• The Complexity Kink: A Prompt-Side Structural Complexity Index for Code-Generation Reliability#978496
• Semantic Layer Induction from Raw Telemetry via Hierarchical LLM and RAG Abstraction#978497
• The Output-Space Hypothesis: Enumerative Equivalence Checking for Tensor Programs#978498
• DeltaSelect: Affordable A/B Testing for Coding Agents#978499
• Code-as-Auditor: Executable Compliance Reasoning via Regulation-to-Code#978500