A formal approach to providing assurance to dynamically adaptive software