Formal Aspects of Specification and Validation of Dynamic Adaptive System by Analyzing Execution Traces

Changes due to new upgrades in the software which is having several concurrently running components are certain to impact the existing system´s execution and performance. The present paper defines a formal approach that can be applied for validation of the system after component integration in the dynamic adaptive environment. One important means of assuring the validation of such system is through analyzing interactions among different components in the multithreaded environment. A technique has been proposed and developed to capture the run-time components interactions using. NET CLR mechanism, which has been able to successfully capture the interactions among components across all application threads which are running concurrently. Captured components interactions are traced into formal method based on pi-calculus and pi-calculus specifications of the system have been validated by Mobility Workbench (MWB). A case study has been presented on multithreaded dynamic-adaptive system.