[Context] Visual notations play an important role in requirements engineering by supporting communication and validation, while formal methods provide a foundation for rigorous analysis. [Problem] Automata with a formal semantics are typically not intended for direct use by requirements engineering practitioners, while visual approaches commonly used in requirements engineering do not support formal reasoning. [Principal Ideas] We introduce Automata-Represented Requirements, a visual approach that combines visual requirements modelling with a pattern-based language for formalizing real-time requirements and its underlying formal semantics. The approach aims to enable intuitive specification of behavioural requirements together with formal reasoning. [Contribution] We outline the design of Automata-Represented Requirements and describe its formal foundations. The approach is implemented as part of HanforPL, a pattern-based language and system for formalizing real-time requirements. Using illustrative examples from requirements engineering practice, we demonstrate how visual modeling and formal reasoning can be effectively integrated.

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

Automata-Represented Requirements in HanforPL

  • Tobias Kolzer,
  • Vincent Langenfeld,
  • Nico Hauff,
  • Elisabeth Henkel,
  • Andreas Podelski

摘要

[Context] Visual notations play an important role in requirements engineering by supporting communication and validation, while formal methods provide a foundation for rigorous analysis. [Problem] Automata with a formal semantics are typically not intended for direct use by requirements engineering practitioners, while visual approaches commonly used in requirements engineering do not support formal reasoning. [Principal Ideas] We introduce Automata-Represented Requirements, a visual approach that combines visual requirements modelling with a pattern-based language for formalizing real-time requirements and its underlying formal semantics. The approach aims to enable intuitive specification of behavioural requirements together with formal reasoning. [Contribution] We outline the design of Automata-Represented Requirements and describe its formal foundations. The approach is implemented as part of HanforPL, a pattern-based language and system for formalizing real-time requirements. Using illustrative examples from requirements engineering practice, we demonstrate how visual modeling and formal reasoning can be effectively integrated.