Smart cyber agents are pivotal in software-intensive systems such as smart manufacturing, robotics, and the Internet of Things. These agents monitor physical surroundings through sensors and make impactful decisions that influence the environment. Software engineering challenges in this domain include the specification of interactive multi-agent tasks. The general-purpose Domain-Specific Language named LIrAs, Language for Interactive Agents, is a high-level language that allows for unambiguous custom pattern definition. Additionally, LIrAs facilitates interactions with human agents, a safety-critical situation requiring particular attention. This paper lays the foundation for LIrAs specifications translation to Stochastic Hybrid Automaton (SHA). The target SHA model structure follows a three-layer hierarchical structure and makes LIrAs specifications amenable to formal verification, specifically Statistical Model Checking, through the Uppaal tool, capable of including time-dependent physical phenomena, such as human fatigue and robot dynamics.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Verification-Oriented Specification of Multi-agent Interaction Patterns

  • Alberto Tagliaferro,
  • Livia Lestingi,
  • Matteo Rossi

摘要

Smart cyber agents are pivotal in software-intensive systems such as smart manufacturing, robotics, and the Internet of Things. These agents monitor physical surroundings through sensors and make impactful decisions that influence the environment. Software engineering challenges in this domain include the specification of interactive multi-agent tasks. The general-purpose Domain-Specific Language named LIrAs, Language for Interactive Agents, is a high-level language that allows for unambiguous custom pattern definition. Additionally, LIrAs facilitates interactions with human agents, a safety-critical situation requiring particular attention. This paper lays the foundation for LIrAs specifications translation to Stochastic Hybrid Automaton (SHA). The target SHA model structure follows a three-layer hierarchical structure and makes LIrAs specifications amenable to formal verification, specifically Statistical Model Checking, through the Uppaal tool, capable of including time-dependent physical phenomena, such as human fatigue and robot dynamics.