SCALABLE METHODS FOR ANALYZING FORMALIZED REQUIREMENTS AND LOCALIZING ERRORS

摘要

According to some embodiments, a system and method are provided comprising acommunication device operative to communicate with a user to obtain one ormorerequirements, wherein each requirement is defined using a formal notation; arequirementsanalysis module to receive the one or more requirements, store the one or morerequirements, and analyze each requirement individually and two or morerequirements inconjunction to determine whether a conflict exists in the one or morerequirements; an errorlocalization module to identify each requirement involved in the conflict andindicates howthe one or more requirement conflicts; a memory for storing programinstructions; at leastone requirements analysis processor, coupled to the memory, and incommunication withrequirements analysis module and the error localization module and operativeto executeprogram instructions to: analyze each requirement individually to determine iftherequirement is self-conflicting by executing a self-conflicting module of therequirementsanalysis module; generate an error explanation by executing the errorlocalization modulein response to the self-conflicting module determining the requirement self-conflicts;receive a first updated requirement from a user in response to the self-conflicting moduledetermining the requirement is self-conflicting; repetitively analyze eachupdatedrequirement to determine if the requirement self-conflicts until the self-conflicting moduledetermines the requirement is not self-conflicting; analyze two or morerequirements inconjunction to determine if two or more requirements conflict by executing aset-conflictingmodule of the requirements analysis module after it is determined eachrequirement is not self-conflicting; generate an error explanation byexecuting the errorlocalization module in response to the set-conflicting module determining twoor morerequirements conflict; receive a second updated requirement from a user inresponse to theset-conflicting module determining two or more requirements conflict; andrepetitivelyanalyze each updated requirement with the set-conflicting module to determineif the twoor more requirements conflict until the set-conflicting module determines thetwo or morerequirement are not self-conflicting; generate an indication that requirementsanalysis iscomplete for the one or more requirements and the one or more requirements isvalidatedfor use in software design. Numerous other aspects are provided.