Abstract:

It can be claimed that current Lotos environments don't support sufficiently the design of a large specification. Given the requirements and service specification of a protocol, a good Lotos environment should help to develop the final specification gradually step by step. At each step, it should also be possible to verify that the correct final specification is reachable, at least in principle. In this talk we pay attention to the CCS-related works of Celikkan, Cleaveland and Steffen. We examine their notion of partially defined specifications and show its usefulness also with respect to Lotos. However, there are some problems in applying the concept to specifications in full Lotos.