A Formal Framework for verification and validation of external behavioral models of Embedded Systems represented through Black Box Structures

Embedded Systems can be engineered using Cleanroom Software Engineering (CRSE) methodology as it considers all the quality issues as an integral part of the CRSE Life cycle model and lays stress on the reduced size and effort of testing through statistical use testing. Both CRSE and Embedded systems development methodology are based on stimulus-response models. The stimulus-response models are used for designing the external behavioral requirements. Thus, CRSE in a revised form can conveniently be used for the development of reliable embedded systems. Verification and validation of one model with the other, such as verifying the external behavior models (Black Box Structures) with the requirement specifications and vice versa, are the most important built-in features of CRSE. The verification and validation methods described in the literature are manual procedures which are based on either intuition or experience. CRSE suffers from lack of Formal Frameworks to verify Box structures with the requirements specification. In this paper, a framework is proposed for verifying Black box structures which are derived using END-TO-END processing requirements of the embedded systems. The verification mechanism is built around generation of stimulus-response sequences in two different ways and proving that the sequences generated are the same. Thus, the mechanism ensures that the system has been designed properly.