MODULAR FORMAL VERIFICATION OF SPECIFICATIONS OF CONCURRENT SYSTEMS