A Declarative and Flexible Specification for Probabilistic and Quantitative Behavioral Patterns

Abstract

Probabilities and quantative measures represent a key feature in modern software development which is being applied in diverse domains such as robotic and satellite missions or Self-Adaptive Systems. In this work we present a declarative and graphical framework called Probabilistic FVS (Feather Weigh Visual Scenarios) to specify systems’ behavior with probabilistic and quantative capabilities. This framework is expressive enough to model most of the most known probabilistic specification patterns. Using patterns is a neat improvement to ease the task of specifying the expected behavior of systems and formally verified them with tools like model checkers. Our approach is validated employing a real case of study base on a nano-satellite mission. We also developed a user-profile interaction to obtain meaningful probabilistic measures for the case of study.