The importance of requirements in the process of designing correct systems is being increasingly recognized. In the last years, several formalisms for describing requirements have been developed and made their way into the design process.
PSL has been proposed as a means to write specifications that are both easy to read and mathematically precise; it integrates temporal operators and regular expressions, and allows for the representation of the full class of omega-regular languages.
RAT (Requirements Analysis Tool) is a tool supporting a methodology to pinpoint defects in a set of requirements specifying the expected behavior of the new system.
In particular, given a set of requirements R, expressed as a set of PSL properties, we propose to assess whether they are “strict” enough (i.e. all unexpected behaviors are ruled out) by checking if the set of “assertions” A (i.e. properties that are expected to hold on all the behaviors described by R), is indeed logically entailed by R.
Similarly, we check if our requirements are “permissive” enough (i.e. all interesting behaviors have not been ruled out), by checking if a set P of “possibilities” (i.e. properties that desribe behaviors that we expect R not to rule out) is indeed compatible with R.
RAT allows also to check whether a set of requirements is realizable, that’s if it there exists an implementation that, regardless of the behaviors of the enviroment compatible with the assumption on it, fulfills the guarantee on the behaviors of the system.
Last but not least, the tool provides the user the ability to play with the semantics of PSL properties by allowing the inspection of behaviors compatible with the PSL property itself.
RAT has been developed as a joint work among ES Unit of FBK and the Institute for Software Technology of the Technical University of Graz.
The development of RAT was made possible under the PROSYD project, founded by a generous grant of the European Commission, Information Society Technologies under contract 507219.
