Tool Support for the Compositional Development of Distributed Systems.
Georg Rock, Stephan Werner, Andreas Wolpers · 1997
There is a large number of formalisms available for the development of distributed, concurrent and reactive systems. Also, effort has been invested in the development of model checkers and theorem provers for such formalisms. We argue that for formal developments of a substantial size, the increased complexity of formalisms for compositional development (like [1]) requires tool support which goes beyond theorem provers for the bare formalism. In particular, we discuss the management of proof obligations, changes in the development, and the relationship between development structure and proof structure. 1 Introduction With respect to theoretical aspects, formal description techniques for state-based concurrent, reactive and distributed systems have been developed to a level of maturity where they promise real benefits for the development of systems. Unfortunately, the effort spent on tools for such formal methods has been focused on support for model checking or proving in the...