Fast formal analysis of requirements via "topoi diagrams"

  • Menzies T
  • Powell J
  • Houle M
  • 18


    Mendeley users who have this article in their library.
  • 10


    Citations of this article.


Early testing of requirements can decrease the cost of removing errors in software projects. However unless done carefully, that testing process can significantly add to the cost of requirements analysis. We show that requirements expressed as topoi diagrams can be built and tested cheaply sing our SP2 algorithm, the formal temporal properties of a large class of topoi can be proven very quickly, in time nearly linear in the number of nodes and edges in the diagram. There are two limitations to our approach. Firstly, topoi diagrams cannot express certain complex concepts such as iteration and sub-routine calls. Hence, our approach is more useful for requirements engineering than for traditional model checking domains. Secondly, our approach is better for exploring the temporal occurrence of properties than the temporal ordering of properties. Within these restrictions, we can express a useful range of concepts currently seen in requirements engineering, and a wide range of interesting temporal properties.

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document


Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free