|Final Report of the COST-247 Action|
Functionality decomposition of basic Lotos expressions with generalized termination, enabling and disabling
|Jozef Stefan Institute|
|Digital communications and networks department|
|POB 3000, SI-1001 Ljubljana, Slovenia|
|Tel: +386 61 1773 531|
|Fax: +386 61 1262 102|
A correctness-preserving transformation is proposed for functionality decomposition of Basic LOTOS expressions with generalised termination, enabling and disabling. Given a specification of the required external behaviour, i.e. the expected service of a distributed system, and a partitioning of the specified actions among the system components, the transformation derives behaviour of individual system components implementing the service. There may be an arbitrary finite number of system components pairwise communicating over auxiliary LOTOS gates.
This presentation has been given during the COST-247 International Workshop on Applied Formal Methods in System Design (Maribor, Slovenia, June 17--19, 1996).
COST-247 Working Group(s): 1
This Page was prepared by Mark Jorgensen.