Modeling and testing object-oriented distributed systems with linear-time temporal logic

We present a framework for constructing formal models of object-oriented di stributed systems and a property language to express behavioral constraints in such models. Most of the existing models have their origin in specific mathematical notations and/or concepts. In contrast, we have developed our model such that it accounts for a large set of phenomena associated with in dustrial implementations of object-oriented distributed systems, The model that we propose, while closer to industrial concerns and practice, still ha s the powerful features of formal approaches. It also offers the possibilit y to automatically check at service run-time that the final service impleme ntation has not violated and is not violating properties expressed at the a bstraction level of our model. In our model, which relies on event-based be havioral abstraction, we use linear-time temporal logic as the underlying f ormalism for the specification of properties. We introduce two novel operat ors which are especially useful for object-oriented systems and which provi de a number of advantages over the well-known temporal logic operators. A r ecent decision of one of our industrial partners to adopt our proposal into one of their development platforms can be seen as a strong evidence of the relevance of our work and as a promising step towards a better understandi ng between the academic formal methods community and industry. Copyright (C ) 2001 John Wiley & Sons, Ltd.