An Efficient and Flexible Synthesis of Behavioral Patterns Specifications employing the GR(1)

Abstract

The usage of the GR(1) subset of Linear Temporal Logic has been proposed as an efficient way of appying formal verification tools and techniques. Another important milestone for formal verification are behavioral specification patterns which ease the task of eliciting the expected behavior of software systems. Recently, attractive behavioral patterns specifications has been proposed in cutting edge domains such as robotic missions, but its codification in the GR(1) format has been pinpointed as a challenging process. In this work we propose the use of a flexible and powerful behavioral framework called FVS to specify and synthesize modern behavioral patterns in the GR(1) style to optimize the formal verification process. Formal and empirical validation of our initial results are also presented