Patent ID: 8453117

Claim:
A method comprising, by one or more computer systems: accessing: an event-driven application input by a user, the event-driven application comprising source code; one or more use cases input by the user for the event-driven application, the use cases being formally specified using a predefined syntax and referring to one or more events that drives the event-driven application; and one or more functional requirements input by the user for the event-driven application, the functional requirements being formally specified using the predefined syntax and each referring to a requirement that the event-driven application needs to satisfy when a particular one of the use cases occurs; parsing the use cases and the functional requirements according to the predefined syntax to construct one or more validation modules for validating the event-driven application without any modification to the source code of the event-driven application for validation purposes; formally validating the event-driven application using the validation modules without relying on assertions inserted into the source code of the event-driven application for validation purposes; and if the formal validation finds one or more defects in the event-driven application, generating output for communication to the user identifying the defects.