Formal Verification of Data for Parameterized Systems
Mathieu Clabaut · 2014
Systerel is an SME specializing in the development of safety-critical real-time systems. The question of data verification is related to efforts to reduce the development costs of safe2, software-based complex systems. This chapter describes the requirements and solutions associated with the verification of configuration data. The classic system specification and design cycle using subsystems, subsequently refined into material and software components, potentially over the course of multiple iterations, involves a number of functional and non-functional requirements. Once data with known properties has been produced, the next stage is to verify the conformity of the data with the identified properties. The chapter describes the different methods used for this purpose. It provides a significant contribution to improving the quality of verifications of the associated process.