Thu 27 Jun 2024 10:45 - 11:15 at M104 - Specification Chair(s): Kurt Schneider

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 Jun

Displayed 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
30m
Paper
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
30m
Paper
ReqCompletion: Domain-Enhanced Automatic Completion for Software RequirementsIEEE TCSE Distinguished Paper
Research Papers
Xiaoli Lian Beihang University, China, Jieping Ma Beihang University, Heyang Lv , Li Zhang Beihang University
11:45
30m
Paper
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