This thesis proposes a knowledge based critic for software specifications. The critic is part of an environment where the users can build their specifications using a Petri net based language, ObjNPN. The system tries to make the development of the specifications an interactive process. The user can invoke the critic as soon as a primitive specification has been developed. The critic performs a domain-dependent analysis of the specifications. A case-based approach is adopted using examples from the domain. The analysis involves critiquing the specifications for the presence/absence of components related to the policies of the domain. The system also provides mechanisms for performing symbolic execution of the specifications.