Compositional modelling: The formal perspective

We provide a formal framework within which an Information System (IS) could be modelled, analysed, and verified in a compositional manner. Our work is based on Interval Temporal Logic (ITL) and its programming language subset, Tempura. This is achieved by considering IS, of an enterprise, as a class of reactive systems in which it is continually reacting to asynchronously occurring events within a given period of time. Such a reactive nature permits an enterprise to pursue its business activities to best compete with others in the market place. The technique is illustrated by applying it to a small case study from Public Service Systems (PSS).