New Horizons for Metamorphic Relationships in Formal Verification

Abstract

In this work we broadened the impact of the so called Metamorphic relationships (MR’s) in the formal verification phase. We showed the potential of our behavioral framework called FVS (Feather Weight Visual Scenarios) to successfully denote metamorphic properties in diverse, complex and meaningful domains such as UAV’s flying missions and operating systems for On Board Computers (OBC) for nano satellites. We employed MR’s to validate behavior in a BIG-DATA context, where possible a large amount of data and information seen as traces must be verified but also a novel way to relate different goals and UAV’s configurations in the context of the dynamic adaption of AUV’s missions due to changes in the requirements. In addition, we explored complementary behavior as a possible source for obtaining MR’s.