Formal requirements models: simulation, validation and veri cation
J. Paul Gibson · 2001
Requirements models have three distinct roles they are the principle media of communication between clients and requirements engineers, they are the only model upon which rigorous and automated analysis can be carried out before development begins, and they are the structural foundation upon which design and implementation depend. A major part of building requirements is the modelling of the system to be developed (or updated) together with the system environment. These models are, of course, abstractions of the real world and their operational semantics can be executed to provide a simulation model for validation: to show that the behaviour speci ed actually corresponds to what exists or what is required. The models also have to be veri ed to show their logical consistency. A formal object oriented method facilitates incremental development, where the integration of simulation (through animation), theorem proving and model checking increases con dence in model correctness. Formal requirements models: simulation, validation and veri cation Abstract Requirements models have three distinct roles they are the principle media of communication between clients and requirements engineers, they are the only model upon which rigorous and automated analysis can be carried out before development begins, and they are the structural foundation upon which design and implementation depend. A major part of building requirements is the modelling of the system to be developed (or updated) together with the system environment. These models are, of course, abstractions of the real world and their operational semantics can be executed to provide a simulation model for validation: to show that the behaviour speci ed actually corresponds to what exists or what is required. The models also have to be veri ed to show their logical consistency. A formal object oriented method facilitates incremental development, where the integration of simulation (through animation), theorem proving and model checking increases con dence in model correctness.Requirements models have three distinct roles they are the principle media of communication between clients and requirements engineers, they are the only model upon which rigorous and automated analysis can be carried out before development begins, and they are the structural foundation upon which design and implementation depend. A major part of building requirements is the modelling of the system to be developed (or updated) together with the system environment. These models are, of course, abstractions of the real world and their operational semantics can be executed to provide a simulation model for validation: to show that the behaviour speci ed actually corresponds to what exists or what is required. The models also have to be veri ed to show their logical consistency. A formal object oriented method facilitates incremental development, where the integration of simulation (through animation), theorem proving and model checking increases con dence in model correctness.