Automata-Represented Requirements in HanforPL
摘要
[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.