Marijn Rol: Verification of ASD multi-component systems in mCRL2

Event Details

Analytical Software Design (ASD) assists the creation of software systems. Systems designed in ASD are composed of multiple components in order to divide the complexity of the whole system over them. The verification of system properties and requirements is limited to the scope of single components, disallowing the verification of end-to-end properties. We present an approach for the verification of end-to-end properties on multi-component systems. This provides a higher confidence in the functional correctness and reliability. A system based on a real-life ASD model serves as use-case for the proposed approach. Results show that verification of multi-component systems can be done through mCRL2, but scalability issues are observed as larger systems are verified.