SCALABLE METHODS FOR ANALYZING FORMALIZED REQUIREMENTS AND LOCALIZING ERRORS

摘要

According to some embodiments, a system and method are provided comprising a communication device operative to communicate with a user to obtain one or more requirements, wherein each requirement is defined using a formal notation; a requirements analysis module to receive the one or more requirements, store the one or more requirements, and analyze each requirement individually and two or more requirements in conjunction to determine whether a conflict exists in the one or more requirements; an error localization module to identify each requirement involved in the conflict and indicates how the one or more requirement conflicts; a memory for storing program instructions; at least one requirements analysis processor, coupled to the memory, and in communication with requirements analysis module and the error localization module and operative to execute program instructions to: analyze each requirement individually to determine if the requirement is self-conflicting by executing a self-conflicting module of the requirements analysis module; generate an error explanation by executing the error localization module in 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 module determining the requirement is self-conflicting; repetitively analyze each updated requirement to determine if the requirement self-conflicts until the self-conflicting module determines the requirement is not self-conflicting; analyze two or more requirements in conjunction to determine if two or more requirements conflict by executing a set-conflicting module of the requirements analysis module after it is determined each requirement is not self-conflicting; generate an error explanation by executing the error localization module in response to the set-conflicting module determining two or more requirements conflict; receive a second updated requirement from a user in response to the set-conflicting module determining two or more requirements conflict; and repetitively analyze each updated requirement with the set-conflicting module to determine if the two or more requirements conflict until the set-conflicting module determines the two or more requirement are not self-conflicting; generate an indication that requirements analysis is complete for the one or more requirements and the one or more requirements is validated for use in software design. Numerous other aspects are provided.

主权项

1. A system comprising:
a communication device operative to communicate with a user to obtain one or more requirements, wherein each requirement is defined using a formal notation; a requirements analysis module to receive the one or more requirements, store the one or more requirements, and analyze each requirement individually and two or more requirements in conjunction to determine whether a conflict exists in the one or more requirements; an error localization module to identify each requirement involved in the conflict and indicates how the one or more requirement conflicts; a memory for storing program instructions; at least one requirements analysis processor, coupled to the memory, and in communication with requirements analysis module and the error localization module and operative to execute program instructions to:
analyze each requirement individually to determine if the requirement is self-conflicting by executing a self-conflicting module of the requirements analysis module;generate an error explanation by executing the error localization module in 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 module determining the requirement is self-conflicting;repetitively analyze each updated requirement to determine if the requirement self-conflicts until the self-conflicting module determines the requirement is not self-conflicting;analyze two or more requirements in conjunction to determine if two or more requirements conflict by executing a set-conflicting module of the requirements analysis module after it is determined each requirement is not self-conflicting;generate an error explanation by executing the error localization module in response to the set-conflicting module determining two or more requirements conflict;receive a second updated requirement from a user in response to the set-conflicting module determining two or more requirements conflict; andrepetitively analyze each updated requirement with the set-conflicting module to determine if the two or more requirements conflict until the set-conflicting module determines the two or more requirement are not self-conflicting;generate an indication that requirements analysis is complete for the one or more requirements and the one or more requirements is validated for use in software design.