Model-checking plus testing: From software architecture analysis to code testing

Software Model-Checking and Testing are some of the most used techniques to analyze software systems and identify hidden faults. While software model-checking allows for an exhaustive and automatic analysis of the system expressed through a model, software testing is based on a clever selection of "relevant" test cases, which may be manually or automatically run over the system. In this paper we analyze how those two analysis techniques may be integrated in a specific context, where a Software Architecture (SA) specification of the system is available, model-checking techniques axe used to validate the SA model conformance with respect to selected properties, while testing techniques are used to validate the implementation conformance to the SA model. The results of this research axe applied to an SDH Telecommunication system architecture designed by Siemens CNX.