NuSMV2: an open source tool for symbolic model checking