業務ロジックがどういうものか知らないけど仕様記述自体はできると思うよ

ただ形式仕様記述ができることと
論理矛盾の検出ができることの間には大きな隔たりがあるのが現状

状態の数が限られているならなんとかなるけど
状態変数に実数とか時間を持つとなると途端に検証が困難になる