Central to the problem frames approach is the distinction of three different descriptions: requirements R, domain assumptions W and specifications S, tied together with the socalled frame concern, a proof obligation that has to hold between them if a problem diagram is to be correct: S, W R. The form this proof should take is not fixed a priori. It might, however, be desirable to automate it in order to allow for an efficient analysis of large diagrams. To make this possible, we follow some earlier suggestions to use the Event Calculus as a suitable formalism for these descriptions. The main contribution of the present paper is a set of consistency rules as well as guidelines for passing from a problem diagram to its formal description. Categories and Subject Descriptors D.2.1 [Software Engineering]: Requirements/Specifications--Languages, Methodologies, Tools General Terms Design, Documentation, Languages
Thein Than Tun, Jon G. Hall, Lucia Rapanotti, Karl