Fast formal analysis of requirements via “Topoi diagrams”

Abstract

Early testing of requirements can decrease the cost of removing errors in software projects. Howevel; unless done carefully, that testing process can sign8cantly add to the cost of requirements analysis. We show here that requirements expressed as topoi diagrams can be built and tested cheaply - using our SP2 algorithm, the formal temporal properties of a large class of topoi can be proven vely 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 usefulfo r requirements engineering than fo r traditional model checking domains. Secondly, our approach is betterfo r exploring the temporal occurrence of properties than the temporal ordering of properties. Withinthese restrictions, we can express a useful range of concepts currently seen in requirementsengineering, and a wide range of interesting temporalproperties.