pith. machine review for the scientific record. sign in

arxiv: 2604.25772 · v1 · submitted 2026-04-28 · 💻 cs.SE

Recognition: unknown

Scenario-based System Testing for Distributed Robotics Applications

Jan Peleska , Felix Br\"uning , Wen-Ling Huang , Anne E. Haxthausen
Authors on Pith no claims yet

Pith reviewed 2026-05-07 15:54 UTC · model grok-4.3

classification 💻 cs.SE
keywords scenario-based testingdistributed roboticsonline testingsystem-level testsdynamic reconfigurationtest compositionmodel-based testingSCSL
0
0 comments X

The pith

SCSL composes elementary scenarios into system tests for distributed robots and executes them online to handle nondeterminism and runtime changes.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces the SCenario Specification Language to enable automated system-level testing when monolithic models are impractical due to high complexity, nondeterminism, and dynamic configurations in distributed robotic systems. It shows how complex tests can be built by combining simpler scenario descriptions through sequential and parallel composition operators. Online test selection during execution addresses the inability to precompute all behaviors, while a collaboration construct allows the test platform to remove unavailable components, add new ones, and rewire interfaces at runtime. A sympathetic reader would care because this targets real-world collaborative robots, such as those in salvage missions, where traditional testing approaches break down. The work demonstrates these ideas through a prototype tool and an example execution trace.

Core claim

SCSL provides a language for specifying expected behaviors and stimuli in elementary scenarios that compose via sequential and parallel operators into full system tests, paired with an online execution platform that selects steps at runtime and a collaboration construct that supports removing, adding, and rewiring components dynamically during test runs.

What carries the argument

The SCenario Specification Language (SCSL) with its sequential and parallel composition operators plus collaboration construct, which decomposes tests and enables on-the-fly selection and reconfiguration without a single monolithic model.

Load-bearing premise

That breaking tests into elementary scenarios and selecting steps online during execution will cover the necessary behaviors of nondeterministic distributed systems without missing critical failures.

What would settle it

Running the SCSL prototype on a multi-robot salvage mission where a known nondeterministic failure mode occurs only after specific runtime reconfigurations, and checking whether the generated tests detect or exercise that failure.

Figures

Figures reproduced from arXiv: 2604.25772 by Anne E. Haxthausen, Felix Br\"uning, Jan Peleska, Wen-Ling Huang.

Figure 1
Figure 1. 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 propert… view at source ↗
Figure 2
Figure 2. Figure 2: Rover-type robot. Robots. There are n robots of the rover type (see view at source ↗
Figure 3
Figure 3. Figure 3: Instantiation of Fig. 1 for the ‘software-only’ system test deployment. view at source ↗
Figure 4
Figure 4. Figure 4: SCSL-Based Test Artifact Generation Workflow view at source ↗
Figure 5
Figure 5. 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 gener￾ated test executions follow well-defined paths from … view at source ↗
Figure 6
Figure 6. Figure 6: Example symbolic Büchi automaton. Step Transition Transition Expression Concrete Valuation 1 s0 → accept z = 1 ∧ x = p0 − 25 ∧ p0 = 42 {z := 1, x := 17, p0 = 42} view at source ↗
Figure 7
Figure 7. Figure 7: The Architecture of the System Test Execution. view at source ↗
Figure 8
Figure 8. Figure 8: Test Suite Schedule. 37 view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The manuscript presents the SCenario Specification Language (SCSL) for automated generation and execution of system-level tests targeting complex distributed robotics applications. It composes tests from elementary scenarios via sequential and parallel operators, supports online (on-the-fly) selection and execution to handle nondeterminism, and introduces a collaboration construct for dynamic runtime reconfiguration of components and interfaces. The claims are illustrated via a salvage-mission example with collaborating robots and a prototype tool platform.

Significance. If the runtime selection mechanism can be shown to systematically address nondeterminism, SCSL would offer a practical alternative to monolithic model-based testing for distributed systems whose configuration and behavior cannot be fully precomputed. The scenario-composition approach and collaboration construct directly target real engineering challenges in robotics; the prototype and example provide initial feasibility evidence.

major comments (2)
  1. [Abstract] Abstract: the central claim that online testing 'selects and executes test steps during runtime' to address nondeterminism without exhaustive precomputation is load-bearing, yet no decision procedure, coverage metric, or argument is supplied showing that critical interleavings arising from parallel composition and dynamic reconfiguration will be reached rather than missed.
  2. [Salvage mission example] Salvage-mission example: the illustration demonstrates syntax and concepts but supplies no quantitative data (e.g., number of paths explored, failure modes detected, or coverage achieved) that would allow assessment of whether the online mechanism actually mitigates the exponential path space described in the skeptic note.
minor comments (2)
  1. The abstract refers to 'automatically generated test execution' without clarifying the generation algorithm beyond composition; a dedicated section on the generation and selection engine would improve clarity.
  2. Notation for the collaboration construct and its reconfiguration operations should be defined more formally (e.g., via small-step semantics or pseudocode) to avoid ambiguity when components join or leave.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback and positive assessment of SCSL's relevance to distributed robotics testing challenges. We respond point-by-point to the major comments below, outlining revisions that will strengthen the presentation of the online selection mechanism and the illustrative example.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the central claim that online testing 'selects and executes test steps during runtime' to address nondeterminism without exhaustive precomputation is load-bearing, yet no decision procedure, coverage metric, or argument is supplied showing that critical interleavings arising from parallel composition and dynamic reconfiguration will be reached rather than missed.

    Authors: We agree that the abstract's emphasis on online testing is central and that the manuscript does not supply a formal decision procedure or coverage metric. The online mechanism, detailed in the tool platform description, selects steps at runtime by matching observed SUT states against scenario constraints and available collaboration reconfigurations, thereby avoiding exhaustive precomputation of all interleavings. In the revision we will add a subsection that (i) describes the concrete selection heuristics used by the prototype, (ii) explains how parallel operators and the collaboration construct influence which interleavings are exercised, and (iii) supplies an informal argument that runtime observation of nondeterministic outcomes allows the tester to reach critical paths that would be missed by any static precomputed schedule. The abstract will be revised to reflect this clarification rather than overstating guarantees. revision: yes

  2. Referee: [Salvage mission example] Salvage-mission example: the illustration demonstrates syntax and concepts but supplies no quantitative data (e.g., number of paths explored, failure modes detected, or coverage achieved) that would allow assessment of whether the online mechanism actually mitigates the exponential path space described in the skeptic note.

    Authors: The salvage-mission example is presented to illustrate syntax, composition operators, and the collaboration construct in a realistic setting. We acknowledge that it currently lacks quantitative metrics. In the revised manuscript we will extend the example section with execution statistics obtained from the prototype on the same scenario, including the number of distinct interleavings explored during online execution, the failure modes that were triggered, and a simple coverage count of exercised scenario elements. These data will be accompanied by a brief comparison to the size of the precomputed state space to illustrate the mitigation effect. revision: yes

Circularity Check

0 steps flagged

No circularity in SCSL language and tool presentation

full rationale

The paper introduces SCSL as a novel scenario specification language whose core constructs (elementary scenarios, sequential/parallel composition, and collaboration for dynamic reconfiguration) are defined directly by syntax and semantics, then illustrated on a robot salvage-mission example. No equations, fitted parameters, predictions of test coverage, or uniqueness theorems are claimed; the online (on-the-fly) selection mechanism is presented as an engineering feature of the tool platform rather than a derived result that reduces to its own inputs. No self-citations are invoked as load-bearing premises for the central claims. The contribution is therefore self-contained as a language definition plus prototype demonstration.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 2 invented entities

The central claims rest on domain assumptions about test composition and runtime selection rather than fitted parameters or new physical entities.

axioms (2)
  • domain assumption Elementary scenarios can be composed sequentially and in parallel to specify complex system-level test behavior.
    Invoked when describing how complex tests are built from elementary ones.
  • domain assumption Online (on-the-fly) test step selection can adequately exercise nondeterministic distributed systems without exhaustive precomputation.
    Central to addressing challenge (2) of substantial nondeterminism.
invented entities (2)
  • SCSL language no independent evidence
    purpose: Specification language for scenario-based test generation and execution
    New artifact introduced by the paper.
  • collaboration construct no independent evidence
    purpose: Mechanism for dynamic reconfiguration of test interfaces during execution
    New construct to handle changing SUT configurations.

pith-pipeline@v0.9.0 · 5518 in / 1352 out tokens · 47990 ms · 2026-05-07T15:54:07.020579+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

59 extracted references · 25 canonical work pages

  1. [1]

    Margaria, B

    J.Peleska, J.Brauer, W.Huang, Model-basedtestingforavionicsystems – 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 Lect...

    work page doi:10.1007/978-3-030-03427-6 2018

  2. [2]

    Hauer, T

    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, Auck- land, New Zealand, October 27-30, 2019, IEEE, 2019, pp. 2950–2955. doi:10.1109/ITSC.2019.8917326. URLhttps://doi.org/10.1109/ITSC.2019.8917326

    work page doi:10.1109/itsc.2019.8917326 2019

  3. [3]

    K. G. Larsen, M. Mikucionis, B. Nielsen, Online testing of real-time systems using uppaal, in: J. Grabowski, B. Nielsen (Eds.), Formal Ap- proaches to Software Testing, Springer Berlin Heidelberg, Berlin, Hei- delberg, 2005, pp. 79–94

    2005

  4. [4]

    S. D. Brookes, A. W. Roscoe, Deadlock analysis in networks of com- municating processes, Distributed Comput. 4 (1991) 209–230.doi: 10.1007/BF01784721. URLhttps://doi.org/10.1007/BF01784721

    work page doi:10.1007/bf01784721 1991

  5. [5]

    C. B. Nielsen, P. G. Larsen, J. S. Fitzgerald, J. Woodcock, J. Pe- leska, 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. URLhttps://doi.org/10.1145/2794381

    work page doi:10.1145/2794381 2015

  6. [6]

    Peleska, F

    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 Au- tonomous Robotic Systems - 26th Annual Conference, TAROS 2025, York, UK, August 20-22, 2025, Proceedings, Vol. 16045 of Lecture Notes in Computer Science,...

    work page doi:10.1007/978-3-032-01486-3_25 2025

  7. [7]

    Cavalcanti, R

    A. Cavalcanti, R. M. Hierons, Challenges in testing of cyclic sys- tems, in: Y. Aït-Ameur, F. Khendek, D. Méry (Eds.), 27th Inter- national 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. URLhttps://doi.org/10.1109/ICECCS59891.2023.00010

    work page doi:10.1109/iceccs59891.2023.00010 2023

  8. [8]

    Hilscher, S

    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, Sp...

    work page doi:10.1007/978-3-642-24559-6_28 2011

  9. [9]

    J. M. Spivey, The Z Notation: A Reference Manual, 2nd Edition, Pren- tice Hall, New York, NY, USA, 1992

    1992

  10. [10]

    C. B. Jones, Systematic Software Development Using VDM, Prentice- Hall, 1986

    1986

  11. [11]

    rep., OMG (2017)

    Object Management Group, OMG Unified Modeling Language (OMG UML), superstructure, version 2.5.1, Tech. rep., OMG (2017)

    2017

  12. [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. URLhttps://doi.org/10.1145/356625.356626

    work page doi:10.1145/356625.356626 1974

  13. [13]

    Mochizuki, M

    S. Mochizuki, M. Shimakawa, S. Hagihara, N. Yonezaki, Fast transla- tion 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

    2014

  14. [14]

    K. I. Eder, W. Huang, J. Peleska, Complete agent-driven model-based system testing for autonomous systems, in: M. Farrell, M. Luck- 49 cuck (Eds.), Proceedings Third Workshop on Formal Methods for Au- tonomous Systems, FMAS 2021, Virtual, October 21-22, 2021, EPTCS, 2021, pp. 54–72.doi:10.4204/EPTCS.348.4. URLhttps://doi.org/10.4204/EPTCS.348.4

    work page doi:10.4204/eptcs.348.4 2021

  15. [15]

    Ganguly, Y

    R. Ganguly, Y. Xue, A. Jonckheere, P. Ljung, B. Schornstein, B. Bonakdarpour, M. Herlihy, Distributed runtime verification of met- ric temporal properties for cross-chain protocols, CoRR abs/2204.09796 (2022).arXiv:2204.09796,doi:10.48550/ARXIV.2204.09796. URLhttps://doi.org/10.48550/arXiv.2204.09796

    work page doi:10.48550/arxiv.2204.09796 2022

  16. [16]

    A behavioural car-following model for computer simulation

    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. URLhttps://www.sciencedirect.com/science/article/pii/ 0191261581900370

    work page doi:10.1016/0191-2615(81)90037-0 1981

  17. [17]

    doi: 10.1103/physreve.62.1805

    M. Treiber, A. Hennecke, D. Helbing, Congested traffic states in empir- ical observations and microscopic simulations, Physical Review E 62 (2) (2000) 1805–1824.doi:10.1103/physreve.62.1805. URLhttp://dx.doi.org/10.1103/PhysRevE.62.1805

    work page doi:10.1103/physreve.62.1805 2000

  18. [18]

    Bando, K

    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. URLhttps://link.aps.org/doi/10.1103/PhysRevE.58.5429

    work page doi:10.1103/physreve.58.5429 1998

  19. [19]

    Defining and substantiating the terms scene, situation, and scenario for automated driving,

    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 Trans- portation Systems, ITSC 2015, Gran Canaria, Spain, September 15-18, 2015, IEEE, 2015, pp. 982–988.doi:10.1109/ITSC.2015.164. URLhttps://doi.org/10...

    work page doi:10.1109/itsc.2015.164 2015

  20. [20]

    Schwammberger, Introducing liveness into multi-lane spatial logic lane change controllers using UPPAAL, in: M

    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 Con- trol of Autonomous Vehicles, SCAV@CPSWeek 2018, Porto, Portu- gal, 10th April 2018, Vol. 269 of EPTCS, 2018, pp. 17–31.doi: 50 10.4204/EPTCS.269.3. UR...

    work page doi:10.4204/eptcs.269.3 2018

  21. [21]

    W. Damm, E. Möhlmann, T. Peikenkamp, A. Rakow, A formal seman- tics 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...

    work page doi:10.1007/978-3-319-95246-8_11 2018

  22. [22]

    Stemmer, I

    R. Stemmer, I. Saxena, L. Panneke, D. Grundt, A. Austel, E. Möhlmann, B. Westphal, Runtime monitoring of complex scenario- based requirements for autonomous driving functions, Science of Com- puter Programming 244 (2025) 103301.doi:10.1016/j.scico.2025. 103301

    work page doi:10.1016/j.scico.2025 2025

  23. [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)

    1962

  24. [24]

    Sarmiento, J

    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. URLhttps://www.sciencedirect....

    work page doi:10.1016/j.entcs.2016.12.008 2016

  25. [25]

    asam.net/standards/ASAM_OpenSCENARIO/ASAM_OpenSCENARIO_XML/ latest/index.html(2024)

    ASAM, ASAM OpenSCENARIO,https://publications.pages. asam.net/standards/ASAM_OpenSCENARIO/ASAM_OpenSCENARIO_XML/ latest/index.html(2024)

    2024

  26. [26]

    Finkeldei, C

    F. Finkeldei, C. Thees, J.-N. Weghorn, M. Althoff, Scenario fac- tory 2.0: Scenario-based testing of automated vehicles with com- monroad, Automotive Innovation 8 (2025) 207–220.doi:10.1007/ s42154-025-00360-0

    2025

  27. [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

    work page doi:10.1145/3715722 2025

  28. [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 Trans- portation Systems (2025).doi:10.48550/arXiv.2505.16587

    work page doi:10.48550/arxiv.2505.16587 2025

  29. [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 Tech- nology and Intelligent Transport Systems (VEHITS 2025), 2025, pp. 88–99.doi:10.5220/0013286600003941

    work page doi:10.5220/0013286600003941 2025

  30. [30]

    Harel, H

    D. Harel, H. Kugler, A. Pnueli, Synthesis revisited: Generating statechart models from scenario-based requirements, 2005, microsoft Research Technical Report / preprint. URLhttps://www.microsoft.com/en-us/research/wp-content/ uploads/2005/01/he05.pdf

    2005

  31. [31]

    ptvgroup.com/en/products/ptv-vissim(2024)

    PTV Group, Multimodal traffic simulation software,https://www. ptvgroup.com/en/products/ptv-vissim(2024)

    2024

  32. [32]

    OMG, OMG systems modeling language v2,https://www.omg.org/ spec/SysML/2.0/Beta2/About-SysML(2024)

    2024

  33. [33]

    Jafer, B

    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

    2016

  34. [34]

    Mallet, Clock constraint specification language: specifying clock con- straints with UML/MARTE, Innov

    F. Mallet, Clock constraint specification language: specifying clock con- straints with UML/MARTE, Innov. Syst. Softw. Eng. 4 (3) (2008) 309– 314.doi:10.1007/S11334-008-0055-2. URLhttps://doi.org/10.1007/s11334-008-0055-2

    work page doi:10.1007/s11334-008-0055-2 2008

  35. [35]

    Y. Chen, R. Gandhi, Y. Zhang, C. Fan, NL2TL: transforming nat- ural 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 Lin- guistics, 2023, pp. 158...

    work page doi:10.18653/v1/2023.emnlp-main 2023

  36. [36]

    Cohen, D

    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...

    work page doi:10.1007/978-3-031-73741-1 2023

  37. [37]

    Cavalcanti, A

    A. Cavalcanti, A. Sampaio, A. Miyazawa, P. Ribeiro, M. Con- serva 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. URLhttps://www.sciencedirect.com/science/article/pii/ S0167642318301655

    work page doi:10.1016/j.scico.2019.01.004 2019

  38. [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. URLhttp://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/ view/6997

    2013

  39. [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 se- quencesπ=σ 0.σ1 . . . σq of valuation func...

    2010

  40. [40]

    If, for example, rover numberjis part of the collaboration and active in stepi, thenV i contains symbolscoll.r[i].cmd,coll.r[i].dst,coll.r[i].id, coll.r[i].pos,coll.r[i].id

    All parameter symbols of objects that are active in stepi. If, for example, rover numberjis part of the collaboration and active in stepi, thenV i contains symbolscoll.r[i].cmd,coll.r[i].dst,coll.r[i].id, coll.r[i].pos,coll.r[i].id

  41. [41]

    If scenario instanceReturn(coll.r[j]) is active in stepi, for example,V i containssymbolsReturn(coll.r[j]).activeandReturn(coll.r[j]).aux isLoaded

    All auxiliary variable symbols of active instances of elementary scenar- ios, including the implicitly defined auxiliary variables likeactive. If scenario instanceReturn(coll.r[j]) is active in stepi, for example,V i containssymbolsReturn(coll.r[j]).activeandReturn(coll.r[j]).aux isLoaded

  42. [42]

    The setDis the union of all variable types

    The global auxiliary variable symbolEoTindicating the end of the system test. The setDis the union of all variable types. The symbol setsV i change between steps under the following conditions

  43. [43]

    If an object is deleted from the collaboration in stepi, its parameter symbols are no longer present inVi+1

  44. [44]

    until the object is removed again from the collaboration

    If an object is added to the collaboration in stepi, its parameter sym- bols become elements ofVi+1, Vi+2, . . .until the object is removed again from the collaboration

  45. [45]

    If an elementary scenario instance is runnable and its precondition is fulfilled in stepi, its auxiliary variables are visible inVi+1

  46. [46]

    If the execution state of an elementary scenario instance changes from activeto¬activein stepi, then its auxiliary variable symbols are no longer contained inVi+1

  47. [47]

    runtime error

    A schedule is illegal if an active scenario tries to evaluate attributes of a non-existing object (“runtime error”). Active scenarios can always checkobject reference̸=nullto ensure that these runtime errors do not occur. 54 SymbolEoTis contained in all symbol setsV 0, V1, . . . , Vq. For valuations σi, i= 0, . . . ,(q−1), its value isσ i(EoT) =false. Onl...

  48. [48]

    Every scenario instance transits through execution states passive− →runnable− →active− →passive

  49. [49]

    State active is characterised for a scenario instanceSbyS.active= true

  50. [50]

    The auxiliary symbols of a scenario are visible inVi if and only if it is active in observation stepi

  51. [51]

    Sinceφonly refers to object parameters and never to auxiliary variables, it can be evaluated in any stepiwhere all object parameter symbols occurring inφare contained inV i

    A runnable scenario instance becomes active in stepi+ 1, if its pre- conditionφevaluates totruein stepi. Sinceφonly refers to object parameters and never to auxiliary variables, it can be evaluated in any stepiwhere all object parameter symbols occurring inφare contained inV i. If this is not the case because parameters of objects are refer- enced that ar...

  52. [52]

    In a parallel composition of scenario instancesS1 ∥S 2, bothS 1 andS 2 become immediately runnable. 55

  53. [53]

    as fast as possible

    In a sequential composition of scenario instancesS1;S 2,S 2 remains pas- siveuntiltheS 1 hastraversedexecutionstatespassive− →runnable− → active− →passive, whereafterS 2 becomes runnable. Appendix A.4. The effect of interface definitions Suppose that a collaboration has interface interfaceIfromO 1.atoO 2.b with objectsO 1, O2. An interface transfers the d...

  54. [54]

    Letc≥1be the maximal cycle time of these objects.21 Then π′, i|=Xφiff∃ℓ∈ {i+ 1,

    Letφbe an LTL formula referring to object parameters, parameters of S, and auxiliary variables ofS. Letc≥1be the maximal cycle time of these objects.21 Then π′, i|=Xφiff∃ℓ∈ {i+ 1, . . . ,min(k,2c−1)} π ′, ℓ|=φ. 5.π ′, i|=φ 1Uφ2 iff there existsi≤j≤ksuch thatπ ′, j|=φ 2 and ∀ℓ∈ {i, . . . , k−1} π ′, ℓ|=φ 1

  55. [55]

    The usual syntactic abbreviationsFφ≡trueUφ,Gφ≡ ¬F¬φ,φ 1 ⇒φ 2 ≡ ¬(φ1 ∧ ¬φ2), andφ 1 ⇔φ 2 ≡(φ 1 ⇒φ 2 ∧φ 2 ⇒φ 1)are defined just as in conventional LTL

    A formula holds on the complete sequenceπ′, if it holds at the first indexi= 1, that is,π ′ |=φiffπ ′,1|=φ. The usual syntactic abbreviationsFφ≡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 ...

  56. [56]

    If the precondition ofSevaluates totruefor the first time inσ i, then the effect of the initial action becomes visible inσi+1

  57. [57]

    If a condition-action has a guard condition[g]that evaluates totrue inσ j andSis active inσ j andσ j+1, then the effect of the associated action becomes visible inσj+1

  58. [58]

    If a condition-action has a change conditionwhen(ψ)andψevaluates tofalseinσ j−1 and totrueinσ j, then the effect of the associated action becomes visible inσj+1, provided thatSis active in steps(j− 1), j,(j+ 1)

  59. [59]

    With this interpretation, auxiliary vari- ables that are not affected by any action in stepjremain unchanged inσ j+1

    The action semantics is that of conventional while-languages [39], but with terminating loops only. With this interpretation, auxiliary vari- ables that are not affected by any action in stepjremain unchanged inσ j+1. 58