Logics for Specifying Concurrent Information Systems
This chapter concentrates on a challenging problem of information system specification and design, namely how to cope on a high level of abstraction with concurrent behaviour and communication as implied by distribution. Since distributed information systems are reactive and open systems maintaining data bases and applications, it is crucial to develop high-level specification techniques that can cope with data and programs as well as with concurrent workflow and communication issues. Techniques from conceptual modeling, abstract data types, concurrent processes and communication protocols are relevant and have to be combined. In the approach presented here, temporal logic is used for specifying sequential object behaviour, and communication facilities are added for specifying interaction between concurrent objects. We study two distributed temporal logics dealing with communication in two different ways. D0 adds basic statements that can only express synchronous “calling” of predicates, while D1 adds much richer facilities for making local statements about other objects in their respective local logics. D0 is more operational and can be animated or implemented more easily, while D1 is intuitively more appealing and convenient for modeling and specification. We demonstrate by example how D1 can be effectively reduced to D0 in a sound and complete way.