Verification of Variable Software: an Experience Report
Richard Bubel, Crystal Chang Din, Reiner Hähnle · 2010
Abstract. We report on our experiences with formal specification and verification of variable and customizable software realized in a software product family architecture using the Java Modeling Language (JML) and the KeY verification system. Software product families can be adapted to different deployment scenarios and provide instantiable feature sets as requested by the customer. Along a small case study we explore how to generate JML specifications for/from a given feature configuration and report on verification attempts of selected methods of the derived product. We identify challenges that need to be solved to allow scalable specification and verification of variable software. 1