Using a Modular Distributed Temporal Logic for In-the-large Object Specification

TitleUsing a Modular Distributed Temporal Logic for In-the-large Object Specification
Publication TypeConference Proceedings
Year of Conference1998
AuthorsKüster Filipe, J.
Conference NameProc. of the First International Workshop on Component-based Software Development in Computational Logic (COCL'98), Pisa, Italy, September 19

Our general goal is to provide a semantic foundation for in-the-large specification of distributed information systems. We use \sc Troll, an object-oriented formal language, for system specification. Our claim is that objects are not enough as a modularisation unit when it comes to deal with very large systems. An intermediary concept between the system and the objects is needed for allowing reusability of specifications and provide a clearer system structure. Enriching \sc Troll with a module concept enforces us to develop new theoretical constructs ensuring an appropriate underpinning of the language. A modular distributed temporal logic \sc Mdtl has been developed which describes the dynamic aspects of modular systems. The main features of the logic are its own modularity, the ability to express inter-module (a)synchronous communication and intra-module concurrency. It also seems promising to support module refinement. \sc Mdtl is based on $n$-agent logics and interpreted over labelled prime event structures. In this paper we present the logic and semantics underlying the modular object-oriented specification language by means of a small toy example.