On Optimization in Composition of Concurrent Formal Specifications

Bhed Bahadur BISTA  

IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E87-A    No.11    pp.2905-2908
Publication Date: 2004/11/01
Online ISSN: 
Print ISSN: 0916-8508
Type of Manuscript: Special Section LETTER (Special Section on Concurrent Systems and Hybrid Systems)
formal specification,  FDT,  LOTOS,  combining processes,  intermediate processes,  

Full Text: PDF(168.4KB)>>
Buy this Article

LOTOS parallel operator, which is a binary operator, is used to combine processes in order to express their concurrency. Unlike other LOTOS operators, various possibilities exist when combining processes by the parallel operator. If two processes are selected randomly for combining, the size of the composite intermediate process after combining may be large. In this paper, we propose an algorithm for selecting two processes out of three or more processes so that the size of the intermediate process is the smallest when combined by the parallel operator. Smaller size of an intermediate process means it takes less memory space which is very important in designing verification tools for systems or communication protocols specified in LOTOS.