Automatic verification of behavioral specifications in software intensive systems