FSP and FLTL framework for specification and verification of middle-agents