Techniques for analysis and validation of software requirements specifications written in theknowledge representation language Templar are presented. Templar specifications are analyzedin terms of ambiguity, non-minimality, contradiction, incompleteness, and redundancy. SinceTemplar is a powerful knowledge representation language supporting a rich set of modelingprimitives, it is difficult to reason directly on Templar specifications. To solve this problem,Templar specifications are mapped into equivalent temporal logic programs which are analyzedin terms the criteria listed above. However, it is hard to reason about Templar specificationsbecause some of the criteria cannot be formally proven, and the verification of other criteriaconstitute undecidable or intractable problems. To overcome these difficulties, we consider aset of tractable conditions for each criteria, which serve as "alarms" for the user. If a conditionis violated then it means that the specification either definitely has or potentially can have aproblem. Furthermore, the user is notified about the source and the nature of the problem incertain cases.
展开▼
