Keeping Behavioral Programs Alive: Specifying and Executing Liveness Requirements
arxiv(2024)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要