Keeping Behavioral Programs Alive: Specifying and Executing Liveness Requirements
One of the benefits of using executable specifications such as Behavioral Programming (BP) is the ability to align the system implementation with its requirements. This is facilitated in BP by a protocol that allows independent implementation modules that specify what the system may, must, and must not do. By that, each module can enforce a single system requirement, including negative specifications such as “don’t do X after Y.” The existing BP protocol, however, allows only the enforcement of safety requirements and does not support the execution of liveness properties such as “do X at least three times.” To model liveness requirements in BP directly and independently, we propose idioms for tagging states with “must-finish,” indicating that tasks are yet to be completed. We show that this idiom allows a direct specification of known requirements patterns from the literature. We also offer semantics and two execution mechanisms, one based on a translation to Büchi automata and the other based on a Markov decision process (MDP). The latter approach offers the possibility of utilizing deep reinforcement learning (DRL) algorithms, which bear the potential to handle large software systems effectively. This paper presents a qualitative and quantitative assessment of the proposed approach using a proof-of-concept tool. A formal analysis of the MDP-based execution mechanism is given in an appendix.
Thu 27 JunDisplayed time zone: (UTC) Coordinated Universal Time change
10:45 - 12:15 | SpecificationResearch Papers / RE@Next! Papers at M104 Chair(s): Kurt Schneider Leibniz Universität Hannover, Software Engineering Group | ||
10:45 30mPaper | Keeping Behavioral Programs Alive: Specifying and Executing Liveness Requirements Research Papers Tom Yaacov Ben-Gurion University of the Negev, Achiya Elyasaf Ben-Gurion University of the Negev, Gera Weiss Ben-Gurion University of the Negev Pre-print | ||
11:15 30mPaper | ReqCompletion: Domain-Enhanced Automatic Completion for Software Requirements Research Papers Xiaoli Lian Beihang University, China, Jieping Ma Beihang University, Heyang Lv , Li Zhang Beihang University | ||
11:45 30mPaper | Using LLMs in Software Requirements Specifications: An Empirical Evaluation RE@Next! Papers Madhava Krishna , Bhagesh Gaur Indraprastha Institute of Information Technology, Delhi, Arsh Varma , Pankaj Jalote Pre-print |