NuSMV 2: An OpenSource Tool for Symbolic Model Checking