Iterative refinement of specification for component based embedded systems

The current practice of component based engineering raises concerns in industry when the specification of proprietary components suffers from inaccuracy and incompleteness. The engineers face difficulties in producing quality systems since they lack knowledge on the interoperability of components. In order to address this issue, we present a novel framework for iterative refinement of specification for component based systems. The novelty is the use of a preliminary behavioral model as a source for triggering refinement iterations. Moreover, it exploits rigorous formal techniques to achieve high-level system validation as an integral part of the refinement procedure. The framework has been evaluated on an automotive system in which the embedded software control units were developed by third-party vendors. The final results produced an improved formal system specification that identified several behaviors that were previously unknown.