Abstract Interpretation and Model Checking for Checking Secure Information Flow in Concurrent Systems